internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.mod_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 m : M
pos : 0 < m
⊢ (a + b) % m = (m * (a / m) + a % m + (m * (b / m) + b % m)) % m
Tactic:
simp [div_add_mod]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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 m : M
pos : 0 < m
⊢ (m * (a / m) + a % m + (m * (b / m) + b % m)) % m = (m * (a / m) + m * (b / m) + a % m + b % m) % m
Tactic:
simp [←add_assoc, add_right_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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 m : M
pos : 0 < m
⊢ (m * (a / m) + m * (b / m) + a % m + b % m) % m = (a % m + b % m) % m
Tactic:
simp [add_assoc, pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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 : M
pos : 0 < m
⊢ a * b % m = (m * (a / m) + a % m) * (m * (b / m) + b % m) % m
Tactic:
simp [div_add_mod]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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 : M
pos : 0 < m
⊢ (m * (a / m) + a % m) * (m * (b / m) + b % m) % m = a % m * (b % m) % m
Tactic:
simp [add_mul, mul_add, pos, mul_left_comm _ m, add_assoc, mul_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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
⊢ a % b / b = 0
Tactic:
rcases zero_le b 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 : 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
pos : 0 < b
⊢ a % b / b = 0
Theorem: LO.FirstOrder.Arith.Model.mod_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
a : M
⊢ a % 0 / 0 = 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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 b : M
pos : 0 < b
⊢ a % b / b = 0
Tactic:
exact div_eq_zero_of_lt b (by simp [pos])
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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 < b
Tactic:
simp [pos]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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 < 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_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
⊢ 0 < 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_two_not_zero_iff
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 = 0 ↔ a % 2 = 1
Tactic:
rcases mod_two a with (h | h) <;> simp [*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mod_two_not_one_iff
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 = 1 ↔ a % 2 = 0
Tactic:
rcases mod_two a with (h | h) <;> simp [*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
⊢ 2 ∣ a * b → 2 ∣ a ∨ 2 ∣ 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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
H : 2 ∣ a * b
⊢ 2 ∣ a ∨ 2 ∣ b
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
⊢ 2 ∣ a ∨ 2 ∣ 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
H : 2 ∣ a * b
A : ¬(2 ∣ a ∨ 2 ∣ b)
⊢ False
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬(2 ∣ a ∨ 2 ∣ b)
⊢ False
Tactic:
simp [not_or] at 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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
⊢ False
Tactic:
have ha : a % 2 = 1 := by
  have : a % 2 = 0 ∨ a % 2 = 1 := mod_two a
  simpa [show a % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.1] 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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
⊢ False
Tactic:
have hb : b % 2 = 1 := by
  have : b % 2 = 0 ∨ b % 2 = 1 :=
    le_one_iff_eq_zero_or_one.mp <| lt_two_iff_le_one.mp <| mod_lt b (b := 2) (by simp)
  simpa [show b % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.2] 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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
⊢ False
Tactic:
have : a * b % 2 = 1 := by simp [mod_mul, ha, 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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this : a * b % 2 = 1
⊢ False
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this : a * b % 2 = 1
⊢ False
Tactic:
have : ¬2 ∣ a * b := by simp [←mod_eq_zero_iff_dvd, 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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this✝ : a * b % 2 = 1
this : ¬2 ∣ a * b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this✝ : a * b % 2 = 1
this : ¬2 ∣ a * b
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
⊢ a % 2 = 1
Tactic:
have : a % 2 = 0 ∨ a % 2 = 1 := mod_two 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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
this : a % 2 = 0 ∨ a % 2 = 1
⊢ a % 2 = 1
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
this : a % 2 = 0 ∨ a % 2 = 1
⊢ a % 2 = 1
Tactic:
simpa [show a % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.1] using this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
this : a % 2 = 0 ∨ a % 2 = 1
⊢ a % 2 ≠ 0
Tactic:
simpa [←mod_eq_zero_iff_dvd] using A.1
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
⊢ b % 2 = 1
Tactic:
have : b % 2 = 0 ∨ b % 2 = 1 :=
  le_one_iff_eq_zero_or_one.mp <| lt_two_iff_le_one.mp <| mod_lt b (b := 2) (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 : M
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
this : b % 2 = 0 ∨ b % 2 = 1
⊢ b % 2 = 1
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
this : b % 2 = 0 ∨ b % 2 = 1
⊢ b % 2 = 1
Tactic:
simpa [show b % 2 ≠ 0 from by simpa [←mod_eq_zero_iff_dvd] using A.2] using this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
⊢ 0 < 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
this : b % 2 = 0 ∨ b % 2 = 1
⊢ b % 2 ≠ 0
Tactic:
simpa [←mod_eq_zero_iff_dvd] using A.2
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
⊢ a * b % 2 = 1
Tactic:
simp [mod_mul, ha, hb]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_dvd_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
H : 2 ∣ a * b
A : ¬2 ∣ a ∧ ¬2 ∣ b
ha : a % 2 = 1
hb : b % 2 = 1
this : a * b % 2 = 1
⊢ ¬2 ∣ a * b
Tactic:
simp [←mod_eq_zero_iff_dvd, this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.even_or_odd
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) ∨ a = 2 * (a / 2) + 1
Tactic:
have : 2 * (a / 2) + (a % 2) = a := div_add_mod a 2
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 : 2 * (a / 2) + a % 2 = a
⊢ a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1
Theorem: LO.FirstOrder.Arith.Model.even_or_odd
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 : 2 * (a / 2) + a % 2 = a
⊢ a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1
Tactic:
rcases mod_two a with (e | e) <;> { simp[e] at this; simp [this] }
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.even_or_odd
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
this : 2 * (a / 2) + a % 2 = a
e : a % 2 = 1
⊢ a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1
Tactic:
simp[e] at this
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 : M
e : a % 2 = 1
this : 2 * (a / 2) + 1 = a
⊢ a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1
Theorem: LO.FirstOrder.Arith.Model.even_or_odd
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
e : a % 2 = 1
this : 2 * (a / 2) + 1 = a
⊢ a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1
Tactic:
simp [this]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.even_or_odd'
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) ∨ a = 2 * (a / 2) + 1
Tactic:
have : 2 * (a / 2) + (a % 2) = a := div_add_mod a 2
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 : 2 * (a / 2) + a % 2 = a
⊢ a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1
Theorem: LO.FirstOrder.Arith.Model.even_or_odd'
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 : 2 * (a / 2) + a % 2 = a
⊢ a = 2 * (a / 2) ∨ a = 2 * (a / 2) + 1
Tactic:
rcases mod_two a with (e | e) <;>  simp [e] at this <;> simp [*]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_prime
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
⊢ 2 ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_prime
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
⊢ ¬IsUnit 2
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.two_prime
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), 2 ∣ a * b → 2 ∣ a ∨ 2 ∣ b
Tactic:
intro a b 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 ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a b : M
h : 2 ∣ a * b
⊢ 2 ∣ a ∨ 2 ∣ b
Theorem: LO.FirstOrder.Arith.Model.two_prime
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 : 2 ∣ a * b
⊢ 2 ∣ a ∨ 2 ∣ b
Tactic:
exact two_dvd_mul h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 : M
⊢ ∃! x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Tactic:
have : ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1) := by
  have : a < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1) := by
    simpa using open_leastNumber (P := λ x ↦ x * x ≤ a) ⟨“x | x * x ≤ &a”, by simp, by simp⟩
  have hn : a < (a + 1) * (a + 1) := calc
    a ≤ a * a             := le_mul_self a
    _ < a * a + 1         := lt_add_one (a * a)
    _ ≤ (a + 1) * (a + 1) := by simp [add_mul_self_eq]
  exact this hn
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 : ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
⊢ ∃! x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 : M
this : ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
⊢ ∃! x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Tactic:
rcases this with ⟨x, hx⟩
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
⊢ ∃! x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 : M
⊢ ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Tactic:
have : a < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1) := by
  simpa using open_leastNumber (P := λ x ↦ x * x ≤ a) ⟨“x | x * x ≤ &a”, by simp, 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 < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
⊢ ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 : M
this : a < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
⊢ ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Tactic:
have hn : a < (a + 1) * (a + 1) := calc
  a ≤ a * a             := le_mul_self a
  _ < a * a + 1         := lt_add_one (a * a)
  _ ≤ (a + 1) * (a + 1) := by simp [add_mul_self_eq]
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 < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
hn : a < (a + 1) * (a + 1)
⊢ ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 : M
this : a < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
hn : a < (a + 1) * (a + 1)
⊢ ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Tactic:
exact this hn
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 : M
⊢ a < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
Tactic:
simpa using open_leastNumber (P := λ x ↦ x * x ≤ a) ⟨“x | x * x ≤ &a”, by simp, by simp⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 : M
⊢ “(#0 * #0) ≤ &a”.Open
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 : M
⊢ ∀ (x : M), (fun x => x * x ≤ a) x ↔ (Semiformula.Evalm M ![x] id) (“(#0 * #0) ≤ &a”)
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 : M
this : a < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
⊢ a * a + 1 ≤ (a + 1) * (a + 1)
Tactic:
simp [add_mul_self_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
⊢ ∀ (y : M), y * y ≤ a ∧ a < (y + 1) * (y + 1) → y = x
Tactic:
intro y hy
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
⊢ y = x
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
⊢ y = x
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sqrt_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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
⊢ False
Tactic:
wlog lt : x < y
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
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 : M ⊧ₘ* 𝐈open] (a x : M),
    x * x ≤ a ∧ a < (x + 1) * (x + 1) → ∀ (y : M), y * y ≤ a ∧ a < (y + 1) * (y + 1) → ¬y = x → x < y → False
lt : ¬x < y
⊢ False

M✝ : Type u_1
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
lt : x < y
⊢ False
Theorem: LO.FirstOrder.Arith.Model.sqrt_exists_unique
Proof state before:
M✝ : Type u_1
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
lt : x < y
⊢ False
Tactic:
have : a < a := calc
  a < (x + 1) * (x + 1) := hx.2
  _ ≤ y * y             := mul_self_le_mul_self (by simp) (lt_iff_succ_le.mp lt)
  _ ≤ a                 := hy.1
Proof state after:
M✝ : Type u_1
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 x : M
hx : x * x ≤ a ∧ a < (x + 1) * (x + 1)
y : M
hy : y * y ≤ a ∧ a < (y + 1) * (y + 1)
ne : ¬y = x
lt : x < y
this : a < a
⊢ False