Theorem: exists_coprime (Flt/Euler.lean)

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
set d := Int.gcd a b with hd'
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
obtain ⟨A, HA⟩ : ↑d ∣ a := Int.gcd_dvd_left a b
State after:
case intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ?m.1006 * A
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ?m.1006 * A
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
obtain ⟨B, HB⟩ : ↑d ∣ b := Int.gcd_dvd_right a b
State after:
case intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ?m.1006 * A
B : ℤ
HB : b = ?m.1144 * B
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ?m.1006 * A
B : ℤ
HB : b = ?m.1144 * B
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
obtain ⟨C, HC⟩ : ↑d ∣ c :=
  by
  rw [← Int.pow_dvd_pow_iff hn, ← h, HA, HB, mul_pow, mul_pow, ← mul_add]
  exact dvd_mul_right _ _
State after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ?m.1006 * A
B : ℤ
HB : b = ?m.1144 * B
C : ℤ
HC : c = ?m.1220 * C
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ?m.1006 * A
B : ℤ
HB : b = ?m.1144 * B
C : ℤ
HC : c = ?m.1220 * C
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have hdpos : 0 < d := Int.gcd_pos_of_non_zero_left _ ha'
State after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have hd := Int.coe_nat_ne_zero_iff_pos.mpr hdpos
State after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have hsoln : A ^ n + B ^ n = C ^ n :=
  by
  apply Int.eq_of_mul_eq_mul_left (pow_ne_zero n hd)
  simp only [mul_add, ← mul_pow, ← HA, ← HB, ← HC, h]
State after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have hsoln' : B ^ n + A ^ n = C ^ n := by rwa [add_comm] at hsoln
State after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have hcoprime : IsCoprime A B :=
  by
  rw [← Int.gcd_eq_one_iff_coprime]
  apply Nat.eq_of_mul_eq_mul_left hdpos
  rw [← Int.natAbs_ofNat d, ← Int.gcd_mul_left, ← HA, ← HB, hd', Int.natAbs_ofNat, mul_one]
State after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have HA' : A.natAbs ≤ a.natAbs := by
  rw [HA]
  simp only [Int.natAbs_ofNat, Int.natAbs_mul]
  exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
State after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have HB' : B.natAbs ≤ b.natAbs := by
  rw [HB]
  simp only [Int.natAbs_ofNat, Int.natAbs_mul]
  exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
State after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
have HC' : C.natAbs ≤ c.natAbs := by
  rw [HC]
  simp only [Int.natAbs_ofNat, Int.natAbs_mul]
  exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
State after:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'

State before:
case intro.intro.intro
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ∃ a' b' c',
    Int.natAbs a' ≤ Int.natAbs a ∧ Int.natAbs b' ≤ Int.natAbs b ∧ Int.natAbs c' ≤ Int.natAbs c ∧ FltCoprime n a' b' c'
Tactic:
exact
  ⟨A, B, C, HA', HB', HC',
    ⟨right_ne_zero_of_mul (by rwa [HA] at ha'), right_ne_zero_of_mul (by rwa [HB] at hb'),
      right_ne_zero_of_mul (by rwa [HC] at hc'), hsoln⟩,
    hcoprime, coprime_add_self_pow hn hsoln hcoprime,
    coprime_add_self_pow hn hsoln' hcoprime.symm⟩
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ↑d ∣ c
Tactic:
rw [← Int.pow_dvd_pow_iff hn, ← h, HA, HB, mul_pow, mul_pow, ← mul_add]
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ↑d ^ n ∣ ↑d ^ n * (A ^ n + B ^ n)

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
⊢ ↑d ^ n ∣ ↑d ^ n * (A ^ n + B ^ n)
Tactic:
exact dvd_mul_right _ _
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ A ^ n + B ^ n = C ^ n
Tactic:
apply Int.eq_of_mul_eq_mul_left (pow_ne_zero n hd)
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ ↑d ^ n * (A ^ n + B ^ n) = ↑d ^ n * C ^ n

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
⊢ ↑d ^ n * (A ^ n + B ^ n) = ↑d ^ n * C ^ n
Tactic:
simp only [mul_add, ← mul_pow, ← HA, ← HB, ← HC, h]
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
⊢ B ^ n + A ^ n = C ^ n
Tactic:
rwa [add_comm] at hsoln
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ IsCoprime A B
Tactic:
rw [← Int.gcd_eq_one_iff_coprime]
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ Int.gcd A B = 1

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ Int.gcd A B = 1
Tactic:
apply Nat.eq_of_mul_eq_mul_left hdpos
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ d * Int.gcd A B = d * 1

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
⊢ d * Int.gcd A B = d * 1
Tactic:
rw [← Int.natAbs_ofNat d, ← Int.gcd_mul_left, ← HA, ← HB, hd', Int.natAbs_ofNat, mul_one]
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.natAbs a
Tactic:
rw [HA]
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.natAbs (↑d * A)

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.natAbs (↑d * A)
Tactic:
simp only [Int.natAbs_ofNat, Int.natAbs_mul]
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.gcd a b * Int.natAbs A

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
⊢ Int.natAbs A ≤ Int.gcd a b * Int.natAbs A
Tactic:
exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.natAbs b
Tactic:
rw [HB]
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.natAbs (↑d * B)

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.natAbs (↑d * B)
Tactic:
simp only [Int.natAbs_ofNat, Int.natAbs_mul]
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.gcd a b * Int.natAbs B

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
⊢ Int.natAbs B ≤ Int.gcd a b * Int.natAbs B
Tactic:
exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.natAbs c
Tactic:
rw [HC]
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.natAbs (↑d * C)

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.natAbs (↑d * C)
Tactic:
simp only [Int.natAbs_ofNat, Int.natAbs_mul]
State after:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.gcd a b * Int.natAbs C

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
⊢ Int.natAbs C ≤ Int.gcd a b * Int.natAbs C
Tactic:
exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos)
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ?m.4410 * A ≠ 0
Tactic:
rwa [HA] at ha'
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ?m.4476 * B ≠ 0
Tactic:
rwa [HB] at hb'
State after:
no goals

State before:
n : ℕ
hn : 0 < n
a b c : ℤ
ha' : a ≠ 0
hb' : b ≠ 0
hc' : c ≠ 0
h : a ^ n + b ^ n = c ^ n
d : ℕ := Int.gcd a b
hd' : d = Int.gcd a b
A : ℤ
HA : a = ↑d * A
B : ℤ
HB : b = ↑d * B
C : ℤ
HC : c = ↑d * C
hdpos : 0 < d
hd : ↑d ≠ 0
hsoln : A ^ n + B ^ n = C ^ n
hsoln' : B ^ n + A ^ n = C ^ n
hcoprime : IsCoprime A B
HA' : Int.natAbs A ≤ Int.natAbs a
HB' : Int.natAbs B ≤ Int.natAbs b
HC' : Int.natAbs C ≤ Int.natAbs c
⊢ ?m.4512 * C ≠ 0
Tactic:
rwa [HC] at hc'
State after:
no goals