Theorem: MyNat.add_squared (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
⊢ (a + b) ^ two = a ^ two + b ^ two + two * a * b
Tactic:
rw [two_eq_succ_one]
State after:
a b : Nat
⊢ (a + b) ^ succ one = a ^ succ one + b ^ succ one + succ one * a * b

State before:
a b : Nat
⊢ (a + b) ^ succ one = a ^ succ one + b ^ succ one + succ one * a * b
Tactic:
rw [one_eq_succ_zero]
State after:
a b : Nat
⊢ (a + b) ^ succ (succ zero) = a ^ succ (succ zero) + b ^ succ (succ zero) + succ (succ zero) * a * b

State before:
a b : Nat
⊢ (a + b) ^ succ (succ zero) = a ^ succ (succ zero) + b ^ succ (succ zero) + succ (succ zero) * a * b
Tactic:
rw [pow_succ, pow_succ, pow_succ, pow_succ, pow_succ, pow_succ]
State after:
a b : Nat
⊢ (a + b) ^ zero * (a + b) * (a + b) = a ^ zero * a * a + b ^ zero * b * b + succ (succ zero) * a * b

State before:
a b : Nat
⊢ (a + b) ^ zero * (a + b) * (a + b) = a ^ zero * a * a + b ^ zero * b * b + succ (succ zero) * a * b
Tactic:
rw [pow_zero, pow_zero, pow_zero]
State after:
a b : Nat
⊢ one * (a + b) * (a + b) = one * a * a + one * b * b + succ (succ zero) * a * b

State before:
a b : Nat
⊢ one * (a + b) * (a + b) = one * a * a + one * b * b + succ (succ zero) * a * b
Tactic:
rw [one_mul, one_mul, one_mul]
State after:
a b : Nat
⊢ (a + b) * (a + b) = a * a + b * b + succ (succ zero) * a * b

State before:
a b : Nat
⊢ (a + b) * (a + b) = a * a + b * b + succ (succ zero) * a * b
Tactic:
rw [add_mul, mul_add, mul_add]
State after:
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + succ (succ zero) * a * b

State before:
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + succ (succ zero) * a * b
Tactic:
rw [succ_mul, succ_mul, zero_mul, zero_add, add_mul]
State after:
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + (a * b + a * b)

State before:
a b : Nat
⊢ a * a + a * b + (b * a + b * b) = a * a + b * b + (a * b + a * b)
Tactic:
rw [add_assoc]
State after:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + b * b + (a * b + a * b)

State before:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + b * b + (a * b + a * b)
Tactic:
rw [add_assoc (a*a) _ _]
State after:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (b * b + (a * b + a * b))

State before:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (b * b + (a * b + a * b))
Tactic:
rw [add_left_comm (b*b) (a*b) (a*b)]
State after:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (a * b + (b * b + a * b))

State before:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (a * b + (b * b + a * b))
Tactic:
rw [add_comm (b*b) (a*b)]
State after:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (a * b + (a * b + b * b))

State before:
a b : Nat
⊢ a * a + (a * b + (b * a + b * b)) = a * a + (a * b + (a * b + b * b))
Tactic:
rw [mul_comm a b]
State after:
no goals