internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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 : ℕ))
Proof 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
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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₂)
Proof 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
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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₂
Proof 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
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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₂)
Proof 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
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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₂›
Proof 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
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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₂›
Proof 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
Theorem: Lean4Axiomatic.Natural.subst_mul_eq
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ 0 ↔ n ≃ 0 ∨ m ≃ 0
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ 0 → n ≃ 0 ∨ m ≃ 0

case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n ≃ 0 ∨ m ≃ 0 → n * m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case mp
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ 0 → n ≃ 0 ∨ m ≃ 0
Tactic:
apply cases_on (motive := λ x => x * m ≃ 0 → x ≃ 0 ∨ m ≃ 0) n
Proof state after:
case mp.zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ 0 → 0 ≃ 0 ∨ m ≃ 0

case mp.step
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 * m ≃ 0 → step m_1 ≃ 0 ∨ m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ 0 → 0 ≃ 0 ∨ m ≃ 0
Tactic:
case zero =>
  intro (_ : 0 * m ≃ 0)
  show 0 ≃ 0 ∨ m ≃ 0
  exact Or.inl Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 * m ≃ 0 → step m_1 ≃ 0 ∨ m ≃ 0
Tactic:
case step =>
  intro n (_ : step n * m ≃ 0)
  show step n ≃ 0 ∨ m ≃ 0
  apply Or.inr
  show m ≃ 0
  have : n * m + m ≃ 0 := calc
    n * m + m  ≃ _ := Rel.symm step_mul
    step n * m ≃ _ := ‹step n * m ≃ 0›
    0          ≃ _ := Rel.refl
  have ⟨_, (_ : m ≃ 0)⟩ := zero_sum_split ‹n * m + m ≃ 0›
  exact ‹m ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ 0 * m ≃ 0 → 0 ≃ 0 ∨ m ≃ 0
Tactic:
intro (_ : 0 * m ≃ 0)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : 0 * m ≃ 0
⊢ 0 ≃ 0 ∨ m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : 0 * m ≃ 0
⊢ 0 ≃ 0 ∨ m ≃ 0
Tactic:
exact Or.inl Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ ∀ (m_1 : ℕ), step m_1 * m ≃ 0 → step m_1 ≃ 0 ∨ m ≃ 0
Tactic:
intro n (_ : step n * m ≃ 0)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ step n ≃ 0 ∨ m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ step n ≃ 0 ∨ m ≃ 0
Tactic:
apply Or.inr
Proof state after:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
⊢ m ≃ 0
Tactic:
have : n * m + m ≃ 0 := calc
  n * m + m  ≃ _ := Rel.symm step_mul
  step n * m ≃ _ := ‹step n * m ≃ 0›
  0          ≃ _ := Rel.refl
Proof state after:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
this : n * m + m ≃ 0
⊢ m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
this : n * m + m ≃ 0
⊢ m ≃ 0
Tactic:
have ⟨_, (_ : m ≃ 0)⟩ := zero_sum_split ‹n * m + m ≃ 0›
Proof state after:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
this : n * m + m ≃ 0
left✝ : n * m ≃ 0
right✝ : m ≃ 0
⊢ m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case h
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m n : ℕ
x✝ : step n * m ≃ 0
this : n * m + m ≃ 0
left✝ : n * m ≃ 0
right✝ : m ≃ 0
⊢ m ≃ 0
Tactic:
exact ‹m ≃ 0›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n ≃ 0 ∨ m ≃ 0 → n * m ≃ 0
Tactic:
intro (_ : n ≃ 0 ∨ m ≃ 0)
Proof state after:
case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ n * m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ n * m ≃ 0
Tactic:
apply Or.elim ‹n ≃ 0 ∨ m ≃ 0›
Proof state after:
case mpr.left
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ n ≃ 0 → n * m ≃ 0

case mpr.right
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ m ≃ 0 → n * m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case mpr.left
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ n ≃ 0 → n * m ≃ 0
Tactic:
intro (_ : n ≃ 0)
Proof state after:
case mpr.left
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : n ≃ 0 ∨ m ≃ 0
x✝ : n ≃ 0
⊢ n * m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case mpr.left
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : n ≃ 0 ∨ m ≃ 0
x✝ : n ≃ 0
⊢ n * m ≃ 0
Tactic:
calc
  n * m ≃ _ := AA.substL ‹n ≃ 0›
  0 * m ≃ _ := zero_mul
  0     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case mpr.right
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n ≃ 0 ∨ m ≃ 0
⊢ m ≃ 0 → n * m ≃ 0
Tactic:
intro (_ : m ≃ 0)
Proof state after:
case mpr.right
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : n ≃ 0 ∨ m ≃ 0
x✝ : m ≃ 0
⊢ n * m ≃ 0
Theorem: Lean4Axiomatic.Natural.mul_split_zero
Proof state before:
case mpr.right
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : n ≃ 0 ∨ m ≃ 0
x✝ : m ≃ 0
⊢ n * m ≃ 0
Tactic:
calc
  n * m ≃ _ := AA.substR ‹m ≃ 0›
  n * 0 ≃ _ := mul_zero
  0     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ Positive (n * m) ↔ Positive n ∧ Positive m
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ Positive (n * m) → Positive n ∧ Positive m

