internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.open_leastNumber
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
P : M → Prop
hP : ∃ p, p.Open ∧ ∀ (x : M), P x ↔ (Semiformula.Evalm M ![x] id) p
zero : P 0
a : M
counterex : ¬P a
n : M
ih : P n
A : ∀ (x : M), P x → P (x + 1)
⊢ P (n + 1)
Tactic:
exact A n ih
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ ∃! u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
have : ∃ u, b * u ≤ a ∧ a < b * (u + 1) := by
  have : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1) := by
    simpa using open_leastNumber (P := fun u ↦ b * u ≤ a) ⟨“x | &b * x ≤ &a”, by simp, by intro x; simp⟩
  simp at this
  have hx : a < b * (a + 1) := by
    have : a + 0 < b * a + b :=
      add_lt_add_of_le_of_lt (le_mul_self_of_pos_left pos) pos
    simpa [mul_add] using this
  exact this hx
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃! u, b * u ≤ a ∧ a < b * (u + 1)
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃! u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
rcases this with ⟨u, hu⟩
Proof state after:
case intro
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃! u, b * u ≤ a ∧ a < b * (u + 1)
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
have : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1) := by
  simpa using open_leastNumber (P := fun u ↦ b * u ≤ a) ⟨“x | &b * x ≤ &a”, by simp, by intro x; simp⟩
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
have hx : a < b * (a + 1) := by
  have : a + 0 < b * a + b :=
    add_lt_add_of_le_of_lt (le_mul_self_of_pos_left pos) pos
  simpa [mul_add] using this
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
hx : a < b * (a + 1)
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
hx : a < b * (a + 1)
⊢ ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
exact this hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
Tactic:
simpa using open_leastNumber (P := fun u ↦ b * u ≤ a) ⟨“x | &b * x ≤ &a”, by simp, by intro x; simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ “(&b * #0) ≤ &a”.Open
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ ∀ (x : M), (fun u => b * u ≤ a) x ↔ (Semiformula.Evalm M ![x] id) (“(&b * #0) ≤ &a”)
Tactic:
intro x
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
x : M
⊢ (fun u => b * u ≤ a) x ↔ (Semiformula.Evalm M ![x] id) (“(&b * #0) ≤ &a”)
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
x : M
⊢ (fun u => b * u ≤ a) x ↔ (Semiformula.Evalm M ![x] id) (“(&b * #0) ≤ &a”)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
⊢ a < b * (a + 1)
Tactic:
have : a + 0 < b * a + b :=
  add_lt_add_of_le_of_lt (le_mul_self_of_pos_left pos) pos
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this✝ : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
this : a + 0 < b * a + b
⊢ a < b * (a + 1)
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
this✝ : a < b * (a + 1) → ∃ u, b * u ≤ a ∧ a < b * (u + 1)
this : a + 0 < b * a + b
⊢ a < b * (a + 1)
Tactic:
simpa [mul_add] using this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
⊢ ∀ (y : M), b * y ≤ a ∧ a < b * (y + 1) → y = u
Tactic:
intro u' hu'
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
⊢ u' = u
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
⊢ u' = u
Tactic:
by_contra ne
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
⊢ False
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
⊢ False
Tactic:
wlog lt : u < u'
Proof state after:
case inr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] [inst_6 : M ⊧ₘ* 𝐈open] (a : M) {b : M},
    0 < b →
      ∀ (u : M), b * u ≤ a ∧ a < b * (u + 1) → ∀ (u' : M), b * u' ≤ a ∧ a < b * (u' + 1) → ¬u' = u → u < u' → False
lt : ¬u < u'
⊢ False

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
⊢ False
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
⊢ False
Tactic:
have : a < a := by calc
  a < b * (u + 1) := hu.2
  _ ≤ b * u'      := (_root_.mul_le_mul_left pos).mpr (lt_iff_succ_le.mp lt)
  _ ≤ a           := hu'.1
Proof state after:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
this : a < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
this : a < a
⊢ False
Tactic:
exact LT.lt.false this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
case inr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] [inst_6 : M ⊧ₘ* 𝐈open] (a : M) {b : M},
    0 < b →
      ∀ (u : M), b * u ≤ a ∧ a < b * (u + 1) → ∀ (u' : M), b * u' ≤ a ∧ a < b * (u' + 1) → ¬u' = u → u < u' → False
lt : ¬u < u'
⊢ False
Tactic:
exact this a pos u' hu' u hu (Ne.symm ne) (Ne.lt_of_le ne $ by simpa using lt)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
this :
  ∀ {M : Type u_1} [inst : Zero M] [inst_1 : One M] [inst_2 : Add M] [inst_3 : Mul M] [inst_4 : LT M]
    [inst_5 : M ⊧ₘ* 𝐏𝐀⁻] [inst_6 : M ⊧ₘ* 𝐈open] (a : M) {b : M},
    0 < b →
      ∀ (u : M), b * u ≤ a ∧ a < b * (u + 1) → ∀ (u' : M), b * u' ≤ a ∧ a < b * (u' + 1) → ¬u' = u → u < u' → False
lt : ¬u < u'
⊢ u' ≤ u
Tactic:
simpa using lt
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique_pos
Proof state before:
M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
u : M
hu : b * u ≤ a ∧ a < b * (u + 1)
u' : M
hu' : b * u' ≤ a ∧ a < b * (u' + 1)
ne : ¬u' = u
lt : u < u'
⊢ a < a
Tactic:
calc
a < b * (u + 1) := hu.2
_ ≤ b * u'      := (_root_.mul_le_mul_left pos).mpr (lt_iff_succ_le.mp lt)
_ ≤ a           := hu'.1
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
⊢ ∃! u, (0 < b → b * u ≤ a ∧ a < b * (u + 1)) ∧ (b = 0 → u = 0)
Tactic:
have : 0 ≤ b := by exact zero_le b
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
this : 0 ≤ b
⊢ ∃! u, (0 < b → b * u ≤ a ∧ a < b * (u + 1)) ∧ (b = 0 → u = 0)
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
this : 0 ≤ b
⊢ ∃! u, (0 < b → b * u ≤ a ∧ a < b * (u + 1)) ∧ (b = 0 → u = 0)
Tactic:
rcases this with (rfl | pos) <;> simp [*]
Proof state after:
case inr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ ∃! u, (b * u ≤ a ∧ a < b * (u + 1)) ∧ (b = 0 → u = 0)
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
⊢ 0 ≤ b
Tactic:
exact zero_le b
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_exists_unique
Proof state before:
case inr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < b
⊢ ∃! u, (b * u ≤ a ∧ a < b * (u + 1)) ∧ (b = 0 → u = 0)
Tactic:
simpa [pos_iff_ne_zero.mp pos] using div_exists_unique_pos a pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
⊢ ∃ r < b, a = b * (a / b) + r
Tactic:
let r := a - b * (a / b)
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
⊢ ∃ r < b, a = b * (a / b) + r
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
⊢ ∃ r < b, a = b * (a / b) + r
Tactic:
have e : a = b * (a / b) + r := by simp [add_tsub_self_of_le (mul_div_le_pos a hb)]
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
⊢ ∃ r < b, a = b * (a / b) + r
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
⊢ ∃ r < b, a = b * (a / b) + r
Tactic:
exact ⟨r, by
  by_contra A
  have hyv : b ≤ r := by simpa using A
  have : a < a := by calc
        a < b * (a / b + 1) := lt_mul_div_succ a hb
        _ ≤ b * (a / b) + r := by simpa [mul_add] using hyv
        _ = a               := e.symm
  simp at this, e⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
⊢ a = b * (a / b) + r
Tactic:
simp [add_tsub_self_of_le (mul_div_le_pos a hb)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
⊢ r < b
Tactic:
by_contra A
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
A : ¬r < b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
A : ¬r < b
⊢ False
Tactic:
have hyv : b ≤ r := by simpa using A
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
A : ¬r < b
hyv : b ≤ r
⊢ False
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
A : ¬r < b
hyv : b ≤ r
⊢ False
Tactic:
have : a < a := by calc
      a < b * (a / b + 1) := lt_mul_div_succ a hb
      _ ≤ b * (a / b) + r := by simpa [mul_add] using hyv
      _ = a               := e.symm
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
A : ¬r < b
hyv : b ≤ r
this : a < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
A : ¬r < b
hyv : b ≤ r
this : a < a
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
A : ¬r < b
⊢ b ≤ r
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
A : ¬r < b
hyv : b ≤ r
⊢ a < a
Tactic:
calc
a < b * (a / b + 1) := lt_mul_div_succ a hb
_ ≤ b * (a / b) + r := by simpa [mul_add] using hyv
_ = a               := e.symm
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_mul_div_add_of_pos
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
hb : 0 < b
r : M := a - b * (a / b)
e : a = b * (a / b) + r
A : ¬r < b
hyv : b ≤ r
⊢ b * (a / b + 1) ≤ b * (a / b) + r
Tactic:
simpa [mul_add] using hyv
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_spec_zero
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a : M
⊢ 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_defined
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
⊢ 𝚺₀-Function₂ fun x x_1 => x / x_1 via divDef
Tactic:
intro v
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => (fun x x_1 => x / x_1) (v 0) (v 1)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val divDef)
Theorem: LO.FirstOrder.Arith.Model.div_defined
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
v : Fin (Nat.succ 2) → M
⊢ (fun v => v 0 = (fun v => (fun x x_1 => x / x_1) (v 0) (v 1)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val divDef)
Tactic:
simp[div_graph, divDef, Matrix.vecHead, Matrix.vecTail]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_spec_of_pos'
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
b a : M
h : 0 < b
⊢ ∃ v < b, a = a / b * b + v
Tactic:
simpa [mul_comm] using eq_mul_div_add_of_pos a h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_eq_of
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
c a b : M
hb : b * c ≤ a
ha : a < b * (c + 1)
⊢ a / b = c
Tactic:
have pos : 0 < b := pos_of_mul_pos_left (pos_of_gt ha) (by simp)
Proof state after:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
c a b : M
hb : b * c ≤ a
ha : a < b * (c + 1)
pos : 0 < b
⊢ a / b = c
Theorem: LO.FirstOrder.Arith.Model.div_eq_of
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
c a b : M
hb : b * c ≤ a
ha : a < b * (c + 1)
pos : 0 < b
⊢ a / b = c
Tactic:
exact (div_exists_unique_pos a pos).unique ⟨mul_div_le_pos a pos, lt_mul_div_succ a pos⟩ ⟨hb, ha⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_eq_of
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
c a b : M
hb : b * c ≤ a
ha : a < b * (c + 1)
⊢ 0 ≤ c + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul_add
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b r : M
hr : r < b
⊢ b * a ≤ a * b + r
Tactic:
simp [mul_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul_add
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b r : M
hr : r < b
⊢ a * b + r < b * (a + 1)
Tactic:
simp [mul_comm b a, mul_add, hr]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul_add'
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b r : M
hr : r < b
⊢ (b * a + r) / b = a
Tactic:
simpa [mul_comm] using div_mul_add a b hr
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_div
Proof state before:
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a : M
⊢ 0 / a = 0
Tactic:
rcases zero_le a with (rfl | pos)
Proof state after:
case inl
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
⊢ 0 / 0 = 0

case inr
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a : M
pos : 0 < a
⊢ 0 / a = 0
Theorem: LO.FirstOrder.Arith.Model.zero_div
Proof state before:
case inl
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
⊢ 0 / 0 = 0
Tactic:
simp
Proof state after:
no goals