Theorem: HTPI.Example_6_3_2 (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:
by_induc
State after:
case Base_Case
a : ℝ
m : ℕ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

case Induction_Step
a : ℝ
m : ℕ
⊢ ∀ (n : ℕ), a ^ (m + n) = a ^ m * a ^ n → a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)

State before:
case Base_Case
a : ℝ
m : ℕ
⊢ a ^ (m + 0) = a ^ m * a ^ 0
Tactic:
show a ^ (m + 0) = a ^ m * a ^ 0 from
  calc a ^ (m + 0)
    _ = a ^ m := by rfl
    _ = a ^ m * 1 := (mul_one (a ^ m)).symm
    _ = a ^ m * a ^ 0 := by rfl
State after:
no goals

State before:
a : ℝ
m : ℕ
⊢ a ^ (m + 0) = a ^ m
Tactic:
rfl
State after:
no goals

State before:
a : ℝ
m : ℕ
⊢ a ^ m * 1 = a ^ m * a ^ 0
Tactic:
rfl
State after:
no goals

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

State before:
case Induction_Step
a : ℝ
m n : ℕ
⊢ a ^ (m + n) = a ^ m * a ^ n → a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
Tactic:
assume ih : a ^ (m + n) = a ^ m * a ^ n
State after:
case Induction_Step
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)

State before:
case Induction_Step
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)
Tactic:
show a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1) from
  calc a ^ (m + (n + 1))
    _ = a ^ ((m + n) + 1) := by rw [add_assoc]
    _ = a * a ^ (m + n) := by rfl
    _ = a * (a ^ m * a ^ n) := by rw [ih]
    _ = a ^ m * (a * a ^ n) := by
          rw [←mul_assoc, mul_comm a, mul_assoc]
    _ = a ^ m * (a ^ (n + 1)) := by rfl
State after:
no goals

State before:
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a ^ (m + (n + 1)) = a ^ (m + n + 1)
Tactic:
rw [add_assoc]
State after:
no goals

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

State before:
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a * a ^ (m + n) = a * (a ^ m * a ^ n)
Tactic:
rw [ih]
State after:
no goals

State before:
a : ℝ
m n : ℕ
ih : a ^ (m + n) = a ^ m * a ^ n
⊢ a * (a ^ m * a ^ n) = a ^ m * (a * a ^ n)
Tactic:
rw [←mul_assoc, mul_comm a, mul_assoc]
State after:
no goals

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