-- Mathlib/NumberTheory/FLT/Four.lean
theorem mul {a b c k : ℤ} (hk0 : k ≠ 0) :
    Fermat42 a b c ↔ Fermat42 (k * a) (k * b) (k ^ 2 * c)

Proof state:
case mp.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Tactic:
have H : a ^ 4 + b ^ 4 = c ^ 2 := f42.2.2

Result:
case mp.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
H : a ^ 4 + b ^ 4 = c ^ 2
⊢ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Proof state:
case mp
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Tactic:
constructor

Result:
case mp.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * a ≠ 0

case mp.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Proof state:
case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 2

Tactic:
apply (mul_right_inj' (pow_ne_zero 4 hk0)).mp

Result:
case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ k ^ 4 * (a ^ 4 + b ^ 4) = k ^ 4 * c ^ 2

Proof state:
case mp.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Tactic:
constructor

Result:
case mp.right.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * b ≠ 0

case mp.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Proof state:
case mp.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
H : a ^ 4 + b ^ 4 = c ^ 2
⊢ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Tactic:
linear_combination k ^ 4 * H

Result:
no goals

Proof state:
case mp.right.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * b ≠ 0

Tactic:
exact mul_ne_zero hk0 f42.2.1

Result:
no goals

Proof state:
case mp.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * a ≠ 0

Tactic:
exact mul_ne_zero hk0 f42.1

Result:
no goals

Proof state:
a b c k : ℤ
hk0 : k ≠ 0
⊢ Fermat42 a b c ↔ Fermat42 (k * a) (k * b) (k ^ 2 * c)

Tactic:
delta Fermat42

Result:
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 ↔ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Proof state:
case mpr.right.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0

Tactic:
exact right_ne_zero_of_mul f42.2.1

Result:
no goals

Proof state:
case mp
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 → k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Tactic:
intro f42

Result:
case mp
a b c k : ℤ
hk0 : k ≠ 0
f42 : a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Proof state:
case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ k ^ 4 * (a ^ 4 + b ^ 4) = k ^ 4 * c ^ 2

Tactic:
linear_combination f42.2.2

Result:
no goals

Proof state:
case mpr
a b c k : ℤ
hk0 : k ≠ 0
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2 → a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Tactic:
intro f42

Result:
case mpr
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Proof state:
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 ↔ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

Tactic:
constructor

Result:
case mp
a b c k : ℤ
hk0 : k ≠ 0
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 → k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2

case mpr
a b c k : ℤ
hk0 : k ≠ 0
⊢ k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2 → a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Proof state:
case mpr
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Tactic:
constructor

Result:
case mpr.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0

case mpr.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Proof state:
case mpr.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2

Tactic:
constructor

Result:
case mpr.right.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ b ≠ 0

case mpr.right.right
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 2

Proof state:
case mpr.left
a b c k : ℤ
hk0 : k ≠ 0
f42 : k * a ≠ 0 ∧ k * b ≠ 0 ∧ (k * a) ^ 4 + (k * b) ^ 4 = (k ^ 2 * c) ^ 2
⊢ a ≠ 0

Tactic:
exact right_ne_zero_of_mul f42.1

Result:
no goals