internlm/Lean-Github huggingface dataset:
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
this : m ≄ 0
⊢ Positive (n * m)
Tactic:
have : n ≄ 0 ∧ m ≄ 0 := And.intro ‹n ≄ 0› ‹m ≄ 0›
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
this : n ≄ 0 ∧ m ≄ 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
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
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
this✝ : n ≄ 0 ∧ m ≄ 0
this : ¬(n ≃ 0 ∨ m ≃ 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
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
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
this✝¹ : n ≄ 0 ∧ m ≄ 0
this✝ : ¬(n ≃ 0 ∨ m ≃ 0)
this : n * m ≄ 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
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
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
this✝² : n ≄ 0 ∧ m ≄ 0
this✝¹ : ¬(n ≃ 0 ∨ m ≃ 0)
this✝ : n * m ≄ 0
this : Positive (n * 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
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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_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 (_ : Positive n) (_ : Positive m)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : Positive n
x✝ : Positive m
⊢ Positive (n * m)
Theorem: Lean4Axiomatic.Natural.mul_positive
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m : ℕ
x✝¹ : Positive n
x✝ : Positive m
⊢ Positive (n * m)
Tactic:
exact mul_preserves_positive.mpr (And.intro ‹Positive n› ‹Positive m›)
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_distribL_add
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ n * (m + k) ≃ n * m + n * k
Tactic:
apply ind_on (motive := λ x => x * (m + k) ≃ x * m + x * k) n
Proof state after:
case zero
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ 0 * (m + k) ≃ 0 * m + 0 * k

case step
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * (m + k) ≃ m_1 * m + m_1 * k → step m_1 * (m + k) ≃ step m_1 * m + step m_1 * k
Theorem: Lean4Axiomatic.Natural.mul_distribL_add
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ 0 * (m + k) ≃ 0 * m + 0 * k
Tactic:
case zero =>
  show 0 * (m + k) ≃ 0 * m + 0 * k
  calc
    0 * (m + k)   ≃ _ := zero_mul
    0             ≃ _ := Rel.symm Addition.zero_add
    0 + 0         ≃ _ := AA.substL (Rel.symm zero_mul)
    0 * m + 0     ≃ _ := AA.substR (Rel.symm zero_mul)
    0 * m + 0 * k ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_distribL_add
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * (m + k) ≃ m_1 * m + m_1 * k → step m_1 * (m + k) ≃ step m_1 * m + step m_1 * k
Tactic:
case step =>
  intro n (ih : n * (m + k) ≃ n * m + n * k)
  show step n * (m + k) ≃ step n * m + step n * k
  calc
    step n * (m + k)          ≃ _ := step_mul
    n * (m + k) + (m + k)     ≃ _ := AA.substL ih
    n * m + n * k + (m + k)   ≃ _ := AA.assoc
    n * m + (n * k + (m + k)) ≃ _ := AA.substR (Rel.symm AA.assoc)
    n * m + ((n * k + m) + k) ≃ _ := AA.substR (AA.substL AA.comm)
    n * m + ((m + n * k) + k) ≃ _ := AA.substR AA.assoc
    n * m + (m + (n * k + k)) ≃ _ := Rel.symm AA.assoc
    (n * m + m) + (n * k + k) ≃ _ := AA.substL (Rel.symm step_mul)
    step n * m + (n * k + k)  ≃ _ := AA.substR (Rel.symm step_mul)
    step n * m + step n * k   ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_distribL_add
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ 0 * (m + k) ≃ 0 * m + 0 * k
Tactic:
calc
  0 * (m + k)   ≃ _ := zero_mul
  0             ≃ _ := Rel.symm Addition.zero_add
  0 + 0         ≃ _ := AA.substL (Rel.symm zero_mul)
  0 * m + 0     ≃ _ := AA.substR (Rel.symm zero_mul)
  0 * m + 0 * k ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.mul_distribL_add
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n m k : ℕ
⊢ ∀ (m_1 : ℕ), m_1 * (m + k) ≃ m_1 * m + m_1 * k → step m_1 * (m + k) ≃ step m_1 * m + step m_1 * k
Tactic:
intro n (ih : n * (m + k) ≃ n * m + n * k)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m k n : ℕ
ih : n * (m + k) ≃ n * m + n * k
⊢ step n * (m + k) ≃ step n * m + step n * k
Theorem: Lean4Axiomatic.Natural.mul_distribL_add
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n✝ m k n : ℕ
ih : n * (m + k) ≃ n * m + n * k
⊢ step n * (m + k) ≃ step n * m + step n * k
Tactic:
calc
  step n * (m + k)          ≃ _ := step_mul
  n * (m + k) + (m + k)     ≃ _ := AA.substL ih
  n * m + n * k + (m + k)   ≃ _ := AA.assoc
  n * m + (n * k + (m + k)) ≃ _ := AA.substR (Rel.symm AA.assoc)
  n * m + ((n * k + m) + k) ≃ _ := AA.substR (AA.substL AA.comm)
  n * m + ((m + n * k) + k) ≃ _ := AA.substR AA.assoc
  n * m + (m + (n * k + k)) ≃ _ := Rel.symm AA.assoc
  (n * m + m) + (n * k + k) ≃ _ := AA.substL (Rel.symm step_mul)
  step n * m + (n * k + k)  ≃ _ := AA.substR (Rel.symm step_mul)
  step n * m + step n * k   ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.subst_mul_lt
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
⊢ Positive m → n₁ < n₂ → n₁ * m < n₂ * m
Tactic:
intro (_ : Positive m) (_ : n₁ < n₂)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
⊢ n₁ * m < n₂ * m
Theorem: Lean4Axiomatic.Natural.subst_mul_lt
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
⊢ n₁ * m < n₂ * m
Tactic:
have ⟨(d : ℕ), (_ : Positive d), (_ : n₂ ≃ n₁ + d)⟩ :=
  lt_defn_add.mp ‹n₁ < n₂›
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
⊢ n₁ * m < n₂ * m
Theorem: Lean4Axiomatic.Natural.subst_mul_lt
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
⊢ n₁ * m < n₂ * m
Tactic:
have : n₂ * m ≃ n₁ * m + d * m := calc
  n₂ * m         ≃ _ := AA.substL ‹n₂ ≃ n₁ + d›
  (n₁ + d) * m   ≃ _ := AA.distribR
  n₁ * m + d * m ≃ _ := Rel.refl
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
this : n₂ * m ≃ n₁ * m + d * m
⊢ n₁ * m < n₂ * m
Theorem: Lean4Axiomatic.Natural.subst_mul_lt
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
this : n₂ * m ≃ n₁ * m + d * m
⊢ n₁ * m < n₂ * m
Tactic:
have : Positive (d * m) := mul_positive ‹Positive d› ‹Positive m›
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
this✝ : n₂ * m ≃ n₁ * m + d * m
this : Positive (d * m)
⊢ n₁ * m < n₂ * m
Theorem: Lean4Axiomatic.Natural.subst_mul_lt
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n₁ n₂ m : ℕ
x✝¹ : Positive m
x✝ : n₁ < n₂
d : ℕ
left✝ : Positive d
right✝ : n₂ ≃ n₁ + d
this✝ : n₂ * m ≃ n₁ * m + d * m
this : Positive (d * m)
⊢ n₁ * m < n₂ * m
Tactic:
exact lt_defn_add.mpr
  ⟨d * m, ‹Positive (d * m)›, ‹n₂ * m ≃ n₁ * m + d * m›⟩
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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)
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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›
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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))
Proof 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
Theorem: Lean4Axiomatic.Natural.factors_eqv_1
Proof 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
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.sqrt1
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n * n ≃ 1 ↔ n ≃ 1
Tactic:
apply Iff.intro
Proof state after:
case mp
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n * n ≃ 1 → n ≃ 1

