-- Mathlib/NumberTheory/FLT/Basic.lean
lemma isCoprime_of_gcd_eq_one_of_FLT {n : ℕ} {a b c : ℤ} (Hgcd : Finset.gcd {a, b, c} id = 1)
    (HF : a ^ n + b ^ n + c ^ n = 0) : IsCoprime a b

Proof state:
case inr.refine_1
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ ¬(a = 0 ∧ b = 0)

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case inr.refine_1.intro
n : ℕ
c : ℤ
hn : n ≠ 0
Hgcd : {0, 0, c}.gcd id = 1
HF : 0 ^ n + 0 ^ n + c ^ n = 0
⊢ False

Proof state:
case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ 1

Tactic:
rw [← Hgcd]

Result:
case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ {a, b, c}.gcd id

Proof state:
case inr.refine_1.intro
n : ℕ
c : ℤ
hn : n ≠ 0
Hgcd : {0, 0, c}.gcd id = 1
HF : c = 0
⊢ False

Tactic:
simp only [HF, Finset.mem_singleton, Finset.insert_eq_of_mem, Finset.gcd_singleton, id_eq,
  map_zero, zero_ne_one] at Hgcd

Result:
no goals

Proof state:
case inr
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ IsCoprime a b

Tactic:
refine isCoprime_of_prime_dvd  ?_ <| (fun p hp hpa hpb ↦ hp.not_dvd_one ?_)

Result:
case inr.refine_1
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ ¬(a = 0 ∧ b = 0)

case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ 1

Proof state:
case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ p ∣ id x

Tactic:
rcases hx with hx | hx | hx <;> simp only [id_eq, hx, hpa, hpb,
  dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT hp hpa hpb HF]

Result:
no goals

Proof state:
case inr.refine_1.intro
n : ℕ
c : ℤ
hn : n ≠ 0
Hgcd : {0, 0, c}.gcd id = 1
HF : 0 ^ n + 0 ^ n + c ^ n = 0
⊢ False

Tactic:
simp only [ne_eq, hn, not_false_eq_true, zero_pow, add_zero, zero_add, pow_eq_zero_iff]
  at HF

Result:
case inr.refine_1.intro
n : ℕ
c : ℤ
hn : n ≠ 0
Hgcd : {0, 0, c}.gcd id = 1
HF : c = 0
⊢ False

Proof state:
case inl
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ 0 + b ^ 0 + c ^ 0 = 0
⊢ IsCoprime a b

Tactic:
simp only [pow_zero, Int.reduceAdd, OfNat.ofNat_ne_zero] at HF

Result:
no goals

Proof state:
case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ {a, b, c}.gcd id

Tactic:
refine Finset.dvd_gcd_iff.mpr fun x hx ↦ ?_

Result:
case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x ∈ {a, b, c}
⊢ p ∣ id x

Proof state:
case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x ∈ {a, b, c}
⊢ p ∣ id x

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx

Result:
case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
x : ℤ
hx : x = a ∨ x = b ∨ x = c
⊢ p ∣ id x

Proof state:
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
⊢ IsCoprime a b

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ 0 + b ^ 0 + c ^ 0 = 0
⊢ IsCoprime a b

case inr
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ IsCoprime a b