Theorem: Lean4Axiomatic.Natural.add_step (Lean4Axiomatic/Natural/Addition.lean)

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + step m ≃ step (n + m)
Tactic:
apply ind_on (motive := λ n => n + step m ≃ step (n + m)) n
State after:
case zero
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + step m ≃ step (0 + m)

case step
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 + step m ≃ step (m_1 + m) → step m_1 + step m ≃ step (step m_1 + m)

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + step m ≃ step (0 + m)
Tactic:
case zero =>
  show 0 + step m ≃ step (0 + m)
  calc
    0 + step m   ≃ _ := Addition.zero_add
    step m       ≃ _ := AA.subst₁ (Rel.symm Addition.zero_add)
    step (0 + m) ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 + step m ≃ step (m_1 + m) → step m_1 + step m ≃ step (step m_1 + m)
Tactic:
case step =>
  intro n (ih : n + step m ≃ step (n + m))
  show step n + step m ≃ step (step n + m)
  calc
    step n + step m     ≃ _ := Addition.step_add
    step (n + step m)   ≃ _ := AA.subst₁ ih
    step (step (n + m)) ≃ _ := AA.subst₁ (Rel.symm Addition.step_add)
    step (step n + m)   ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ 0 + step m ≃ step (0 + m)
Tactic:
calc
  0 + step m   ≃ _ := Addition.zero_add
  step m       ≃ _ := AA.subst₁ (Rel.symm Addition.zero_add)
  step (0 + m) ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), m_1 + step m ≃ step (m_1 + m) → step m_1 + step m ≃ step (step m_1 + m)
Tactic:
intro n (ih : n + step m ≃ step (n + m))
State after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
ih : n + step m ≃ step (n + m)
⊢ step n + step m ≃ step (step n + m)

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
ih : n + step m ≃ step (n + m)
⊢ step n + step m ≃ step (step n + m)
Tactic:
calc
  step n + step m     ≃ _ := Addition.step_add
  step (n + step m)   ≃ _ := AA.subst₁ ih
  step (step (n + m)) ≃ _ := AA.subst₁ (Rel.symm Addition.step_add)
  step (step n + m)   ≃ _ := Rel.refl
State after:
no goals