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

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

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ 0 * 0 ≃ 0
Tactic:
case zero =>
  show 0 * 0 ≃ 0
  exact zero_mul
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ ∀ (m : ℕ), m * 0 ≃ 0 → step m * 0 ≃ 0
Tactic:
case step =>
  intro n (ih : n * 0 ≃ 0)
  show step n * 0 ≃ 0
  calc
    step n * 0 ≃ _ := step_mul
    n * 0 + 0  ≃ _ := AA.substL ih
    0 + 0      ≃ _ := Addition.zero_add
    0          ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ 0 * 0 ≃ 0
Tactic:
exact zero_mul
State after:
no goals

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ n : ℕ
ih : n * 0 ≃ 0
⊢ step n * 0 ≃ 0
Tactic:
calc
  step n * 0 ≃ _ := step_mul
  n * 0 + 0  ≃ _ := AA.substL ih
  0 + 0      ≃ _ := Addition.zero_add
  0          ≃ _ := Rel.refl
State after:
no goals