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

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

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ m * 0
Tactic:
case zero =>
  show 0 * m ≃ m * 0
  calc
    0 * m ≃ _ := zero_mul
    0     ≃ _ := Rel.symm mul_zero
    m * 0 ≃ _ := 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 : ℕ), m_1 * m ≃ m * m_1 → step m_1 * m ≃ m * step m_1
Tactic:
case step =>
  intro n (ih : n * m ≃ m * n)
  show step n * m ≃ m * step n
  calc
    step n * m ≃ _ := step_mul
    n * m + m  ≃ _ := AA.substL ih
    m * n + m  ≃ _ := Rel.symm mul_step
    m * step n ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ m * 0
Tactic:
calc
  0 * m ≃ _ := zero_mul
  0     ≃ _ := Rel.symm mul_zero
  m * 0 ≃ _ := 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 : ℕ), m_1 * m ≃ m * m_1 → step m_1 * m ≃ m * step m_1
Tactic:
intro n (ih : n * m ≃ m * n)
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
ih : n * m ≃ m * n
⊢ step n * m ≃ m * step n

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