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

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

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ ∀ (y : ℕ), 0 ≃ y → 0 * m ≃ y * m
Tactic:
case zero =>
  intro n₂
  show 0 ≃ n₂ → 0 * m ≃ n₂ * m
  apply cases_on (motive := λ y => 0 ≃ y → 0 * m ≃ y * m)
  case zero =>
    intro (_ : 0 ≃ (0 : ℕ))
    show 0 * m ≃ 0 * m
    exact Rel.refl
  case step =>
    intro n₂ (_ : 0 ≃ step n₂)
    exact absurd (Rel.symm ‹0 ≃ step n₂›) step_neqv_zero
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ ∀ (m_1 : ℕ), (∀ (y : ℕ), m_1 ≃ y → m_1 * m ≃ y * m) → ∀ (y : ℕ), step m_1 ≃ y → step m_1 * m ≃ y * m
Tactic:
case step =>
  intro n₁ (ih : ∀ y, n₁ ≃ y → n₁ * m ≃ y * m) n₂
  show step n₁ ≃ n₂ → step n₁ * m ≃ n₂ * m
  apply cases_on (motive := λ y => step n₁ ≃ y → step n₁ * m ≃ y * m)
  case zero =>
    intro (_ : step n₁ ≃ 0)
    exact absurd ‹step n₁ ≃ 0› step_neqv_zero
  case step =>
    intro n₂ (_ : step n₁ ≃ step n₂)
    show step n₁ * m ≃ step n₂ * m
    have : n₁ ≃ n₂ := AA.inject ‹step n₁ ≃ step n₂›
    have : n₁ * m ≃ n₂ * m := ih n₂ ‹n₁ ≃ n₂›
    calc
      step n₁ * m  ≃ _ := step_mul
      (n₁ * m) + m ≃ _ := AA.substL ‹n₁ * m ≃ n₂ * m›
      (n₂ * m) + m ≃ _ := Rel.symm step_mul
      step n₂ * m  ≃ _ := Rel.refl
State after:
no goals

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

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

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

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂✝ m n₂ : ℕ
⊢ ∀ (m_1 : ℕ), 0 ≃ step m_1 → 0 * m ≃ step m_1 * m
Tactic:
case step =>
  intro n₂ (_ : 0 ≃ step n₂)
  exact absurd (Rel.symm ‹0 ≃ step n₂›) step_neqv_zero
State after:
no goals

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

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

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂✝¹ m n₂✝ n₂ : ℕ
x✝ : 0 ≃ step n₂
⊢ 0 * m ≃ step n₂ * m
Tactic:
exact absurd (Rel.symm ‹0 ≃ step n₂›) step_neqv_zero
State after:
no goals

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂ : ℕ
⊢ step n₁ ≃ n₂ → step n₁ * m ≃ n₂ * m
Tactic:
apply cases_on (motive := λ y => step n₁ ≃ y → step n₁ * m ≃ y * m)
State after:
case zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂ : ℕ
⊢ step n₁ ≃ 0 → step n₁ * m ≃ 0 * m

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂ : ℕ
⊢ step n₁ ≃ 0 → step n₁ * m ≃ 0 * m
Tactic:
case zero =>
  intro (_ : step n₁ ≃ 0)
  exact absurd ‹step n₁ ≃ 0› step_neqv_zero
State after:
no goals

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

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂ : ℕ
x✝ : step n₁ ≃ 0
⊢ step n₁ * m ≃ 0 * m
Tactic:
exact absurd ‹step n₁ ≃ 0› step_neqv_zero
State after:
no goals

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝¹ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂✝ n₂ : ℕ
x✝ : step n₁ ≃ step n₂
⊢ step n₁ * m ≃ step n₂ * m
Tactic:
have : n₁ ≃ n₂ := AA.inject ‹step n₁ ≃ step n₂›
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝¹ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂✝ n₂ : ℕ
x✝ : step n₁ ≃ step n₂
this : n₁ ≃ n₂
⊢ step n₁ * m ≃ step n₂ * m

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝¹ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂✝ n₂ : ℕ
x✝ : step n₁ ≃ step n₂
this : n₁ ≃ n₂
⊢ step n₁ * m ≃ step n₂ * m
Tactic:
have : n₁ * m ≃ n₂ * m := ih n₂ ‹n₁ ≃ n₂›
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝¹ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂✝ n₂ : ℕ
x✝ : step n₁ ≃ step n₂
this✝ : n₁ ≃ n₂
this : n₁ * m ≃ n₂ * m
⊢ step n₁ * m ≃ step n₂ * m

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁✝ n₂✝¹ m n₁ : ℕ
ih : ∀ (y : ℕ), n₁ ≃ y → n₁ * m ≃ y * m
n₂✝ n₂ : ℕ
x✝ : step n₁ ≃ step n₂
this✝ : n₁ ≃ n₂
this : n₁ * m ≃ n₂ * m
⊢ step n₁ * m ≃ step n₂ * m
Tactic:
calc
  step n₁ * m  ≃ _ := step_mul
  (n₁ * m) + m ≃ _ := AA.substL ‹n₁ * m ≃ n₂ * m›
  (n₂ * m) + m ≃ _ := Rel.symm step_mul
  step n₂ * m  ≃ _ := Rel.refl
State after:
no goals