internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.zero_div
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 : M
pos : 0 < a
⊢ 0 / a = 0
Tactic:
exact div_eq_of (by simp) (by simpa)
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
pos : 0 < a
⊢ a * 0 ≤ 0
Tactic:
simp
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
pos : 0 < a
⊢ 0 < a * (0 + 1)
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul
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 c : M
⊢ a / (b * c) = a / b / c
Tactic:
rcases zero_le b with (rfl | hb)
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
a c : M
⊢ a / (0 * c) = a / 0 / c

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 c : M
hb : 0 < b
⊢ a / (b * c) = a / b / c
Theorem: LO.FirstOrder.Arith.Model.div_mul
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 c : M
hb : 0 < b
⊢ a / (b * c) = a / b / c
Tactic:
rcases zero_le c with (rfl | hc)
Proof state after:
case inr.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
a b : M
hb : 0 < b
⊢ a / (b * 0) = a / b / 0

case inr.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 c : M
hb : 0 < b
hc : 0 < c
⊢ a / (b * c) = a / b / c
Theorem: LO.FirstOrder.Arith.Model.div_mul
Proof state before:
case inr.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 c : M
hb : 0 < b
hc : 0 < c
⊢ a / (b * c) = a / b / c
Tactic:
exact div_eq_of
  (by calc
        b * c * (a / b / c) ≤ b * (a / b) := by simp [mul_assoc]; exact mul_le_mul_left (mul_div_le_pos (a / b) hc)
        _                   ≤ a := mul_div_le_pos a hb)
  (by calc
        a < b * (a / b + 1)         := lt_mul_div_succ a hb
        _ ≤ b * c * (a / b / c + 1) := by simp [mul_assoc]; exact mul_le_mul_left (lt_iff_succ_le.mp <| lt_mul_div_succ (a / b) hc))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul
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
a c : M
⊢ a / (0 * c) = a / 0 / c
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul
Proof state before:
case inr.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
a b : M
hb : 0 < b
⊢ a / (b * 0) = a / b / 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul
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 c : M
hb : 0 < b
hc : 0 < c
⊢ b * c * (a / b / c) ≤ a
Tactic:
calc
  b * c * (a / b / c) ≤ b * (a / b) := by simp [mul_assoc]; exact mul_le_mul_left (mul_div_le_pos (a / b) hc)
  _                   ≤ a := mul_div_le_pos a hb
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul
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 c : M
hb : 0 < b
hc : 0 < c
⊢ b * c * (a / b / c) ≤ b * (a / b)
Tactic:
simp [mul_assoc]
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 c : M
hb : 0 < b
hc : 0 < c
⊢ b * (c * (a / b / c)) ≤ b * (a / b)
Theorem: LO.FirstOrder.Arith.Model.div_mul
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 c : M
hb : 0 < b
hc : 0 < c
⊢ b * (c * (a / b / c)) ≤ b * (a / b)
Tactic:
exact mul_le_mul_left (mul_div_le_pos (a / b) hc)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul
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 c : M
hb : 0 < b
hc : 0 < c
⊢ a < b * c * (a / b / c + 1)
Tactic:
calc
  a < b * (a / b + 1)         := lt_mul_div_succ a hb
  _ ≤ b * c * (a / b / c + 1) := by simp [mul_assoc]; exact mul_le_mul_left (lt_iff_succ_le.mp <| lt_mul_div_succ (a / b) hc)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul
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 c : M
hb : 0 < b
hc : 0 < c
⊢ b * (a / b + 1) ≤ b * c * (a / b / c + 1)
Tactic:
simp [mul_assoc]
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 c : M
hb : 0 < b
hc : 0 < c
⊢ b * (a / b + 1) ≤ b * (c * (a / b / c + 1))
Theorem: LO.FirstOrder.Arith.Model.div_mul
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 c : M
hb : 0 < b
hc : 0 < c
⊢ b * (a / b + 1) ≤ b * (c * (a / b / c + 1))
Tactic:
exact mul_le_mul_left (lt_iff_succ_le.mp <| lt_mul_div_succ (a / b) hc)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_div_le
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
⊢ b * (a / b) ≤ a
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
⊢ b * (a / b) ≤ a
Theorem: LO.FirstOrder.Arith.Model.mul_div_le
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
⊢ b * (a / b) ≤ a
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
⊢ b * (a / b) ≤ a
Theorem: LO.FirstOrder.Arith.Model.mul_div_le
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
⊢ b * (a / b) ≤ a
Tactic:
rcases eq_mul_div_add_of_pos a pos with ⟨v, _, e⟩
Proof state after:
case inr.intro.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
v : M
left✝ : v < b
e : a = b * (a / b) + v
⊢ b * (a / b) ≤ a
Theorem: LO.FirstOrder.Arith.Model.mul_div_le
Proof state before:
case inr.intro.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
v : M
left✝ : v < b
e : a = b * (a / b) + v
⊢ b * (a / b) ≤ a
Tactic:
simpa [← e] using show b * (a / b) ≤ b * (a / b) + v from le_self_add
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_div_le
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_le
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
⊢ a / b ≤ a
Tactic:
have : 0 ≤ b := 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
⊢ a / b ≤ a
Theorem: LO.FirstOrder.Arith.Model.div_le
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
⊢ a / b ≤ a
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
⊢ a / b ≤ a
Theorem: LO.FirstOrder.Arith.Model.div_le
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
⊢ a / b ≤ a
Tactic:
have : 1 * (a / b) ≤ b * (a / b) := mul_le_mul_of_nonneg_right (le_iff_lt_succ.mpr (by simp[pos])) (by 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
this : 1 * (a / b) ≤ b * (a / b)
⊢ a / b ≤ a
Theorem: LO.FirstOrder.Arith.Model.div_le
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
this : 1 * (a / b) ≤ b * (a / b)
⊢ a / b ≤ a
Tactic:
simpa using le_trans this (mul_div_le a b)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_le
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
⊢ 1 < b + 1
Tactic:
simp[pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_le
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
⊢ 0 ≤ a / b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul_le
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
⊢ a / b * b ≤ a
Tactic:
rw [mul_comm]
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
⊢ b * (a / b) ≤ a
Theorem: LO.FirstOrder.Arith.Model.div_mul_le
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
⊢ b * (a / b) ≤ a
Tactic:
exact mul_div_le _ _
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_mul_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 b : M
pos : 0 < b
⊢ a < b * (a / b + 1)
Tactic:
rcases eq_mul_div_add_of_pos a pos with ⟨v, hv, e⟩
Proof state after:
case intro.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
v : M
hv : v < b
e : a = b * (a / b) + v
⊢ a < b * (a / b + 1)
Theorem: LO.FirstOrder.Arith.Model.lt_mul_div
Proof state before:
case intro.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
v : M
hv : v < b
e : a = b * (a / b) + v
⊢ a < b * (a / b + 1)
Tactic:
calc a = b * (a / b) + v := e
     _ < b * (a / b + 1) := by simp [mul_add, hv]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.lt_mul_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 b : M
pos : 0 < b
v : M
hv : v < b
e : a = b * (a / b) + v
⊢ b * (a / b) + v < b * (a / b + 1)
Tactic:
simp [mul_add, hv]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_one
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
⊢ a / 1 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_one
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
⊢ a < a / 1 + 1
Tactic:
simpa using lt_mul_div a one_pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_add_mul_self
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 c b : M
pos : 0 < b
⊢ (a + c * b) / b = a / b + c
Tactic:
rcases div_spec_of_pos' a pos with ⟨r, hr, ex⟩
Proof state after:
case intro.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 c b : M
pos : 0 < b
r : M
hr : r < b
ex : a = a / b * b + r
⊢ (a + c * b) / b = a / b + c
Theorem: LO.FirstOrder.Arith.Model.div_add_mul_self
Proof state before:
case intro.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 c b : M
pos : 0 < b
r : M
hr : r < b
ex : a = a / b * b + r
⊢ (a + c * b) / b = a / b + c
Tactic:
simpa [add_mul, add_right_comm, ← ex] using div_mul_add (a / b + c) _ hr
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_add_mul_self'
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 c b : M
pos : 0 < b
⊢ (a + b * c) / b = a / b + c
Tactic:
simpa [mul_comm] using div_add_mul_self a c pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul_add_self
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 c b : M
pos : 0 < b
⊢ (a * b + c) / b = a + c / b
Tactic:
simp [div_add_mul_self, pos, add_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul_add_self'
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 c b : M
pos : 0 < b
⊢ (b * a + c) / b = a + c / b
Tactic:
simp [mul_comm b a, div_mul_add_self, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul_left
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 / b = a
Tactic:
simpa using div_mul_add a _ pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul_right
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 * a / b = a
Tactic:
simpa [mul_comm] using div_mul_add a _ pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_eq_zero_of_lt
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 : a < b
⊢ a / b = 0
Tactic:
simpa using div_mul_add 0 b h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_sq
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
⊢ a ^ 2 / a = a
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 ^ 2 / 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
⊢ a ^ 2 / a = a
Theorem: LO.FirstOrder.Arith.Model.div_sq
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 ^ 2 / 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_sq
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 : M
pos : 0 < a
⊢ a ^ 2 / a = a
Tactic:
simp [sq, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_self
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
hx : 0 < a
⊢ a / a = 1
Tactic:
simpa using div_mul_left 1 hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_mul'
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 * a / b = a
Tactic:
simp [mul_comm, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_add_self_left
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
pos : 0 < a
b : M
⊢ (a + b) / a = 1 + b / a
Tactic:
simpa using div_mul_add_self 1 b pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_add_self_right
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) / b = a / b + 1
Tactic:
simpa using div_add_mul_self a 1 pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_div_self_of_dvd
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
⊢ a * (b / a) = b ↔ a ∣ b
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
b : M
⊢ 0 * (b / 0) = b ↔ 0 ∣ b

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 < a
⊢ a * (b / a) = b ↔ a ∣ b
Theorem: LO.FirstOrder.Arith.Model.mul_div_self_of_dvd
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
b : M
⊢ 0 * (b / 0) = b ↔ 0 ∣ b
Tactic:
simp[eq_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_div_self_of_dvd
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 < a
⊢ a * (b / a) = b ↔ a ∣ b
Tactic:
constructor
Proof state after:
case inr.mp
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 < a
⊢ a * (b / a) = b → a ∣ b

case inr.mpr
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 < a
⊢ a ∣ b → a * (b / a) = b
Theorem: LO.FirstOrder.Arith.Model.mul_div_self_of_dvd
Proof state before:
case inr.mp
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 < a
⊢ a * (b / a) = b → a ∣ b
Tactic:
intro e
Proof state after:
case inr.mp
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 < a
e : a * (b / a) = b
⊢ a ∣ b
Theorem: LO.FirstOrder.Arith.Model.mul_div_self_of_dvd
Proof state before:
case inr.mp
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 < a
e : a * (b / a) = b
⊢ a ∣ b
Tactic:
rw [←e]
Proof state after:
case inr.mp
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 < a
e : a * (b / a) = b
⊢ a ∣ a * (b / a)
Theorem: LO.FirstOrder.Arith.Model.mul_div_self_of_dvd
Proof state before:
case inr.mp
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 < a
e : a * (b / a) = b
⊢ a ∣ a * (b / a)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_div_self_of_dvd
Proof state before:
case inr.mpr
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 < a
⊢ a ∣ b → a * (b / a) = b
Tactic:
rintro ⟨r, rfl⟩
Proof state after:
case inr.mpr.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 : M
pos : 0 < a
r : M
⊢ a * (a * r / a) = a * r
Theorem: LO.FirstOrder.Arith.Model.mul_div_self_of_dvd
Proof state before:
case inr.mpr.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 : M
pos : 0 < a
r : M
⊢ a * (a * r / a) = a * r
Tactic:
simp [pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_lt_of_pos_of_one_lt
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
ha : 0 < a
hb : 1 < b
⊢ a / b < a
Tactic:
rcases zero_le (a / b) with (e | lt)
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
a b : M
ha : 0 < a
hb : 1 < b
e : 0 = a / b
⊢ a / b < a

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
ha : 0 < a
hb : 1 < b
lt : 0 < a / b
⊢ a / b < a
Theorem: LO.FirstOrder.Arith.Model.div_lt_of_pos_of_one_lt
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
a b : M
ha : 0 < a
hb : 1 < b
e : 0 = a / b
⊢ a / b < a
Tactic:
simp [←e, ha]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_lt_of_pos_of_one_lt
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
ha : 0 < a
hb : 1 < b
lt : 0 < a / b
⊢ a / b < a
Tactic:
exact lt_of_lt_of_le (lt_mul_of_one_lt_left lt hb) (mul_div_le a b)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_two_mul_div_two_add_one
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
⊢ a ≤ 2 * (a / 2) + 1
Tactic:
have : a < 2 * (a / 2 + 1) := lt_mul_div_succ a (show 0 < 2 from 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
a : M
this : a < 2 * (a / 2 + 1)
⊢ a ≤ 2 * (a / 2) + 1
Theorem: LO.FirstOrder.Arith.Model.le_two_mul_div_two_add_one
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
this : a < 2 * (a / 2 + 1)
⊢ a ≤ 2 * (a / 2) + 1
Tactic:
exact le_iff_lt_succ.mpr (by simpa [add_assoc, one_add_one_eq_two, mul_add] using this)
Proof state after:
no goals