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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ 1 ↔ n ≃ 1 ∧ m ≃ 1
Tactic:
apply Iff.intro
State after:
case mp
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ 1 → n ≃ 1 ∧ m ≃ 1

case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n ≃ 1 ∧ m ≃ 1 → n * m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n * m ≃ 1 → n ≃ 1 ∧ m ≃ 1
Tactic:
case mp =>
  intro (_ : n * m ≃ 1)
  show n ≃ 1 ∧ m ≃ 1
  have : Positive (n * m) :=
    positive_subst (Rel.symm ‹n * m ≃ 1›) one_positive
  have (And.intro (_ : Positive n) (_ : Positive m)) :=
    mul_preserves_positive.mp this
  have : n ≥ 1 := positive_ge.mp ‹Positive n›
  have : n > 1 ∨ n ≃ 1 := ge_split this
  match this with
  | Or.inl (_ : n > 1) =>
    have : 1 < n * m := calc
      1     ≤ _ := positive_ge.mp ‹Positive m›
      m     ≃ _ := Rel.symm AA.identL
      1 * m < _ := subst_mul_lt ‹Positive m› ‹1 < n›
      n * m ≃ _ := Rel.refl
    have two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1) :=
      AA.TwoOfThree.twoAndThree ‹n * m ≃ 1› ‹n * m > 1›
    have notTwo : ¬AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1) :=
      (trichotomy (n * m) 1).atMostOne
    exact absurd two notTwo
  | Or.inr (_ : n ≃ 1) =>
    have : m ≃ 1 := calc
      m     ≃ _ := Rel.symm AA.identL
      1 * m ≃ _ := AA.substL (Rel.symm ‹n ≃ 1›)
      n * m ≃ _ := ‹n * m ≃ 1›
      1     ≃ _ := Rel.refl
    exact And.intro ‹n ≃ 1› ‹m ≃ 1›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n ≃ 1 ∧ m ≃ 1 → n * m ≃ 1
Tactic:
case mpr =>
  intro (And.intro (_ : n ≃ 1) (_ : m ≃ 1))
  show n * m ≃ 1
  calc
    n * m ≃ _ := AA.substL ‹n ≃ 1›
    1 * m ≃ _ := AA.identL
    m     ≃ _ := ‹m ≃ 1›
    1     ≃ _ := Rel.refl
State after:
no goals

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

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
have : Positive (n * m) :=
  positive_subst (Rel.symm ‹n * m ≃ 1›) one_positive
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this : Positive (n * m)
⊢ n ≃ 1 ∧ m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this : Positive (n * m)
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
have (And.intro (_ : Positive n) (_ : Positive m)) :=
  mul_preserves_positive.mp this
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
⊢ n ≃ 1 ∧ m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
have : n ≥ 1 := positive_ge.mp ‹Positive n›
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝ : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this : n ≥ 1
⊢ n ≃ 1 ∧ m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝ : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this : n ≥ 1
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
have : n > 1 ∨ n ≃ 1 := ge_split this
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝¹ : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝ : n ≥ 1
this : n > 1 ∨ n ≃ 1
⊢ n ≃ 1 ∧ m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝¹ : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝ : n ≥ 1
this : n > 1 ∨ n ≃ 1
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
match this with
| Or.inl (_ : n > 1) =>
  have : 1 < n * m := calc
    1     ≤ _ := positive_ge.mp ‹Positive m›
    m     ≃ _ := Rel.symm AA.identL
    1 * m < _ := subst_mul_lt ‹Positive m› ‹1 < n›
    n * m ≃ _ := Rel.refl
  have two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1) :=
    AA.TwoOfThree.twoAndThree ‹n * m ≃ 1› ‹n * m > 1›
  have notTwo : ¬AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1) :=
    (trichotomy (n * m) 1).atMostOne
  exact absurd two notTwo
| Or.inr (_ : n ≃ 1) =>
  have : m ≃ 1 := calc
    m     ≃ _ := Rel.symm AA.identL
    1 * m ≃ _ := AA.substL (Rel.symm ‹n ≃ 1›)
    n * m ≃ _ := ‹n * m ≃ 1›
    1     ≃ _ := Rel.refl
  exact And.intro ‹n ≃ 1› ‹m ≃ 1›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝¹ : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝ : n ≥ 1
this : n > 1 ∨ n ≃ 1
h✝ : n > 1
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
have : 1 < n * m := calc
  1     ≤ _ := positive_ge.mp ‹Positive m›
  m     ≃ _ := Rel.symm AA.identL
  1 * m < _ := subst_mul_lt ‹Positive m› ‹1 < n›
  n * m ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n > 1
this : 1 < n * m
⊢ n ≃ 1 ∧ m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n > 1
this : 1 < n * m
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
have two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1) :=
  AA.TwoOfThree.twoAndThree ‹n * m ≃ 1› ‹n * m > 1›
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n > 1
this : 1 < n * m
two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1)
⊢ n ≃ 1 ∧ m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n > 1
this : 1 < n * m
two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1)
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
have notTwo : ¬AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1) :=
  (trichotomy (n * m) 1).atMostOne
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n > 1
this : 1 < n * m
two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1)
notTwo : ¬AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1)
⊢ n ≃ 1 ∧ m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n > 1
this : 1 < n * m
two : AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1)
notTwo : ¬AA.TwoOfThree (n * m < 1) (n * m ≃ 1) (n * m > 1)
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
exact absurd two notTwo
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝¹ : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝ : n ≥ 1
this : n > 1 ∨ n ≃ 1
h✝ : n ≃ 1
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
have : m ≃ 1 := calc
  m     ≃ _ := Rel.symm AA.identL
  1 * m ≃ _ := AA.substL (Rel.symm ‹n ≃ 1›)
  n * m ≃ _ := ‹n * m ≃ 1›
  1     ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n ≃ 1
this : m ≃ 1
⊢ n ≃ 1 ∧ m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝ : n * m ≃ 1
this✝² : Positive (n * m)
left✝ : Positive n
right✝ : Positive m
this✝¹ : n ≥ 1
this✝ : n > 1 ∨ n ≃ 1
h✝ : n ≃ 1
this : m ≃ 1
⊢ n ≃ 1 ∧ m ≃ 1
Tactic:
exact And.intro ‹n ≃ 1› ‹m ≃ 1›
State after:
no goals

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
⊢ n ≃ 1 ∧ m ≃ 1 → n * m ≃ 1
Tactic:
intro (And.intro (_ : n ≃ 1) (_ : m ≃ 1))
State after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
left✝ : n ≃ 1
right✝ : m ≃ 1
⊢ n * m ≃ 1

State before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
left✝ : n ≃ 1
right✝ : m ≃ 1
⊢ n * m ≃ 1
Tactic:
calc
  n * m ≃ _ := AA.substL ‹n ≃ 1›
  1 * m ≃ _ := AA.identL
  m     ≃ _ := ‹m ≃ 1›
  1     ≃ _ := Rel.refl
State after:
no goals