File tree Expand file tree Collapse file tree 1 file changed +7
-6
lines changed
Expand file tree Collapse file tree 1 file changed +7
-6
lines changed Original file line number Diff line number Diff line change @@ -43,12 +43,13 @@ fun {α} {x} {xs} {y} {ys} h =>
4343 Classical.byContradiction
4444 (Lean.Grind.intro_with_eq (¬(x = y ∧ xs = ys)) (¬x = y ∨ ¬xs = ys) False (Lean.Grind.not_and (x = y) (xs = ys))
4545 fun h_1 =>
46- Eq.mp
47- (Eq.trans (Eq.symm (eq_true x_eq))
48- (Lean.Grind.eq_false_of_not_eq_true
49- (Eq.trans (Eq.symm (Lean.Grind.or_eq_of_eq_false_right (Lean.Grind.not_eq_of_eq_true (eq_true xs_eq))))
50- (eq_true h_1))))
51- True.intro)
46+ id
47+ (Eq.mp
48+ (Eq.trans (Eq.symm (eq_true x_eq))
49+ (Lean.Grind.eq_false_of_not_eq_true
50+ (Eq.trans (Eq.symm (Lean.Grind.or_eq_of_eq_false_right (Lean.Grind.not_eq_of_eq_true (eq_true xs_eq))))
51+ (eq_true h_1))))
52+ True.intro))
5253-/
5354#guard_msgs in #print ex3._proof_1_1
5455
You can’t perform that action at this time.
0 commit comments