-- Mathlib/NumberTheory/FLT/Four.lean
theorem coprime_of_minimal {a b c : ℤ} (h : Minimal a b c) : IsCoprime a b

Proof state:
case intro.intro.intro.intro.intro
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
hpc : ↑p ^ 2 ∣ c
⊢ False

Tactic:
obtain ⟨c1, rfl⟩ := hpc

Result:
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < c1.natAbs

Tactic:
exact Nat.pos_of_ne_zero (Int.natAbs_ne_zero.2 (ne_zero hf))

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 1 < p ^ 2

Tactic:
exact Nat.one_lt_pow two_ne_zero (Nat.Prime.one_lt hp)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
⊢ False

Tactic:
have hpc : (p : ℤ) ^ 2 ∣ c := by
  rw [← Int.pow_dvd_pow_iff two_ne_zero, ← h.1.2.2]
  apply Dvd.intro (a1 ^ 4 + b1 ^ 4)
  ring

Result:
case intro.intro.intro.intro.intro
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
hpc : ↑p ^ 2 ∣ c
⊢ False

Proof state:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
⊢ ↑p ^ 2 ∣ c

Tactic:
rw [← Int.pow_dvd_pow_iff two_ne_zero, ← h.1.2.2]

Result:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
⊢ (↑p ^ 2) ^ 2 ∣ (↑p * a1) ^ 4 + (↑p * b1) ^ 4

Proof state:
case intro.intro.intro.intro
b c : ℤ
p : ℕ
hp : Nat.Prime p
hpb : p ∣ b.natAbs
a1 : ℤ
h : Minimal (↑p * a1) b c
hab : ¬(↑p * a1).gcd b = 1
hpa : p ∣ (↑p * a1).natAbs
⊢ False

Tactic:
obtain ⟨b1, rfl⟩ := Int.natCast_dvd.mpr hpb

Result:
case intro.intro.intro.intro.intro
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ c1.natAbs < (↑p ^ 2 * c1).natAbs

Tactic:
rw [Int.natAbs_mul, lt_mul_iff_one_lt_left, Int.natAbs_pow, Int.natAbs_ofNat]

Result:
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 1 < p ^ 2

case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ 0 < c1.natAbs

Proof state:
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
⊢ False

Tactic:
have hf : Fermat42 a1 b1 c1 :=
  (Fermat42.mul (Int.natCast_ne_zero.mpr (Nat.Prime.ne_zero hp))).mpr h.1

Result:
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ False

Proof state:
case intro.intro.intro
a b c : ℤ
h : Minimal a b c
hab : ¬a.gcd b = 1
p : ℕ
hp : Nat.Prime p
hpa : p ∣ a.natAbs
hpb : p ∣ b.natAbs
⊢ False

Tactic:
obtain ⟨a1, rfl⟩ := Int.natCast_dvd.mpr hpa

Result:
case intro.intro.intro.intro
b c : ℤ
p : ℕ
hp : Nat.Prime p
hpb : p ∣ b.natAbs
a1 : ℤ
h : Minimal (↑p * a1) b c
hab : ¬(↑p * a1).gcd b = 1
hpa : p ∣ (↑p * a1).natAbs
⊢ False

Proof state:
a b c : ℤ
h : Minimal a b c
hab : ¬a.gcd b = 1
⊢ False

Tactic:
obtain ⟨p, hp, hpa, hpb⟩ := Nat.Prime.not_coprime_iff_dvd.mp hab

Result:
case intro.intro.intro
a b c : ℤ
h : Minimal a b c
hab : ¬a.gcd b = 1
p : ℕ
hp : Nat.Prime p
hpa : p ∣ a.natAbs
hpb : p ∣ b.natAbs
⊢ False

Proof state:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
⊢ (↑p ^ 2) ^ 2 ∣ (↑p * a1) ^ 4 + (↑p * b1) ^ 4

Tactic:
apply Dvd.intro (a1 ^ 4 + b1 ^ 4)

Result:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
⊢ (↑p ^ 2) ^ 2 * (a1 ^ 4 + b1 ^ 4) = (↑p * a1) ^ 4 + (↑p * b1) ^ 4

Proof state:
a b c : ℤ
h : Minimal a b c
⊢ a.gcd b = 1

Tactic:
by_contra hab

Result:
a b c : ℤ
h : Minimal a b c
hab : ¬a.gcd b = 1
⊢ False

Proof state:
c : ℤ
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
h : Minimal (↑p * a1) (↑p * b1) c
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
⊢ (↑p ^ 2) ^ 2 * (a1 ^ 4 + b1 ^ 4) = (↑p * a1) ^ 4 + (↑p * b1) ^ 4

Tactic:
ring

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ False

Tactic:
apply Nat.le_lt_asymm (h.2 _ _ _ hf)

Result:
case intro.intro.intro.intro.intro.intro
p : ℕ
hp : Nat.Prime p
a1 : ℤ
hpa : p ∣ (↑p * a1).natAbs
b1 : ℤ
hpb : p ∣ (↑p * b1).natAbs
hab : ¬(↑p * a1).gcd (↑p * b1) = 1
c1 : ℤ
h : Minimal (↑p * a1) (↑p * b1) (↑p ^ 2 * c1)
hf : Fermat42 a1 b1 c1
⊢ c1.natAbs < (↑p ^ 2 * c1).natAbs

Proof state:
a b c : ℤ
h : Minimal a b c
⊢ IsCoprime a b

Tactic:
apply Int.isCoprime_iff_gcd_eq_one.mpr

Result:
a b c : ℤ
h : Minimal a b c
⊢ a.gcd b = 1