case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ Positive n ∧ Positive m → Positive (n * m)
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ Positive (n * m) → Positive n ∧ Positive m
Tactic:
case mp =>
  intro (_ : Positive (n * m))
  show Positive n ∧ Positive m
  have : n * m ≄ 0 := positive_defn.mp ‹Positive (n * m)›
  have : ¬(n ≃ 0 ∨ m ≃ 0) := mt mul_split_zero.mpr this
  have (And.intro (_ : n ≄ 0) (_ : m ≄ 0)) :=
    Logic.not_or_iff_and_not.mp this
  have : Positive n := positive_defn.mpr ‹n ≄ 0›
  have : Positive m := positive_defn.mpr ‹m ≄ 0›
  exact And.intro ‹Positive n› ‹Positive m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ Positive n ∧ Positive m → Positive (n * m)
Tactic:
case mpr =>
  intro (And.intro (_ : Positive n) (_ : Positive m))
  show Positive (n * m)
  have : n ≄ 0 := positive_defn.mp ‹Positive n›
  have : m ≄ 0 := positive_defn.mp ‹Positive m›
  have : n ≄ 0 ∧ m ≄ 0 := And.intro ‹n ≄ 0› ‹m ≄ 0›
  have : ¬(n ≃ 0 ∨ m ≃ 0) := Logic.not_or_iff_and_not.mpr this
  have : n * m ≄ 0 := mt mul_split_zero.mp this
  have : Positive (n * m) := positive_defn.mpr this
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ Positive (n * m) → Positive n ∧ Positive m
Tactic:
intro (_ : Positive (n * m))
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
⊢ Positive n ∧ Positive m
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
⊢ Positive n ∧ Positive m
Tactic:
have : n * m ≄ 0 := positive_defn.mp ‹Positive (n * m)›
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this : n * m ≄ 0
⊢ Positive n ∧ Positive m
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this : n * m ≄ 0
⊢ Positive n ∧ Positive m
Tactic:
have : ¬(n ≃ 0 ∨ m ≃ 0) := mt mul_split_zero.mpr this
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝ : n * m ≄ 0
this : ¬(n ≃ 0 ∨ m ≃ 0)
⊢ Positive n ∧ Positive m
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝ : n * m ≄ 0
this : ¬(n ≃ 0 ∨ m ≃ 0)
⊢ Positive n ∧ Positive m
Tactic:
have (And.intro (_ : n ≄ 0) (_ : m ≄ 0)) :=
  Logic.not_or_iff_and_not.mp this
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝ : n * m ≄ 0
this : ¬(n ≃ 0 ∨ m ≃ 0)
left✝ : n ≄ 0
right✝ : m ≄ 0
⊢ Positive n ∧ Positive m
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝ : n * m ≄ 0
this : ¬(n ≃ 0 ∨ m ≃ 0)
left✝ : n ≄ 0
right✝ : m ≄ 0
⊢ Positive n ∧ Positive m
Tactic:
have : Positive n := positive_defn.mpr ‹n ≄ 0›
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝¹ : n * m ≄ 0
this✝ : ¬(n ≃ 0 ∨ m ≃ 0)
left✝ : n ≄ 0
right✝ : m ≄ 0
this : Positive n
⊢ Positive n ∧ Positive m
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝¹ : n * m ≄ 0
this✝ : ¬(n ≃ 0 ∨ m ≃ 0)
left✝ : n ≄ 0
right✝ : m ≄ 0
this : Positive n
⊢ Positive n ∧ Positive m
Tactic:
have : Positive m := positive_defn.mpr ‹m ≄ 0›
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝² : n * m ≄ 0
this✝¹ : ¬(n ≃ 0 ∨ m ≃ 0)
left✝ : n ≄ 0
right✝ : m ≄ 0
this✝ : Positive n
this : Positive m
⊢ Positive n ∧ Positive m
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : Positive (n * m)
this✝² : n * m ≄ 0
this✝¹ : ¬(n ≃ 0 ∨ m ≃ 0)
left✝ : n ≄ 0
right✝ : m ≄ 0
this✝ : Positive n
this : Positive m
⊢ Positive n ∧ Positive m
Tactic:
exact And.intro ‹Positive n› ‹Positive m›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ Positive n ∧ Positive m → Positive (n * m)
Tactic:
intro (And.intro (_ : Positive n) (_ : Positive m))
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
left✝ : Positive n
right✝ : Positive m
⊢ Positive (n * m)
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
left✝ : Positive n
right✝ : Positive m
⊢ Positive (n * m)
Tactic:
have : n ≄ 0 := positive_defn.mp ‹Positive n›
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
left✝ : Positive n
right✝ : Positive m
this : n ≄ 0
⊢ Positive (n * m)
Theorem: Lean4Axiomatic.Natural.mul_preserves_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
left✝ : Positive n
right✝ : Positive m
this : n ≄ 0
⊢ Positive (n * m)
Tactic:
have : m ≄ 0 := positive_defn.mp ‹Positive m›
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
left✝ : Positive n
right✝ : Positive m
this✝ : n ≄ 0
this : m ≄ 0
⊢ Positive (n * m)