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
ℕ : 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
no goals