Theorem: Nat.sqPow_eq_gpow (Algdata/Data/Nat/Pow.lean)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
⊢ ∀ (a : α) (n : Nat), sqPow a n = gpow a n
Tactic:
intro a n
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
n : Nat
⊢ sqPow a n = gpow a n

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
n : Nat
⊢ sqPow a n = gpow a n
Tactic:
unfold sqPow
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
n : Nat
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) n = gpow a n

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
n : Nat
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) n = gpow a n
Tactic:
induction n using recBase2 generalizing a
State after:
case zero
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 0 = gpow a 0

case one
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 1 = gpow a 1

case div2
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n✝ : Nat
a✝ : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n✝ / 2 + 1) = gpow a (n✝ / 2 + 1)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n✝ + 2) = gpow a (n✝ + 2)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 0 = gpow a 0
Tactic:
case zero => rfl
State after:
no goals

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 1 = gpow a 1
Tactic:
case one =>
  rw [recBase2_one]
  exact (mul_one a).symm
State after:
no goals

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n + 2) = gpow a (n + 2)
Tactic:
case div2 n h_ind =>
  rw [recBase2_div2]
  rw [h_ind a]
  by_cases n % 2 = 1
  case pos hodd =>
    rw [if_pos hodd]
    conv =>
      lhs; change gpow a (n/2 + 2) * gpow a (n/2 + 1)
      rw [←gpow_add one_mul assoc]
    apply congrArg
    conv =>
      lhs; rw [Nat.add_assoc, ←Nat.add_assoc 2 (n/2) 1, Nat.add_comm 2, Nat.add_assoc _ 2 1, ←Nat.add_assoc]
      rw [←Nat.mul_two, Nat.mul_comm, Nat.add_comm 2 1, ←Nat.add_assoc, ←hodd]
      rw [Nat.div_add_mod]
  case neg heven =>
    rw [if_neg heven]
    rw [←gpow_add one_mul assoc]
    have : n % 2 = 0 := Or.resolve_right (Nat.mod_two_eq_zero_or_one n) heven
    apply congrArg
    conv =>
      lhs; rw [Nat.add_assoc, ←Nat.add_assoc 1, Nat.add_comm 1, Nat.add_assoc _ 1 1, ←Nat.add_assoc]
      rw [←Nat.mul_two, Nat.mul_comm, ←Nat.add_zero (2*(n/2)), ←this]
      rw [Nat.div_add_mod]
State after:
no goals

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 0 = gpow a 0
Tactic:
rfl
State after:
no goals

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) 1 = gpow a 1
Tactic:
rw [recBase2_one]
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
⊢ a = gpow a 1

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
⊢ a = gpow a 1
Tactic:
exact (mul_one a).symm
State after:
no goals

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
⊢ recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n + 2) = gpow a (n + 2)
Tactic:
rw [recBase2_div2]
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
⊢ (if n % 2 = 1 then
      a * recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) *
        recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1)
    else
      recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) *
        recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1)) =
    gpow a (n + 2)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
⊢ (if n % 2 = 1 then
      a * recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) *
        recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1)
    else
      recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) *
        recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
rw [h_ind a]
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
by_cases n % 2 = 1
State after:
case pos
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
h✝ : n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)

case neg
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
h✝ : ¬n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
case pos hodd =>
  rw [if_pos hodd]
  conv =>
    lhs; change gpow a (n/2 + 2) * gpow a (n/2 + 1)
    rw [←gpow_add one_mul assoc]
  apply congrArg
  conv =>
    lhs; rw [Nat.add_assoc, ←Nat.add_assoc 2 (n/2) 1, Nat.add_comm 2, Nat.add_assoc _ 2 1, ←Nat.add_assoc]
    rw [←Nat.mul_two, Nat.mul_comm, Nat.add_comm 2 1, ←Nat.add_assoc, ←hodd]
    rw [Nat.div_add_mod]
