internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.sub_existsUnique
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
this : b ≤ a ∨ a < b
⊢ ∃! c, (a ≥ b → a = b + c) ∧ (a < b → c = 0)
Tactic:
rcases this with (hxy | hxy) <;> simp [hxy]
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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hxy : b ≤ a
⊢ ∃! c, a = b + c
Theorem: LO.FirstOrder.Arith.Model.sub_existsUnique
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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hxy : b ≤ a
⊢ ∃! c, a = b + c
Tactic:
have : ∃ c, a = b + c := exists_add_of_le hxy
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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hxy : b ≤ a
this : ∃ c, a = b + c
⊢ ∃! c, a = b + c
Theorem: LO.FirstOrder.Arith.Model.sub_existsUnique
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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hxy : b ≤ a
this : ∃ c, a = b + c
⊢ ∃! c, a = b + c
Tactic:
rcases this with ⟨c, rfl⟩
Proof state after:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b✝ c✝ b c : M
hxy : b ≤ b + c
⊢ ∃! c_1, b + c = b + c_1
Theorem: LO.FirstOrder.Arith.Model.sub_existsUnique
Proof state before:
case inl.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b✝ c✝ b c : M
hxy : b ≤ b + c
⊢ ∃! c_1, b + c = b + c_1
Tactic:
exact ExistsUnique.intro c rfl (fun a h => (add_left_cancel h).symm)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_le_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
⊢ a - b ≤ a
Tactic:
have : b ≤ a ∨ a < b := le_or_lt b 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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
this : b ≤ a ∨ a < b
⊢ a - b ≤ a
Theorem: LO.FirstOrder.Arith.Model.sub_le_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
this : b ≤ a ∨ a < b
⊢ a - b ≤ a
Tactic:
rcases this with (hxy | hxy) <;> simp[hxy]
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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hxy : b ≤ a
⊢ 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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hxy : a < b
⊢ a - b ≤ a
Theorem: LO.FirstOrder.Arith.Model.sub_le_self
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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hxy : b ≤ a
⊢ a - b ≤ a
Tactic:
simpa [← sub_spec_of_ge hxy] using show a - b ≤ b + (a - b) from le_add_self
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_le_self
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 ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hxy : a < b
⊢ a - b ≤ a
Tactic:
simp[sub_spec_of_lt hxy]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 𝚺₀-Function₂ fun x x_1 => x - x_1 via subDef
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
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 subDef)
Theorem: LO.FirstOrder.Arith.Model.sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
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 subDef)
Tactic:
simp [subDef, sub_eq_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ a ≥ a
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_spec_of_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : a ≤ b
⊢ a - b = 0
Tactic:
rcases lt_or_eq_of_le h with (lt | rfl) <;> simp [sub_spec_of_lt, *]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_add_self_of_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ a - b + b = a
Tactic:
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ a = a - b + b
Theorem: LO.FirstOrder.Arith.Model.sub_add_self_of_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ a = a - b + b
Tactic:
rw [add_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ a = b + (a - b)
Theorem: LO.FirstOrder.Arith.Model.sub_add_self_of_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ a = b + (a - b)
Tactic:
exact sub_spec_of_ge h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.add_tsub_self_of_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ b + (a - b) = a
Tactic:
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ a = b + (a - b)
Theorem: LO.FirstOrder.Arith.Model.add_tsub_self_of_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ a = b + (a - b)
Tactic:
exact sub_spec_of_ge h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.add_sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a + b - b = a
Tactic:
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a = a + b - b
Theorem: LO.FirstOrder.Arith.Model.add_sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a = a + b - b
Tactic:
simpa [add_comm b] using sub_spec_of_ge (@le_add_self _ _ b a)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.add_sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ b + a - b = a
Tactic:
simp [add_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_sub
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ a - 0 = a
Tactic:
simpa using sub_add_self_of_le (show 0 ≤ a from zero_le a)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_remove_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
e : a = b + c
⊢ a - c = b
Tactic:
simp[e]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a - b - c = a - (b + c)
Tactic:
by_cases ha : b + c ≤ a
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : b + c ≤ a
⊢ a - b - c = a - (b + c)

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
⊢ a - b - c = a - (b + c)
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : b + c ≤ a
⊢ a - b - c = a - (b + c)
Tactic:
exact sub_remove_left <| sub_remove_left <| by
  simp [add_assoc, show c + b = b + c from add_comm _ _, sub_add_self_of_le, ha]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : b + c ≤ a
⊢ a = a - (b + c) + c + b
Tactic:
simp [add_assoc, show c + b = b + c from add_comm _ _, sub_add_self_of_le, ha]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
⊢ a - b - c = a - (b + c)
Tactic:
simp [sub_spec_of_lt (show a < b + c from not_le.mp ha)]
Proof state after:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
⊢ a - b - c = 0
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
⊢ a - b - c = 0
Tactic:
by_cases hc : c ≤ a - b
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : c ≤ a - b
⊢ a - b - c = 0

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : ¬c ≤ a - b
⊢ a - b - c = 0
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : c ≤ a - b
⊢ a - b - c = 0
Tactic:
by_cases hb : b ≤ a
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
⊢ a - b - c = 0

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : ¬b ≤ a
⊢ a - b - c = 0
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
⊢ a - b - c = 0
Tactic:
have : a < a := calc
  a < b + c       := not_le.mp ha
  _ ≤ b + (a - b) := by simp[hc]
  _ = a           := add_tsub_self_of_le hb
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
this : a < a
⊢ a - b - c = 0
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
this : a < a
⊢ a - b - c = 0
Tactic:
simp at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : b ≤ a
⊢ b + c ≤ b + (a - b)
Tactic:
simp[hc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : c ≤ a - b
hb : ¬b ≤ a
⊢ a - b - c = 0
Tactic:
simp [show a - b = 0 from sub_spec_of_lt (not_le.mp hb)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_sub
Proof state before:
case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
ha : ¬b + c ≤ a
hc : ¬c ≤ a - b
⊢ a - b - c = 0
Tactic:
exact sub_spec_of_lt (not_le.mp hc)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pos_sub_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 0 < a - b → b < a
Tactic:
contrapose
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ ¬b < a → ¬0 < a - b
Theorem: LO.FirstOrder.Arith.Model.pos_sub_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ ¬b < a → ¬0 < a - b
Tactic:
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a ≤ b → a - b = 0
Theorem: LO.FirstOrder.Arith.Model.pos_sub_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a ≤ b → a - b = 0
Tactic:
exact sub_spec_of_le
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pos_sub_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ b < a → 0 < a - b
Tactic:
intro h
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b < a
⊢ 0 < a - b
Theorem: LO.FirstOrder.Arith.Model.pos_sub_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b < a
⊢ 0 < a - b
Tactic:
by_contra hs
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b < a
hs : ¬0 < a - b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.pos_sub_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b < a
hs : ¬0 < a - b
⊢ False
Tactic:
simp at hs
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b < a
hs : a - b = 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.pos_sub_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b < a
hs : a - b = 0
⊢ False
Tactic:
have : a = b := by simpa [hs] using sub_spec_of_ge (show b ≤ a from LT.lt.le h)
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b < a
hs : a - b = 0
this : a = b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.pos_sub_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b < a
hs : a - b = 0
this : a = b
⊢ False
Tactic:
simp [this] at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pos_sub_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b < a
hs : a - b = 0
⊢ a = b
Tactic:
simpa [hs] using sub_spec_of_ge (show b ≤ a from LT.lt.le h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_eq_zero_iff_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ ¬a - b = 0 ↔ ¬a ≤ b
Tactic:
simp [←pos_iff_ne_zero]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_or_succ
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ a = 0 ∨ ∃ a', a = a' + 1
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 0 = 0 ∨ ∃ a', 0 = a' + 1

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
pos : 0 < a
⊢ a = 0 ∨ ∃ a', a = a' + 1
Theorem: LO.FirstOrder.Arith.Model.zero_or_succ
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ 0 = 0 ∨ ∃ a', 0 = a' + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_or_succ
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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
pos : 0 < a
⊢ a = 0 ∨ ∃ a', a = a' + 1
Tactic:
right
Proof state after:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
pos : 0 < a
⊢ ∃ a', a = a' + 1
Theorem: LO.FirstOrder.Arith.Model.zero_or_succ
Proof state before:
case inr.h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
pos : 0 < a
⊢ ∃ a', a = a' + 1
Tactic:
exact ⟨a - 1, by rw [sub_add_self_of_le]; exact pos_iff_one_le.mp pos⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_or_succ
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
pos : 0 < a
⊢ a = a - 1 + 1
Tactic:
rw [sub_add_self_of_le]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
pos : 0 < a
⊢ 1 ≤ a
Theorem: LO.FirstOrder.Arith.Model.zero_or_succ
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
pos : 0 < a
⊢ 1 ≤ a
Tactic:
exact pos_iff_one_le.mp pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pred_lt_self_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : 0 < a
⊢ a - 1 < a
Tactic:
rcases zero_or_succ a with (rfl | ⟨a, rfl⟩)
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 ⊧ₘ* 𝐏𝐀⁻
b c : M
h : 0 < 0
⊢ 0 - 1 < 0

case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c a : M
h : 0 < a + 1
⊢ a + 1 - 1 < a + 1
Theorem: LO.FirstOrder.Arith.Model.pred_lt_self_of_pos
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 ⊧ₘ* 𝐏𝐀⁻
b c : M
h : 0 < 0
⊢ 0 - 1 < 0
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pred_lt_self_of_pos
Proof state before:
case inr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c a : M
h : 0 < a + 1
⊢ a + 1 - 1 < a + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ (a - b) * c = a * c - b * c
Tactic:
have : a = (a - b) + b := (tsub_eq_iff_eq_add_of_le h).mp rfl
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b) * c = a * c - b * c
Theorem: LO.FirstOrder.Arith.Model.sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b) * c = a * c - b * c
Tactic:
calc
  (a - b) * c = (a - b) * c + b * c - b * c := by simp
  _           = (a - b + b) * c - b * c     := by simp [add_mul]
  _           = a * c - b * c               := by simp [sub_add_self_of_le h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b) * c = (a - b) * c + b * c - b * c
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b) * c + b * c - b * c = (a - b + b) * c - b * c
Tactic:
simp [add_mul]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sub_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
this : a = a - b + b
⊢ (a - b + b) * c - b * c = a * c - b * c
Tactic:
simp [sub_add_self_of_le h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mul_sub
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : b ≤ a
⊢ c * (a - b) = c * a - c * b
Tactic:
simp [mul_comm c, sub_mul, h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_mul_self_of_pos_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hy : 0 < b
⊢ a ≤ b * a
Tactic:
have : 1 * a ≤ b * a := mul_le_mul_of_nonneg_right (one_le_of_zero_lt b hy) (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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hy : 0 < b
this : 1 * a ≤ b * a
⊢ a ≤ b * a
Theorem: LO.FirstOrder.Arith.Model.le_mul_self_of_pos_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hy : 0 < b
this : 1 * a ≤ b * a
⊢ a ≤ b * a
Tactic:
simpa using this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_mul_self_of_pos_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hy : 0 < b
⊢ 0 ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_mul_self_of_pos_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hy : 0 < b
⊢ a ≤ a * b
Tactic:
simpa [mul_comm a b] using le_mul_self_of_pos_left hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_iff_bounded
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
⊢ a ∣ b ↔ ∃ c ≤ b, b = a * c
Tactic:
by_cases hx : a = 0
Proof state after:
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hx : a = 0
⊢ a ∣ b ↔ ∃ c ≤ b, b = a * c

case neg
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a✝ b✝ c a b : M
hx : ¬a = 0
⊢ a ∣ b ↔ ∃ c ≤ b, b = a * c