Theorem: FltRegular.MayAssume.p_ne_three (FltRegular/MayAssume/Lemmas.lean)

State before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
⊢ n ≠ 3
Tactic:
intro hn
State after:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
⊢ False

State before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
⊢ False
Tactic:
have ha : a ≠ 0 := fun ha => by simp [ha] at hprod
State after:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
⊢ False

State before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
⊢ False
Tactic:
have hb : b ≠ 0 := fun hb => by simp [hb] at hprod
State after:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
⊢ False

State before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
⊢ False
Tactic:
have hc : c ≠ 0 := fun hc => by simp [hc] at hprod
State after:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ False

State before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ False
Tactic:
simp [hn, flt_three a b c ha hb hc] at h
State after:
no goals

State before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a = 0
⊢ False
Tactic:
simp [ha] at hprod
State after:
no goals

State before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b = 0
⊢ False
Tactic:
simp [hb] at hprod
State after:
no goals

State before:
a b c : ℤ
n : ℕ
hprod : a * b * c ≠ 0
h : a ^ n + b ^ n = c ^ n
hn : n = 3
ha : a ≠ 0
hb : b ≠ 0
hc : c = 0
⊢ False
Tactic:
simp [hc] at hprod
State after:
no goals