Theorem: Lean4Axiomatic.Natural.pow_flatten (Lean4Axiomatic/Natural/Exponentiation.lean)

State before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ (x ^ n) ^ m ≃ x ^ (n * m)
Tactic:
apply ind_on m
State after:
case zero
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ (x ^ n) ^ 0 ≃ x ^ (n * 0)

case step
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ ∀ (m : ℕ), (x ^ n) ^ m ≃ x ^ (n * m) → (x ^ n) ^ step m ≃ x ^ (n * step m)

State before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ (x ^ n) ^ 0 ≃ x ^ (n * 0)
Tactic:
case zero =>
  show (x^n)^0 ≃ x^(n * 0)
  calc
    _ ≃ (x^n)^0   := Rel.refl
    _ ≃ 1         := pow_zero
    _ ≃ x^0       := Rel.symm pow_zero
    _ ≃ x^(n * 0) := pow_substR (Rel.symm mul_zero)
State after:
no goals

State before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ ∀ (m : ℕ), (x ^ n) ^ m ≃ x ^ (n * m) → (x ^ n) ^ step m ≃ x ^ (n * step m)
Tactic:
case step =>
  intro m' (ih : (x^n)^m' ≃ x^(n * m'))
  show (x^n)^(step m') ≃ x^(n * step m')
  calc
    _ ≃ (x^n)^(step m')  := Rel.refl
    _ ≃ (x^n)^m' * x^n   := pow_step
    _ ≃ x^(n * m') * x^n := AA.substL ih
    _ ≃ x^(n * m' + n)   := Rel.symm pow_compatL_add
    _ ≃ x^(n * step m')  := pow_substR (Rel.symm mul_step)
State after:
no goals

State before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ (x ^ n) ^ 0 ≃ x ^ (n * 0)
Tactic:
calc
  _ ≃ (x^n)^0   := Rel.refl
  _ ≃ 1         := pow_zero
  _ ≃ x^0       := Rel.symm pow_zero
  _ ≃ x^(n * 0) := pow_substR (Rel.symm mul_zero)
State after:
no goals

State before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m : ℕ
⊢ ∀ (m : ℕ), (x ^ n) ^ m ≃ x ^ (n * m) → (x ^ n) ^ step m ≃ x ^ (n * step m)
Tactic:
intro m' (ih : (x^n)^m' ≃ x^(n * m'))
State after:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m m' : ℕ
ih : (x ^ n) ^ m' ≃ x ^ (n * m')
⊢ (x ^ n) ^ step m' ≃ x ^ (n * step m')

State before:
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m m' : ℕ
ih : (x ^ n) ^ m' ≃ x ^ (n * m')
⊢ (x ^ n) ^ step m' ≃ x ^ (n * step m')
Tactic:
calc
  _ ≃ (x^n)^(step m')  := Rel.refl
  _ ≃ (x^n)^m' * x^n   := pow_step
  _ ≃ x^(n * m') * x^n := AA.substL ih
  _ ≃ x^(n * m' + n)   := Rel.symm pow_compatL_add
  _ ≃ x^(n * step m')  := pow_substR (Rel.symm mul_step)
State after:
no goals