Theorem: HTPI.Example_6_3_2_cheating (HTPILib/Chap6.lean)

State before:
⊢ ∀ (a : ℝ) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Tactic:
fix a : Real
State after:
a : ℝ
⊢ ∀ (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n

State before:
a : ℝ
⊢ ∀ (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Tactic:
fix m : Nat
State after:
a : ℝ
m : ℕ
⊢ ∀ (n : ℕ), a ^ (m + n) = a ^ m * a ^ n

State before:
a : ℝ
m : ℕ
⊢ ∀ (n : ℕ), a ^ (m + n) = a ^ m * a ^ n
Tactic:
fix n : Nat
State after:
a : ℝ
m n : ℕ
⊢ a ^ (m + n) = a ^ m * a ^ n

State before:
a : ℝ
m n : ℕ
⊢ a ^ (m + n) = a ^ m * a ^ n
Tactic:
ring
State after:
no goals