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

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have ha : a ≠ 0 := fun ha => by simp [ha] at hprod
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hb : b ≠ 0 := fun hb => by simp [hb] at hprod
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hc : c ≠ 0 := fun hc => by simp [hc] at hprod
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
let s : Finset ℤ := {a, b, c}
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
⊢ let d := {a, b, c}.gcd id;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
set d : ℤ := s.gcd id
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hadiv : d ∣ a := gcd_dvd (by simp [s])
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hbdiv : d ∣ b := gcd_dvd (by simp [s])
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hcdiv : d ∣ c := gcd_dvd (by simp [s])
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hdzero : d ≠ 0 := fun hdzero => by
  simpa [ha] using Finset.gcd_eq_zero_iff.1 hdzero a (by simp [s])
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
have hdp : d ^ n ≠ 0 := fun hdn => hdzero (pow_eq_zero hdn)
State after:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ let d := d;
  (a / d) ^ n + (b / d) ^ n = (c / d) ^ n ∧ {a / d, b / d, c / d}.gcd id = 1 ∧ a / d * (b / d) * (c / d) ≠ 0
Tactic:
refine' ⟨_, _, fun habs => _⟩
State after:
case refine'_1
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n

case refine'_2
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ {a / d, b / d, c / d}.gcd id = 1

case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : a / d * (b / d) * (c / d) = 0
⊢ False

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

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

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

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
⊢ a ∈ s
Tactic:
simp [s]
State after:
no goals

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
⊢ b ∈ s
Tactic:
simp [s]
State after:
no goals

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
⊢ c ∈ s
Tactic:
simp [s]
State after:
no goals

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d = 0
⊢ False
Tactic:
simpa [ha] using Finset.gcd_eq_zero_iff.1 hdzero a (by simp [s])
State after:
no goals

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d = 0
⊢ a ∈ s
Tactic:
simp [s]
State after:
no goals

State before:
case refine'_1
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Tactic:
obtain ⟨na, hna⟩ := hadiv
State after:
case refine'_1.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n

State before:
case refine'_1.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Tactic:
obtain ⟨nb, hnb⟩ := hbdiv
State after:
case refine'_1.intro.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
nb : ℤ
hnb : b = d * nb
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n

State before:
case refine'_1.intro.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
nb : ℤ
hnb : b = d * nb
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Tactic:
obtain ⟨nc, hnc⟩ := hcdiv
State after:
case refine'_1.intro.intro.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
nb : ℤ
hnb : b = d * nb
nc : ℤ
hnc : c = d * nc
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n

State before:
case refine'_1.intro.intro.intro
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
na : ℤ
hna : a = d * na
nb : ℤ
hnb : b = d * nb
nc : ℤ
hnc : c = d * nc
⊢ (a / d) ^ n + (b / d) ^ n = (c / d) ^ n
Tactic:
rwa [← mul_left_inj' hdp, add_mul, ← mul_pow, ← mul_pow, ← mul_pow, hna, hnb, hnc,
  Int.mul_ediv_cancel_left _ hdzero, Int.mul_ediv_cancel_left _ hdzero,
  Int.mul_ediv_cancel_left _ hdzero, mul_comm, ← hna, mul_comm, ← hnb, mul_comm, ← hnc]
State after:
no goals

State before:
case refine'_2
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ {a / d, b / d, c / d}.gcd id = 1
Tactic:
simpa [gcd_eq_gcd_image, d] using
  Finset.gcd_div_id_eq_one (show a ∈ ({a, b, c} : Finset ℤ) by simp) ha
State after:
no goals

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
⊢ a ∈ {a, b, c}
Tactic:
simp
State after:
no goals

State before:
case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : a / d * (b / d) * (c / d) = 0
⊢ False
Tactic:
simp only [mul_eq_zero] at habs
State after:
case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : (a / d = 0 ∨ b / d = 0) ∨ c / d = 0
⊢ False

State before:
case refine'_3
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
habs : (a / d = 0 ∨ b / d = 0) ∨ c / d = 0
⊢ False
Tactic:
rcases habs with ((Ha | Hb) | Hc)
State after:
case refine'_3.inl.inl
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Ha : a / d = 0
⊢ False

case refine'_3.inl.inr
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hb : b / d = 0
⊢ False

case refine'_3.inr
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hc : c / d = 0
⊢ False

State before:
case refine'_3.inl.inl
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Ha : a / d = 0
⊢ False
Tactic:
exact ha (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Ha)
State after:
no goals

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Ha : a / d = 0
⊢ a ∈ s
Tactic:
simp [s]
State after:
no goals

State before:
case refine'_3.inl.inr
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hb : b / d = 0
⊢ False
Tactic:
exact hb (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Hb)
State after:
no goals

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hb : b / d = 0
⊢ b ∈ s
Tactic:
simp [s]
State after:
no goals

State before:
case refine'_3.inr
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hc : c / d = 0
⊢ False
Tactic:
exact hc (Int.eq_zero_of_ediv_eq_zero (gcd_dvd (by simp [s])) Hc)
State after:
no goals

State before:
a b c : ℤ
n : ℕ
H : a ^ n + b ^ n = c ^ n
hprod : a * b * c ≠ 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
s : Finset ℤ := {a, b, c}
d : ℤ := s.gcd id
hadiv : d ∣ a
hbdiv : d ∣ b
hcdiv : d ∣ c
hdzero : d ≠ 0
hdp : d ^ n ≠ 0
Hc : c / d = 0
⊢ c ∈ s
Tactic:
simp [s]
State after:
no goals