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

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + 0 ≃ 0 + m ↔ n ≃ m
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + 0 ≃ 0 + m → n ≃ m

case mpr
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n ≃ m → n + 0 ≃ 0 + m

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n + 0 ≃ 0 + m → n ≃ m
Tactic:
case mp =>
  intro (_ : n + 0 ≃ 0 + m)
  show n ≃ m
  calc
    n     ≃ _ := Rel.symm AA.identR
    n + 0 ≃ _ := ‹n + 0 ≃ 0 + m›
    0 + m ≃ _ := AA.identL
    m     ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ n ≃ m → n + 0 ≃ 0 + m
Tactic:
case mpr =>
  intro (_ : n ≃ m)
  show n + 0 ≃ 0 + m
  calc
    n + 0 ≃ _ := AA.identR
    n     ≃ _ := ‹n ≃ m›
    m     ≃ _ := Rel.symm AA.identL
    0 + m ≃ _ := Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : n + 0 ≃ 0 + m
⊢ n ≃ m
Tactic:
calc
  n     ≃ _ := Rel.symm AA.identR
  n + 0 ≃ _ := ‹n + 0 ≃ 0 + m›
  0 + m ≃ _ := AA.identL
  m     ≃ _ := Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : n ≃ m
⊢ n + 0 ≃ 0 + m
Tactic:
calc
  n + 0 ≃ _ := AA.identR
  n     ≃ _ := ‹n ≃ m›
  m     ≃ _ := Rel.symm AA.identL
  0 + m ≃ _ := Rel.refl
State after:
no goals