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

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

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

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

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

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

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

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