internlm/Lean-Github huggingface dataset:
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
⊢ 0 < 2
Tactic:
simp
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
this : a < 2 * (a / 2 + 1)
⊢ a < 2 * (a / 2) + 1 + 1
Tactic:
simpa [add_assoc, one_add_one_eq_two, mul_add] using this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_monotone
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
h : a ≤ b
c : M
⊢ a / c ≤ b / c
Tactic:
rcases zero_le c 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
a b : M
h : a ≤ b
⊢ a / 0 ≤ b / 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 b : M
h : a ≤ b
c : M
pos : 0 < c
⊢ a / c ≤ b / c
Theorem: LO.FirstOrder.Arith.Model.div_monotone
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
h : a ≤ b
c : M
pos : 0 < c
⊢ a / c ≤ b / c
Tactic:
by_contra A
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
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
⊢ False
Theorem: LO.FirstOrder.Arith.Model.div_monotone
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
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
⊢ False
Tactic:
have : b / c + 1 ≤ a / c := succ_le_iff_lt.mpr (by simpa using A)
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
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
this : b / c + 1 ≤ a / c
⊢ False
Theorem: LO.FirstOrder.Arith.Model.div_monotone
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
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
this : b / c + 1 ≤ a / c
⊢ False
Tactic:
have : a < a := calc
  a ≤ b               := h
  _ < c * (b / c + 1) := lt_mul_div b pos
  _ ≤ c * (a / c)     := mul_le_mul_left this
  _ ≤ a               := mul_div_le a c
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
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
this✝ : b / c + 1 ≤ a / c
this : a < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.div_monotone
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
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
this✝ : b / c + 1 ≤ a / c
this : a < a
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_monotone
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
h : a ≤ b
⊢ a / 0 ≤ b / 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_monotone
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
h : a ≤ b
c : M
pos : 0 < c
A : ¬a / c ≤ b / c
⊢ b / c < a / c
Tactic:
simpa using A
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_lt_of_lt_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
h : a < b * c
⊢ a / c < b
Tactic:
by_contra 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 c : M
h : a < b * c
hb : ¬a / c < b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.div_lt_of_lt_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
h : a < b * c
hb : ¬a / c < b
⊢ False
Tactic:
simp at 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 c : M
h : a < b * c
hb : b ≤ a / c
⊢ False
Theorem: LO.FirstOrder.Arith.Model.div_lt_of_lt_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
h : a < b * c
hb : b ≤ a / c
⊢ False
Tactic:
have : a < a := calc
  a < b * c     := h
  _ ≤ a / c * c := mul_le_mul_right hb
  _ ≤ a         := 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 b c : M
