Theorem: LoVe.BackwardProofs.square_square (LoVe/Homework/Homework2.lean)

State before:
a b c : ℕ
⊢ (a ^ 2) ^ 2 + (b ^ 2) ^ 2 = (c ^ 2) ^ 2 → a ^ 4 + b ^ 4 = c ^ 4
Tactic:
intro h
State after:
a b c : ℕ
h : (a ^ 2) ^ 2 + (b ^ 2) ^ 2 = (c ^ 2) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 4

State before:
a b c : ℕ
h : (a ^ 2) ^ 2 + (b ^ 2) ^ 2 = (c ^ 2) ^ 2
⊢ a ^ 4 + b ^ 4 = c ^ 4
Tactic:
rw [←pow_mul, ←pow_mul, ←pow_mul] at h
State after:
a b c : ℕ
h : a ^ (2 * 2) + b ^ (2 * 2) = c ^ (2 * 2)
⊢ a ^ 4 + b ^ 4 = c ^ 4

State before:
a b c : ℕ
h : a ^ (2 * 2) + b ^ (2 * 2) = c ^ (2 * 2)
⊢ a ^ 4 + b ^ 4 = c ^ 4
Tactic:
exact h
State after:
no goals