Theorem: Lean4Axiomatic.Natural.mul_split_zero (Lean4Axiomatic/Natural/Multiplication.lean)

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ 0 ↔ n ≃ 0 ∨ m ≃ 0
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ 0 → n ≃ 0 ∨ m ≃ 0

case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n ≃ 0 ∨ m ≃ 0 → n * m ≃ 0

State before:
case mp
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ 0 → n ≃ 0 ∨ m ≃ 0
Tactic:
apply cases_on (motive := λ x => x * m ≃ 0 → x ≃ 0 ∨ m ≃ 0) n
State after:
case mp.zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ 0 → 0 ≃ 0 ∨ m ≃ 0

case mp.step
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 * m ≃ 0 → step m_1 ≃ 0 ∨ m ≃ 0

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ 0 → 0 ≃ 0 ∨ m ≃ 0
Tactic:
case zero =>
  intro (_ : 0 * m ≃ 0)
  show 0 ≃ 0 ∨ m ≃ 0
  exact Or.inl Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
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 Or.inr
  show m ≃ 0
  have : n * m + m ≃ 0 := calc
    n * m + m  ≃ _ := Rel.symm step_mul
    step n * m ≃ _ := ‹step n * m ≃ 0›
    0          ≃ _ := Rel.refl
  have ⟨_, (_ : m ≃ 0)⟩ := zero_sum_split ‹n * m + m ≃ 0›
  exact ‹m ≃ 0›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ 0 → 0 ≃ 0 ∨ m ≃ 0
Tactic:
intro (_ : 0 * m ≃ 0)
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : 0 * m ≃ 0
⊢ 0 ≃ 0 ∨ m ≃ 0

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : 0 * m ≃ 0
⊢ 0 ≃ 0 ∨ m ≃ 0
Tactic:
exact Or.inl Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
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 ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ step n ≃ 0 ∨ m ≃ 0

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ step n ≃ 0 ∨ m ≃ 0
Tactic:
apply Or.inr
State after:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ m ≃ 0

State before:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ m ≃ 0
Tactic:
have : n * m + m ≃ 0 := calc
  n * m + m  ≃ _ := Rel.symm step_mul
  step n * m ≃ _ := ‹step n * m ≃ 0›
  0          ≃ _ := Rel.refl
State after:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
this : n * m + m ≃ 0
⊢ m ≃ 0

State before:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
this : n * m + m ≃ 0
⊢ m ≃ 0
Tactic:
have ⟨_, (_ : m ≃ 0)⟩ := zero_sum_split ‹n * m + m ≃ 0›
State after:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
this : n * m + m ≃ 0
left✝ : n * m ≃ 0
right✝ : m ≃ 0
⊢ m ≃ 0

State before:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
this : n * m + m ≃ 0
left✝ : n * m ≃ 0
right✝ : m ≃ 0
⊢ m ≃ 0
Tactic:
exact ‹m ≃ 0›
State after:
no goals

State before:
case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n ≃ 0 ∨ m ≃ 0 → n * m ≃ 0
Tactic:
intro (_ : n ≃ 0 ∨ m ≃ 0)
State after:
case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ n * m ≃ 0

State before:
case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ n * m ≃ 0
Tactic:
apply Or.elim ‹n ≃ 0 ∨ m ≃ 0›
State after:
case mpr.left
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ n ≃ 0 → n * m ≃ 0

case mpr.right
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ m ≃ 0 → n * m ≃ 0

State before:
case mpr.left
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ n ≃ 0 → n * m ≃ 0
Tactic:
intro (_ : n ≃ 0)
State after:
case mpr.left
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : n ≃ 0 ∨ m ≃ 0
x✝ : n ≃ 0
⊢ n * m ≃ 0

State before:
case mpr.left
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : n ≃ 0 ∨ m ≃ 0
x✝ : n ≃ 0
⊢ n * m ≃ 0
Tactic:
calc
  n * m ≃ _ := AA.substL ‹n ≃ 0›
  0 * m ≃ _ := zero_mul
  0     ≃ _ := Rel.refl
State after:
no goals

State before:
case mpr.right
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ m ≃ 0 → n * m ≃ 0
Tactic:
intro (_ : m ≃ 0)
State after:
case mpr.right
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : n ≃ 0 ∨ m ≃ 0
x✝ : m ≃ 0
⊢ n * m ≃ 0

State before:
case mpr.right
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : n ≃ 0 ∨ m ≃ 0
x✝ : m ≃ 0
⊢ n * m ≃ 0
Tactic:
calc
  n * m ≃ _ := AA.substR ‹m ≃ 0›
  n * 0 ≃ _ := mul_zero
  0     ≃ _ := Rel.refl
State after:
no goals