case intro.intro.intro
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Minimal a b (-c)
a b c : ℤ
⊢ Minimal a b c → Minimal a b (-c)
rintro ⟨⟨ha, hb, heq⟩, h2⟩
case intro.intro.intro.left
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Fermat42 a b (-c)

case intro.intro.intro.right
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs (-c) ≤ Int.natAbs c1
case intro.intro.intro
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Minimal a b (-c)
constructor
no goals
case intro.intro.intro.right
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs (-c) ≤ Int.natAbs c1
rwa [Int.natAbs_neg c]
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ a ^ 4 + b ^ 4 = (-c) ^ 2
case intro.intro.intro.left
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ Fermat42 a b (-c)
apply And.intro ha (And.intro hb _)
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ c ^ 2 = (-c) ^ 2
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ a ^ 4 + b ^ 4 = (-c) ^ 2
rw [heq]
no goals
a b c : ℤ
h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → Int.natAbs c ≤ Int.natAbs c1
ha : a ≠ 0
hb : b ≠ 0
heq : a ^ 4 + b ^ 4 = c ^ 2
⊢ c ^ 2 = (-c) ^ 2
exact (neg_sq c).symm