2023-10-15 01:16:09 +02:00
|
|
|
|
import Game.Tactic.Induction
|
|
|
|
|
|
import Game.MyNat.Addition
|
|
|
|
|
|
import Mathlib.Tactic.Have
|
|
|
|
|
|
import Mathlib.Tactic
|
|
|
|
|
|
|
|
|
|
|
|
example (a b : ℕ) : a + b = a → b = 0 := by
|
|
|
|
|
|
induction b with d hd
|
2024-02-29 17:19:01 +01:00
|
|
|
|
· /-
|
|
|
|
|
|
a : ℕ
|
|
|
|
|
|
⊢ a + 0 = a → 0 = 0
|
|
|
|
|
|
-/
|
|
|
|
|
|
sorry
|
|
|
|
|
|
· sorry
|
2023-10-15 01:16:09 +02:00
|
|
|
|
|
|
|
|
|
|
example (a b c : ℕ) (g : c = 0) : a + b = a → b = 0 := by
|
|
|
|
|
|
intro h -- h : a + b = a
|
|
|
|
|
|
induction b with d hd generalizing g
|
2024-02-29 17:19:01 +01:00
|
|
|
|
· /-
|
|
|
|
|
|
a b: ℕ
|
|
|
|
|
|
h✝ : a + b = a
|
|
|
|
|
|
h : a + 0 = a
|
|
|
|
|
|
⊢ 0 = 0
|
|
|
|
|
|
-/
|
|
|
|
|
|
sorry
|
|
|
|
|
|
· /-
|
|
|
|
|
|
case succ
|
|
|
|
|
|
a c d : ℕ
|
|
|
|
|
|
hd : c = 0 → a + d = a → d = 0
|
|
|
|
|
|
g : c = 0
|
|
|
|
|
|
h : a + MyNat.succ d = a
|
|
|
|
|
|
⊢ MyNat.succ d = 0
|
|
|
|
|
|
-/
|
|
|
|
|
|
sorry
|
