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

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
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)

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›
State after:
no goals

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
State after:
no goals

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))
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

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)›
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

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
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

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
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

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›
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

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›
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

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›
State after:
no goals

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))
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)

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›
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)

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›
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)

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
this : m ≄ 0
⊢ Positive (n * m)
Tactic:
have : n ≄ 0 ∧ m ≄ 0 := And.intro ‹n ≄ 0› ‹m ≄ 0›
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
this : n ≄ 0 ∧ m ≄ 0
⊢ Positive (n * m)

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
this✝ : m ≄ 0
this : n ≄ 0 ∧ m ≄ 0
⊢ Positive (n * m)
Tactic:
have : ¬(n ≃ 0 ∨ m ≃ 0) := Logic.not_or_iff_and_not.mpr this
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
this✝ : n ≄ 0 ∧ m ≄ 0
this : ¬(n ≃ 0 ∨ m ≃ 0)
⊢ Positive (n * m)

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
this✝¹ : m ≄ 0
this✝ : n ≄ 0 ∧ m ≄ 0
this : ¬(n ≃ 0 ∨ m ≃ 0)
⊢ Positive (n * m)
Tactic:
have : n * m ≄ 0 := mt mul_split_zero.mp this
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
this✝¹ : n ≄ 0 ∧ m ≄ 0
this✝ : ¬(n ≃ 0 ∨ m ≃ 0)
this : n * m ≄ 0
⊢ Positive (n * m)

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
this✝² : m ≄ 0
this✝¹ : n ≄ 0 ∧ m ≄ 0
this✝ : ¬(n ≃ 0 ∨ m ≃ 0)
this : n * m ≄ 0
⊢ Positive (n * m)
Tactic:
have : Positive (n * m) := positive_defn.mpr this
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
this✝² : n ≄ 0 ∧ m ≄ 0
this✝¹ : ¬(n ≃ 0 ∨ m ≃ 0)
this✝ : n * m ≄ 0
this : Positive (n * m)
⊢ Positive (n * m)

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
this✝³ : m ≄ 0
this✝² : n ≄ 0 ∧ m ≄ 0
this✝¹ : ¬(n ≃ 0 ∨ m ≃ 0)
this✝ : n * m ≄ 0
this : Positive (n * m)
⊢ Positive (n * m)
Tactic:
exact this
State after:
no goals