Theorem: Bulgaria1998P6.lemma_1' (Compfiles/Bulgaria1998P6.lean)

State before:
a b c : ℕ
ha : 0 < a
hb : 0 < b
hc : 0 < c
h : a ^ 4 = b ^ 4 + c ^ 2
⊢ False
Tactic:
induction' a using Nat.strongInductionOn with a ih
State after:
case ind
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
⊢ False

State before:
case ind
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
⊢ False
Tactic:
have hab : Nat.gcd a b = 1 := sorry
State after:
case ind
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
⊢ False

State before:
case ind
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
⊢ False
Tactic:
obtain c_even | c_odd := Nat.even_or_odd c
State after:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
⊢ False

case ind.inr
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_odd : Odd c
⊢ False

State before:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
⊢ False
Tactic:
have a_odd : Odd a := sorry
State after:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
a_odd : Odd a
⊢ False

State before:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
a_odd : Odd a
⊢ False
Tactic:
have b_odd : Odd b := sorry
State after:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
a_odd : Odd a
b_odd : Odd b
⊢ False

State before:
case ind.inl
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_even : Even c
a_odd : Odd a
b_odd : Odd b
⊢ False
Tactic:
sorry
State after:
no goals

State before:
case ind.inr
b c : ℕ
hb : 0 < b
hc : 0 < c
a : ℕ
ih : ∀ m < a, 0 < m → m ^ 4 = b ^ 4 + c ^ 2 → False
ha : 0 < a
h : a ^ 4 = b ^ 4 + c ^ 2
hab : a.gcd b = 1
c_odd : Odd c
⊢ False
Tactic:
sorry
State after:
no goals