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

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

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

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

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 + m ≃ 0 → step m_1 ≃ 0 ∧ m ≃ 0
Tactic:
case step =>
  intro n (_ : step n + m ≃ 0)
  show step n ≃ 0 ∧ m ≃ 0
  apply False.elim
  show False
  have : step (n + m) ≃ step n + m := Rel.symm Addition.step_add
  have : step (n + m) ≃ 0 :=
    Rel.trans ‹step (n + m) ≃ step n + m› ‹step n + m ≃ 0›
  exact absurd ‹step (n + m) ≃ 0› step_neqv_zero
State after:
no goals

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

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : 0 + m ≃ 0
⊢ 0 ≃ 0 ∧ m ≃ 0
Tactic:
have : m ≃ 0 := Rel.trans (Rel.symm Addition.zero_add) ‹0 + m ≃ 0›
State after:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : 0 + m ≃ 0
this : m ≃ 0
⊢ 0 ≃ 0 ∧ m ≃ 0

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n m : ℕ
x✝ : 0 + m ≃ 0
this : m ≃ 0
⊢ 0 ≃ 0 ∧ m ≃ 0
Tactic:
exact And.intro Rel.refl ‹m ≃ 0›
State after:
no goals

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

State before:
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
⊢ step n ≃ 0 ∧ m ≃ 0
Tactic:
apply False.elim
State after:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
⊢ False

State before:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
⊢ False
Tactic:
have : step (n + m) ≃ step n + m := Rel.symm Addition.step_add
State after:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
this : step (n + m) ≃ step n + m
⊢ False

State before:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
this : step (n + m) ≃ step n + m
⊢ False
Tactic:
have : step (n + m) ≃ 0 :=
  Rel.trans ‹step (n + m) ≃ step n + m› ‹step n + m ≃ 0›
State after:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
this✝ : step (n + m) ≃ step n + m
this : step (n + m) ≃ 0
⊢ False

State before:
case h
ℕ : Type
inst✝² : Core ℕ
inst✝¹ : Induction ℕ
inst✝ : Addition ℕ
n✝ m n : ℕ
x✝ : step n + m ≃ 0
this✝ : step (n + m) ≃ step n + m
this : step (n + m) ≃ 0
⊢ False
Tactic:
exact absurd ‹step (n + m) ≃ 0› step_neqv_zero
State after:
no goals