State after:
no goals

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
case neg heven =>
  rw [if_neg heven]
  rw [←gpow_add one_mul assoc]
  have : n % 2 = 0 := Or.resolve_right (Nat.mod_two_eq_zero_or_one n) heven
  apply congrArg
  conv =>
    lhs; rw [Nat.add_assoc, ←Nat.add_assoc 1, Nat.add_comm 1, Nat.add_assoc _ 1 1, ←Nat.add_assoc]
    rw [←Nat.mul_two, Nat.mul_comm, ←Nat.add_zero (2*(n/2)), ←this]
    rw [Nat.div_add_mod]
State after:
no goals

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
rw [if_pos hodd]
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) = gpow a (n + 2)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) = gpow a (n + 2)
Tactic:
conv =>
  lhs; change gpow a (n/2 + 2) * gpow a (n/2 + 1)
  rw [←gpow_add one_mul assoc]
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ gpow a (n / 2 + 2 + (n / 2 + 1)) = gpow a (n + 2)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ gpow a (n / 2 + 2 + (n / 2 + 1)) = gpow a (n + 2)
Tactic:
apply congrArg
State after:
case h
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ n / 2 + 2 + (n / 2 + 1) = n + 2

State before:
case h
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
hodd : n % 2 = 1
⊢ n / 2 + 2 + (n / 2 + 1) = n + 2
Tactic:
conv =>
  lhs; rw [Nat.add_assoc, ←Nat.add_assoc 2 (n/2) 1, Nat.add_comm 2, Nat.add_assoc _ 2 1, ←Nat.add_assoc]
  rw [←Nat.mul_two, Nat.mul_comm, Nat.add_comm 2 1, ←Nat.add_assoc, ←hodd]
  rw [Nat.div_add_mod]
State after:
no goals

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ (if n % 2 = 1 then a * gpow a (n / 2 + 1) * gpow a (n / 2 + 1) else gpow a (n / 2 + 1) * gpow a (n / 2 + 1)) =
    gpow a (n + 2)
Tactic:
rw [if_neg heven]
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ gpow a (n / 2 + 1) * gpow a (n / 2 + 1) = gpow a (n + 2)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ gpow a (n / 2 + 1) * gpow a (n / 2 + 1) = gpow a (n + 2)
Tactic:
rw [←gpow_add one_mul assoc]
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ gpow a (n / 2 + 1 + (n / 2 + 1)) = gpow a (n + 2)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
⊢ gpow a (n / 2 + 1 + (n / 2 + 1)) = gpow a (n + 2)
Tactic:
have : n % 2 = 0 := Or.resolve_right (Nat.mod_two_eq_zero_or_one n) heven
State after:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
this : n % 2 = 0
⊢ gpow a (n / 2 + 1 + (n / 2 + 1)) = gpow a (n + 2)

State before:
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
this : n % 2 = 0
⊢ gpow a (n / 2 + 1 + (n / 2 + 1)) = gpow a (n + 2)
Tactic:
apply congrArg
State after:
case h
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
this : n % 2 = 0
⊢ n / 2 + 1 + (n / 2 + 1) = n + 2

State before:
case h
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
n : Nat
h_ind : ∀ (a : α), recBase2 1 a (fun n x => if n % 2 = 1 then a * x * x else x * x) (n / 2 + 1) = gpow a (n / 2 + 1)
a : α
heven : ¬n % 2 = 1
this : n % 2 = 0
⊢ n / 2 + 1 + (n / 2 + 1) = n + 2
Tactic:
conv =>
  lhs; rw [Nat.add_assoc, ←Nat.add_assoc 1, Nat.add_comm 1, Nat.add_assoc _ 1 1, ←Nat.add_assoc]
  rw [←Nat.mul_two, Nat.mul_comm, ←Nat.add_zero (2*(n/2)), ←this]
  rw [Nat.div_add_mod]
State after:
no goals