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

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

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

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

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