Theorem: Lean4Axiomatic.Natural.pow_substR (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 : α
n₁ n₂ : ℕ
⊢ n₁ ≃ n₂ → x ^ n₁ ≃ x ^ n₂
Tactic:
apply ind_on (motive := λ k => ∀ {j}, k ≃ j → x ^ k ≃ x ^ j) n₁
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 : α
n₁ n₂ : ℕ
⊢ ∀ {j : ℕ}, 0 ≃ j → x ^ 0 ≃ x ^ j

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 : α
n₁ n₂ : ℕ
⊢ ∀ (m : ℕ), (∀ {j : ℕ}, m ≃ j → x ^ m ≃ x ^ j) → ∀ {j : ℕ}, step m ≃ j → x ^ step m ≃ x ^ j

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 : α
n₁ n₂ : ℕ
⊢ ∀ {j : ℕ}, 0 ≃ j → x ^ 0 ≃ x ^ j
Tactic:
case zero =>
  intro (n₂ : ℕ)
  show 0 ≃ n₂ → x ^ 0 ≃ x ^ n₂
  apply cases_on (motive := λ j => 0 ≃ j → x ^ 0 ≃ x ^ j) n₂
  case zero =>
    intro (_ : (0 : ℕ) ≃ 0)
    show x ^ 0 ≃ x ^ 0
    exact Rel.refl
  case step =>
    intro (n₂' : ℕ) (_ : 0 ≃ step n₂')
    show x ^ 0 ≃ x ^ step n₂'
    exact absurd ‹0 ≃ step n₂'› (Rel.symm step_neqv_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 : α
n₁ n₂ : ℕ
⊢ ∀ (m : ℕ), (∀ {j : ℕ}, m ≃ j → x ^ m ≃ x ^ j) → ∀ {j : ℕ}, step m ≃ j → x ^ step m ≃ x ^ j
Tactic:
case step =>
  intro (n₁' : ℕ) (ih : ∀ {j}, n₁' ≃ j → x ^ n₁' ≃ x ^ j) (n₂ : ℕ)
  show step n₁' ≃ n₂ → x ^ step n₁' ≃ x ^ n₂
  apply cases_on (motive := λ j => step n₁' ≃ j → x ^ step n₁' ≃ x ^ j) n₂
  case zero =>
    intro (_ : step n₁' ≃ 0)
    show x ^ step n₁' ≃ x ^ 0
    exact absurd ‹step n₁' ≃ 0› step_neqv_zero
  case step =>
    intro (n₂' : ℕ) (_ : step n₁' ≃ step n₂')
    show x ^ step n₁' ≃ x ^ step n₂'
    have : n₁' ≃ n₂' := AA.inject ‹step n₁' ≃ step n₂'›
    calc
      _ ≃ x ^ step n₁' := Rel.refl
      _ ≃ x ^ n₁' * x  := pow_step
      _ ≃ x ^ n₂' * x  := AA.substL (ih ‹n₁' ≃ n₂'›)
      _ ≃ x ^ step n₂' := 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 : α
n₁ n₂ : ℕ
⊢ ∀ {j : ℕ}, 0 ≃ j → x ^ 0 ≃ x ^ j
Tactic:
intro (n₂ : ℕ)
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 : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ n₂ → x ^ 0 ≃ x ^ n₂

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 : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ n₂ → x ^ 0 ≃ x ^ n₂
Tactic:
apply cases_on (motive := λ j => 0 ≃ j → x ^ 0 ≃ x ^ j) n₂
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 : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ 0 → 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 : α
n₁ n₂✝ n₂ : ℕ
⊢ ∀ (m : ℕ), 0 ≃ step m → x ^ 0 ≃ 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 : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ 0 → x ^ 0 ≃ x ^ 0
Tactic:
case zero =>
  intro (_ : (0 : ℕ) ≃ 0)
  show x ^ 0 ≃ x ^ 0
  exact Rel.refl
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 : α
n₁ n₂✝ n₂ : ℕ
⊢ ∀ (m : ℕ), 0 ≃ step m → x ^ 0 ≃ x ^ step m
Tactic:
case step =>
  intro (n₂' : ℕ) (_ : 0 ≃ step n₂')
  show x ^ 0 ≃ x ^ step n₂'
  exact absurd ‹0 ≃ step n₂'› (Rel.symm step_neqv_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 : α
n₁ n₂✝ n₂ : ℕ
⊢ 0 ≃ 0 → x ^ 0 ≃ x ^ 0
Tactic:
intro (_ : (0 : ℕ) ≃ 0)
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 : α
n₁ n₂✝ n₂ : ℕ
x✝ : 0 ≃ 0
⊢ x ^ 0 ≃ x ^ 0

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 : α
n₁ n₂✝ n₂ : ℕ
x✝ : 0 ≃ 0
⊢ x ^ 0 ≃ x ^ 0
Tactic:
exact Rel.refl
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 : α
n₁ n₂✝ n₂ : ℕ
⊢ ∀ (m : ℕ), 0 ≃ step m → x ^ 0 ≃ x ^ step m
Tactic:
intro (n₂' : ℕ) (_ : 0 ≃ step n₂')
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 : α
n₁ n₂✝ n₂ n₂' : ℕ
x✝ : 0 ≃ step n₂'
⊢ x ^ 0 ≃ x ^ step n₂'

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 : α
n₁ n₂✝ n₂ n₂' : ℕ
x✝ : 0 ≃ step n₂'
⊢ x ^ 0 ≃ x ^ step n₂'
Tactic:
exact absurd ‹0 ≃ step n₂'› (Rel.symm step_neqv_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 : α
n₁ n₂ : ℕ
⊢ ∀ (m : ℕ), (∀ {j : ℕ}, m ≃ j → x ^ m ≃ x ^ j) → ∀ {j : ℕ}, step m ≃ j → x ^ step m ≃ x ^ j
Tactic:
intro (n₁' : ℕ) (ih : ∀ {j}, n₁' ≃ j → x ^ n₁' ≃ x ^ j) (n₂ : ℕ)
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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ n₂ → x ^ step n₁' ≃ x ^ n₂

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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ n₂ → x ^ step n₁' ≃ x ^ n₂
Tactic:
apply cases_on (motive := λ j => step n₁' ≃ j → x ^ step n₁' ≃ x ^ j) n₂
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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ 0 → x ^ step n₁' ≃ 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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ ∀ (m : ℕ), step n₁' ≃ step m → x ^ step n₁' ≃ 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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ 0 → x ^ step n₁' ≃ x ^ 0
Tactic:
case zero =>
  intro (_ : step n₁' ≃ 0)
  show x ^ step n₁' ≃ x ^ 0
  exact absurd ‹step n₁' ≃ 0› step_neqv_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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ ∀ (m : ℕ), step n₁' ≃ step m → x ^ step n₁' ≃ x ^ step m
Tactic:
case step =>
  intro (n₂' : ℕ) (_ : step n₁' ≃ step n₂')
  show x ^ step n₁' ≃ x ^ step n₂'
  have : n₁' ≃ n₂' := AA.inject ‹step n₁' ≃ step n₂'›
  calc
    _ ≃ x ^ step n₁' := Rel.refl
    _ ≃ x ^ n₁' * x  := pow_step
    _ ≃ x ^ n₂' * x  := AA.substL (ih ‹n₁' ≃ n₂'›)
    _ ≃ x ^ step n₂' := 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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ step n₁' ≃ 0 → x ^ step n₁' ≃ x ^ 0
Tactic:
intro (_ : step n₁' ≃ 0)
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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
x✝ : step n₁' ≃ 0
⊢ x ^ step n₁' ≃ x ^ 0

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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
x✝ : step n₁' ≃ 0
⊢ x ^ step n₁' ≃ x ^ 0
Tactic:
exact absurd ‹step n₁' ≃ 0› step_neqv_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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ : ℕ
⊢ ∀ (m : ℕ), step n₁' ≃ step m → x ^ step n₁' ≃ x ^ step m
Tactic:
intro (n₂' : ℕ) (_ : step n₁' ≃ step n₂')
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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'

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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'
Tactic:
have : n₁' ≃ n₂' := AA.inject ‹step n₁' ≃ step n₂'›
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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
this : n₁' ≃ n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'

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 : α
n₁ n₂✝ n₁' : ℕ
ih : ∀ {j : ℕ}, n₁' ≃ j → x ^ n₁' ≃ x ^ j
n₂ n₂' : ℕ
x✝ : step n₁' ≃ step n₂'
this : n₁' ≃ n₂'
⊢ x ^ step n₁' ≃ x ^ step n₂'
Tactic:
calc
  _ ≃ x ^ step n₁' := Rel.refl
  _ ≃ x ^ n₁' * x  := pow_step
  _ ≃ x ^ n₂' * x  := AA.substL (ih ‹n₁' ≃ n₂'›)
  _ ≃ x ^ step n₂' := Rel.symm pow_step
State after:
no goals