case mpr
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n ≃ 1 → n * n ≃ 1
Theorem: Lean4Axiomatic.Natural.sqrt1
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n * n ≃ 1 → n ≃ 1
Tactic:
case mp =>
  intro (_ : n * n ≃ 1)
  show n ≃ 1
  have (And.intro (_ : n ≃ 1) _) := factors_eqv_1.mp ‹n * n ≃ 1›
  exact ‹n ≃ 1›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.sqrt1
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n ≃ 1 → n * n ≃ 1
Tactic:
case mpr =>
  intro (_ : n ≃ 1)
  show n * n ≃ 1
  have : n * n ≃ 1 := factors_eqv_1.mpr (And.intro ‹n ≃ 1› ‹n ≃ 1›)
  exact this
Proof state after:
no goals
Theorem: Lean4Axiomatic.Natural.sqrt1
Proof state before:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
⊢ n * n ≃ 1 → n ≃ 1
Tactic:
intro (_ : n * n ≃ 1)
Proof state after:
ℕ : Type
inst✝⁵ : Core ℕ
inst✝⁴ : Induction ℕ
inst✝³ : Addition ℕ
inst✝² : Sign ℕ
inst✝¹ : Order ℕ
inst✝ : Multiplication ℕ
n : ℕ
x✝ : n * n ≃ 1
⊢ n ≃ 1