File tree Expand file tree Collapse file tree 1 file changed +8
-8
lines changed
Expand file tree Collapse file tree 1 file changed +8
-8
lines changed Original file line number Diff line number Diff line change @@ -200,11 +200,11 @@ def h (as : List Nat) :=
200200
201201/--
202202trace: [ splits ] Case split candidates
203- [ split ] #4615 := match bs with
203+ [ split ] #829a := match bs with
204204 | [] => 1
205205 | [ head ] => 2
206206 | head :: head_1 :: tail => 3
207- [ split ] #ec88 := match as with
207+ [ split ] #dce6 := match as with
208208 | [] => 1
209209 | [ head ] => 2
210210 | head :: head_1 :: tail => 3
@@ -220,7 +220,7 @@ example : h bs = 1 → h as ≠ 0 := by
220220 grind [h.eq_def] =>
221221 instantiate
222222 show_cases
223- cases #ec88
223+ cases #dce6
224224 instantiate
225225 focus instantiate
226226 instantiate
@@ -246,7 +246,7 @@ example : h bs = 1 → h as ≠ 0 := by
246246example : h bs = 1 → h as ≠ 0 := by
247247 grind [h.eq_def] =>
248248 instantiate | as
249- cases #ec88
249+ cases #dce6
250250 all_goals instantiate
251251
252252/--
@@ -292,12 +292,12 @@ example (r p q : Prop) : p ∨ r → p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p
292292example : h bs = 1 → h as ≠ 0 := by
293293 grind [h.eq_def] =>
294294 instantiate
295- cases #ec88 <;> instantiate
295+ cases #dce6 <;> instantiate
296296
297297example : h bs = 1 → h as ≠ 1 := by
298298 grind [h.eq_def] =>
299299 instantiate
300- cases #ec88
300+ cases #dce6
301301 any_goals instantiate
302302 sorry
303303
@@ -313,7 +313,7 @@ h✝ : as = []
313313example : h bs = 1 → h as ≠ 0 := by
314314 grind [h.eq_def] =>
315315 instantiate
316- cases #ec88
316+ cases #dce6
317317 next => skip
318318 all_goals sorry
319319
@@ -326,7 +326,7 @@ def g (as : List Nat) :=
326326example : g bs = 1 → g as ≠ 0 := by
327327 grind [g.eq_def] =>
328328 instantiate
329- cases #ec88
329+ cases #dce6
330330 next => instantiate
331331 next => finish
332332 tactic =>
You can’t perform that action at this time.
0 commit comments