Theorem: Lean4Axiomatic.Natural.pow_substL (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
x₁ x₂ : α
m : ℕ
⊢ x₁ ≃ x₂ → x₁ ^ m ≃ x₂ ^ m
Tactic:
intro (_ : x₁ ≃ x₂)
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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ m ≃ x₂ ^ 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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ m ≃ x₂ ^ m
Tactic:
apply ind_on (motive := λ y => x₁ ^ y ≃ x₂ ^ y) 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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ 0 ≃ x₂ ^ 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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ ∀ (m : ℕ), x₁ ^ m ≃ x₂ ^ m → x₁ ^ step m ≃ x₂ ^ 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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ 0 ≃ x₂ ^ 0
Tactic:
case zero =>
  show x₁ ^ 0 ≃ x₂ ^ 0
  calc
    _ ≃ x₁ ^ 0 := Rel.refl
    _ ≃ 1      := pow_zero
    _ ≃ x₂ ^ 0 := Rel.symm pow_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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ ∀ (m : ℕ), x₁ ^ m ≃ x₂ ^ m → x₁ ^ step m ≃ x₂ ^ step m
Tactic:
case step =>
  intro (m' : ℕ) (ih : x₁ ^ m' ≃ x₂ ^ m')
  show x₁ ^ step m' ≃ x₂ ^ step m'
  calc
    _ ≃ x₁ ^ step m' := Rel.refl
    _ ≃ x₁ ^ m' * x₁ := pow_step
    _ ≃ x₂ ^ m' * x₁ := AA.substL ih
    _ ≃ x₂ ^ m' * x₂ := AA.substR ‹x₁ ≃ x₂›
    _ ≃ x₂ ^ step m' := Rel.symm pow_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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ x₁ ^ 0 ≃ x₂ ^ 0
Tactic:
calc
  _ ≃ x₁ ^ 0 := Rel.refl
  _ ≃ 1      := pow_zero
  _ ≃ x₂ ^ 0 := Rel.symm pow_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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
⊢ ∀ (m : ℕ), x₁ ^ m ≃ x₂ ^ m → x₁ ^ step m ≃ x₂ ^ step m
Tactic:
intro (m' : ℕ) (ih : x₁ ^ m' ≃ x₂ ^ 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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
m' : ℕ
ih : x₁ ^ m' ≃ x₂ ^ m'
⊢ x₁ ^ step m' ≃ x₂ ^ 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
x₁ x₂ : α
m : ℕ
x✝ : x₁ ≃ x₂
m' : ℕ
ih : x₁ ^ m' ≃ x₂ ^ m'
⊢ x₁ ^ step m' ≃ x₂ ^ step m'
Tactic:
calc
  _ ≃ x₁ ^ step m' := Rel.refl
  _ ≃ x₁ ^ m' * x₁ := pow_step
  _ ≃ x₂ ^ m' * x₁ := AA.substL ih
  _ ≃ x₂ ^ m' * x₂ := AA.substR ‹x₁ ≃ x₂›
  _ ≃ x₂ ^ step m' := Rel.symm pow_step
State after:
no goals