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

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

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

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

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

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

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

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m k n : ℕ
ih : n + m ≃ n + k → m ≃ k
x✝ : step n + m ≃ step n + k
⊢ m ≃ k
Tactic:
apply ih
State after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m k n : ℕ
ih : n + m ≃ n + k → m ≃ k
x✝ : step n + m ≃ step n + k
⊢ n + m ≃ n + k

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