h : a < b * c
hb : b ≤ a / c
this : a < a
⊢ False
Theorem: LO.FirstOrder.Arith.Model.div_lt_of_lt_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
h : a < b * c
hb : b ≤ a / c
this : a < a
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_lt_of_lt_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
h : a < b * c
hb : b ≤ a / c
⊢ a / c * c ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_cancel_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
c : M
pos : 0 < c
a b : M
⊢ c * a / (c * b) = a / b
Tactic:
simp [div_mul, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.div_cancel_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
c : M
pos : 0 < c
a b : M
⊢ a * c / (b * c) = a / b
Tactic:
simp [mul_comm _ c, div_cancel_left pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_mul_add_one_div_two
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
⊢ (2 * a + 1) / 2 = a
Tactic:
simp [div_mul_add_self', one_lt_two]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.rem_graph
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 ↔ ∃ x ≤ b, x = b / c ∧ a = b - c * x
Tactic:
simp [mod_def]
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
⊢ a = b - c * (b / c) ↔ ∃ x ≤ b, x = b / c ∧ a = b - c * x
Theorem: LO.FirstOrder.Arith.Model.rem_graph
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 * (b / c) ↔ ∃ x ≤ b, x = b / c ∧ a = b - c * x
Tactic:
constructor
Proof state after:
case 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 c : M
⊢ a = b - c * (b / c) → ∃ x ≤ b, x = b / c ∧ a = b - c * x

case 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 c : M
⊢ (∃ x ≤ b, x = b / c ∧ a = b - c * x) → a = b - c * (b / c)
Theorem: LO.FirstOrder.Arith.Model.rem_graph
Proof state before:
case 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 c : M
⊢ a = b - c * (b / c) → ∃ x ≤ b, x = b / c ∧ a = b - c * x
Tactic:
rintro rfl
Proof state after:
case 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
b c : M
⊢ ∃ x ≤ b, x = b / c ∧ b - c * (b / c) = b - c * x
Theorem: LO.FirstOrder.Arith.Model.rem_graph
Proof state before:
case 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
b c : M
⊢ ∃ x ≤ b, x = b / c ∧ b - c * (b / c) = b - c * x
Tactic:
exact ⟨b / c, by simp, rfl, by rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.rem_graph
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 c : M
⊢ b / c ≤ b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.rem_graph
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 c : M
⊢ b - c * (b / c) = b - c * (b / c)
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.rem_graph
Proof state before:
case 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 c : M
⊢ (∃ x ≤ b, x = b / c ∧ a = b - c * x) → a = b - c * (b / c)
Tactic:
rintro ⟨_, _, rfl, rfl⟩
Proof state after:
case mpr.intro.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
b c : M
left✝ : b / c ≤ b
⊢ b - c * (b / c) = b - c * (b / c)
Theorem: LO.FirstOrder.Arith.Model.rem_graph
Proof state before:
case mpr.intro.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
b c : M
left✝ : b / c ≤ b
⊢ b - c * (b / c) = b - c * (b / c)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.rem_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 remDef
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 remDef)
Theorem: LO.FirstOrder.Arith.Model.rem_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 remDef)
Tactic:
simp [Matrix.vecHead, Matrix.vecTail, remDef, rem_graph, Semiformula.eval_substs, le_iff_lt_succ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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
⊢ a % 0 = a
Tactic:
simp [mod_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.zero_mod
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:
simp [mod_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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
⊢ a % a = 0
Tactic:
rcases zero_le a with (rfl | h)
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
h : 0 < a
⊢ a % a = 0
Theorem: LO.FirstOrder.Arith.Model.mod_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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
⊢ 0 % 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a : M
h : 0 < a
⊢ a % a = 0
Tactic:
simp [mod_def, h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_mul_add_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
a b r : M
hr : r < b
⊢ (a * b + r) % b = r
Tactic:
simp [mod_def, div_mul_add a b hr, mul_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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
b a c : M
pos : 0 < b
⊢ (a * b + c) % b = c % b
Tactic:
simp [mod_def, div_mul_add_self, pos, mul_add, ←sub_sub, show b * a = a * b from mul_comm _ _]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_add_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
c a b : M
pos : 0 < c
⊢ (a + b * c) % c = a % c
Tactic:
simp [add_comm a (b * c), pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_add_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
c a b : M
pos : 0 < c
⊢ (a + c * b) % c = a % c
Tactic:
simp [mul_comm c b, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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
b a c : M
pos : 0 < b
⊢ (b * a + c) % b = c % b
Tactic:
simp [mul_comm b a, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_mul_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 b : M
⊢ a * b % b = 0
Tactic:
rcases zero_le b with (rfl | h)
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 : M
⊢ a * 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 b : M
h : 0 < b
⊢ a * b % b = 0
Theorem: LO.FirstOrder.Arith.Model.mod_mul_self_left
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 : M
⊢ a * 0 % 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_mul_self_left
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
h : 0 < b
⊢ a * b % b = 0
Tactic:
simpa using mod_mul_add_of_lt a b h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_mul_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
⊢ b * a % b = 0
Tactic:
simp [mul_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_eq_self_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
a b : M
h : a < b
⊢ a % b = a
Tactic:
simpa using mod_mul_add_of_lt 0 b h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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
pos : 0 < b
⊢ a % b < b
Tactic:
rcases div_spec_of_pos' a pos with ⟨r, hr, ha⟩
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
r : M
hr : r < b
ha : a = a / b * b + r
⊢ a % b < b
Theorem: LO.FirstOrder.Arith.Model.mod_lt
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
r : M
hr : r < b
ha : a = a / b * b + r
⊢ a % b < b
Tactic:
have : ((a / b) * b + r) % b = r := mod_mul_add_of_lt _ _ hr
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
r : M
hr : r < b
ha : a = a / b * b + r
this : (a / b * b + r) % b = r
⊢ a % b < b
Theorem: LO.FirstOrder.Arith.Model.mod_lt
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
r : M
hr : r < b
ha : a = a / b * b + r
this : (a / b * b + r) % b = r
⊢ a % b < b
Tactic:
have : a % b = r := by simpa [←ha] using this
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
r : M
hr : r < b
ha : a = a / b * b + r
this✝ : (a / b * b + r) % b = r
this : a % b = r
⊢ a % b < b
Theorem: LO.FirstOrder.Arith.Model.mod_lt
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
r : M
hr : r < b
ha : a = a / b * b + r
this✝ : (a / b * b + r) % b = r
this : a % b = r
⊢ a % b < b
Tactic:
simp [this, hr]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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
pos : 0 < b
r : M
hr : r < b
ha : a = a / b * b + r
this : (a / b * b + r) % b = r
⊢ a % b = r
Tactic:
simpa [←ha] using this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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:
simp [mod_def]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_eq_zero_iff_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
⊢ b % a = 0 ↔ a ∣ b
Tactic:
simp [mod_def]
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) ↔ a ∣ b
Theorem: LO.FirstOrder.Arith.Model.mod_eq_zero_iff_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
⊢ b ≤ a * (b / a) ↔ a ∣ b
Tactic:
constructor
Proof state after:
case 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
⊢ b ≤ a * (b / a) → a ∣ b

case 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
⊢ a ∣ b → b ≤ a * (b / a)
Theorem: LO.FirstOrder.Arith.Model.mod_eq_zero_iff_dvd
Proof state before:
case 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
⊢ b ≤ a * (b / a) → a ∣ b
Tactic:
intro H
Proof state after:
case 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
H : b ≤ a * (b / a)
⊢ a ∣ b
Theorem: LO.FirstOrder.Arith.Model.mod_eq_zero_iff_dvd
Proof state before:
case 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
H : b ≤ a * (b / a)
⊢ a ∣ b
Tactic:
exact mul_div_self_of_dvd.mp (le_antisymm (mul_div_le b a) H)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_eq_zero_iff_dvd
Proof state before:
case 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
⊢ a ∣ b → b ≤ a * (b / a)
Tactic:
intro H
Proof state after:
case 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
H : a ∣ b
⊢ b ≤ a * (b / a)
Theorem: LO.FirstOrder.Arith.Model.mod_eq_zero_iff_dvd
Proof state before:
case 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
H : a ∣ b
⊢ b ≤ a * (b / a)
Tactic:
simp [mul_div_self_of_dvd.mpr H]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_add_remove_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
Tactic:
simpa using mod_add_mul a 1 pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_add_remove_right_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 : M
h : m ∣ b
pos : 0 < m
⊢ (a + b) % m = a % m
Tactic:
rcases h with ⟨b, rfl⟩
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 m : M
pos : 0 < m
b : M
⊢ (a + m * b) % m = a % m
Theorem: LO.FirstOrder.Arith.Model.mod_add_remove_right_of_dvd
Proof state before:
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 m : M
pos : 0 < m
b : M
⊢ (a + m * b) % m = a % m
Tactic:
simp [pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_add_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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
pos : 0 < a
⊢ (a + b) % a = b % a
Tactic:
simpa using mod_mul_add 1 b pos
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_add_remove_left_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 : M
h : m ∣ a
pos : 0 < m
⊢ (a + b) % m = b % m
Tactic:
rcases h with ⟨b, rfl⟩
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
b✝ m : M
pos : 0 < m
b : M
⊢ (m * b + b✝) % m = b✝ % m
Theorem: LO.FirstOrder.Arith.Model.mod_add_remove_left_of_dvd
Proof state before:
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
b✝ m : M
pos : 0 < m
b : M
⊢ (m * b + b✝) % m = b✝ % m
Tactic:
simp [pos]
Proof state after:
no goals