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

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

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ 0 * (m + k) ≃ 0 * m + 0 * k
Tactic:
case zero =>
  show 0 * (m + k) ≃ 0 * m + 0 * k
  calc
    0 * (m + k)   ≃ _ := zero_mul
    0             ≃ _ := Rel.symm Addition.zero_add
    0 + 0         ≃ _ := AA.substL (Rel.symm zero_mul)
    0 * m + 0     ≃ _ := AA.substR (Rel.symm zero_mul)
    0 * m + 0 * k ≃ _ := Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ 0 * (m + k) ≃ 0 * m + 0 * k
Tactic:
calc
  0 * (m + k)   ≃ _ := zero_mul
  0             ≃ _ := Rel.symm Addition.zero_add
  0 + 0         ≃ _ := AA.substL (Rel.symm zero_mul)
  0 * m + 0     ≃ _ := AA.substR (Rel.symm zero_mul)
  0 * m + 0 * k ≃ _ := Rel.refl
State after:
no goals

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

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