internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.dvd_iff_bounded
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 a b : M
hx : a = 0
⊢ a ∣ b ↔ ∃ c ≤ b, b = a * c
Tactic:
simp[hx]
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
⊢ b = 0 → ∃ x, x ≤ b
Theorem: LO.FirstOrder.Arith.Model.dvd_iff_bounded
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 a b : M
hx : a = 0
⊢ b = 0 → ∃ x, x ≤ b
Tactic:
rintro rfl
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 : M
hx : a = 0
⊢ ∃ x, x ≤ 0
Theorem: LO.FirstOrder.Arith.Model.dvd_iff_bounded
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 a : M
hx : a = 0
⊢ ∃ x, x ≤ 0
Tactic:
exact ⟨0, by simp⟩
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 : M
hx : a = 0
⊢ 0 ≤ 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_iff_bounded
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 a b : M
hx : ¬a = 0
⊢ a ∣ b ↔ ∃ c ≤ b, b = a * c
Tactic:
constructor
Proof state after:
case neg.mp
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.mpr
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
⊢ (∃ c ≤ b, b = a * c) → a ∣ b
Theorem: LO.FirstOrder.Arith.Model.dvd_iff_bounded
Proof state before:
case neg.mp
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
Tactic:
rintro ⟨c, rfl⟩
Proof state after:
case neg.mp.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✝ a : M
hx : ¬a = 0
c : M
⊢ ∃ c_1 ≤ a * c, a * c = a * c_1
Theorem: LO.FirstOrder.Arith.Model.dvd_iff_bounded
Proof state before:
case neg.mp.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✝ a : M
hx : ¬a = 0
c : M
⊢ ∃ c_1 ≤ a * c, a * c = a * c_1
Tactic:
exact ⟨c, le_mul_self_of_pos_left (pos_iff_ne_zero.mpr hx), rfl⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_iff_bounded
Proof state before:
case neg.mpr
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
⊢ (∃ c ≤ b, b = a * c) → a ∣ b
Tactic:
rintro ⟨c, hz, rfl⟩
Proof state after:
case neg.mpr.intro.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✝ a : M
hx : ¬a = 0
c : M
hz : c ≤ a * c
⊢ a ∣ a * c
Theorem: LO.FirstOrder.Arith.Model.dvd_iff_bounded
Proof state before:
case neg.mpr.intro.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✝ a : M
hx : ¬a = 0
c : M
hz : c ≤ a * c
⊢ a ∣ a * c
Tactic:
exact dvd_mul_right a c
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_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 2 → M
⊢ (fun v => (fun a b => a ∣ b) (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val dvdDef)
Tactic:
simp [dvd_iff_bounded, Matrix.vecHead, Matrix.vecTail, dvdDef]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
h : 0 < b
⊢ a ∣ b → a ≤ b
Tactic:
rintro ⟨c, 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 ⊧ₘ* 𝐏𝐀⁻
a c✝ c : M
h : 0 < a * c
⊢ a ≤ a * c
Theorem: LO.FirstOrder.Arith.Model.le_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 ⊧ₘ* 𝐏𝐀⁻
a c✝ c : M
h : 0 < a * c
⊢ a ≤ a * c
Tactic:
exact le_mul_self_of_pos_right
  (pos_iff_ne_zero.mpr (show c ≠ 0 from by rintro rfl; simp at h))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.le_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 ⊧ₘ* 𝐏𝐀⁻
a c✝ c : M
h : 0 < a * c
⊢ c ≠ 0
Tactic:
rintro 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 c : M
h : 0 < a * 0
⊢ False
Theorem: LO.FirstOrder.Arith.Model.le_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 ⊧ₘ* 𝐏𝐀⁻
a c : M
h : 0 < a * 0
⊢ False
Tactic:
simp at h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_dvd_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
pos : 0 < b
⊢ b < a → ¬a ∣ b
Tactic:
intro hb 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
pos : 0 < b
hb : b < a
h : a ∣ b
⊢ False
Theorem: LO.FirstOrder.Arith.Model.not_dvd_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
pos : 0 < b
hb : b < a
h : a ∣ b
⊢ False
Tactic:
exact not_le.mpr hb (le_of_dvd pos h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_antisymm
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 → a = b
Tactic:
intro hx 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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hx : a ∣ b
hy : b ∣ a
⊢ a = b
Theorem: LO.FirstOrder.Arith.Model.dvd_antisymm
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
hx : a ∣ b
hy : b ∣ a
⊢ a = b
Tactic:
rcases show a = 0 ∨ 0 < a from eq_zero_or_pos a with (rfl | ltx)
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
hx : 0 ∣ b
hy : b ∣ 0
⊢ 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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hx : a ∣ b
hy : b ∣ a
ltx : 0 < a
⊢ a = b
Theorem: LO.FirstOrder.Arith.Model.dvd_antisymm
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
hx : 0 ∣ b
hy : b ∣ 0
⊢ 0 = b
Tactic:
simp [show b = 0 from by simpa using hx]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_antisymm
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
b c : M
hx : 0 ∣ b
hy : b ∣ 0
⊢ b = 0
Tactic:
simpa using hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_antisymm
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 : M
hx : a ∣ b
hy : b ∣ a
ltx : 0 < a
⊢ a = b
Tactic:
rcases show b = 0 ∨ 0 < b from eq_zero_or_pos b with (rfl | lty)
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 ⊧ₘ* 𝐏𝐀⁻
a c : M
ltx : 0 < a
hx : a ∣ 0
hy : 0 ∣ a
⊢ a = 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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hx : a ∣ b
hy : b ∣ a
ltx : 0 < a
lty : 0 < b
⊢ a = b
Theorem: LO.FirstOrder.Arith.Model.dvd_antisymm
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 ⊧ₘ* 𝐏𝐀⁻
a c : M
ltx : 0 < a
hx : a ∣ 0
hy : 0 ∣ a
⊢ a = 0
Tactic:
simp [show a = 0 from by simpa using hy]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_antisymm
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 c : M
ltx : 0 < a
hx : a ∣ 0
hy : 0 ∣ a
⊢ a = 0
Tactic:
simpa using hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_antisymm
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hx : a ∣ b
hy : b ∣ a
ltx : 0 < a
lty : 0 < b
⊢ a = b
Tactic:
exact le_antisymm (le_of_dvd lty hx) (le_of_dvd ltx hy)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a ∣ 1 → a = 1
Tactic:
intro hx
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐏𝐀⁻
a b c : M
hx : a ∣ 1
⊢ a = 1
Theorem: LO.FirstOrder.Arith.Model.dvd_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hx : a ∣ 1
⊢ a = 1
Tactic:
exact dvd_antisymm hx (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
hx : a ∣ 1
⊢ 1 ∣ a
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.dvd_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ a = 1 → a ∣ 1
Tactic:
rintro 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 ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 1 ∣ 1
Theorem: LO.FirstOrder.Arith.Model.dvd_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 ⊧ₘ* 𝐏𝐀⁻
b c : M
⊢ 1 ∣ 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unit_iff_eq_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ IsUnit a → a = 1
Tactic:
rintro ⟨u, 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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
u : Mˣ
⊢ ↑u = 1
Theorem: LO.FirstOrder.Arith.Model.unit_iff_eq_one
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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
u : Mˣ
⊢ ↑u = 1
Tactic:
simp [units_eq_one u]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.unit_iff_eq_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c a : M
⊢ a = 1 → IsUnit a
Tactic:
rintro 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
⊢ IsUnit 1
Theorem: LO.FirstOrder.Arith.Model.unit_iff_eq_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 ⊧ₘ* 𝐏𝐀⁻
a b c : M
⊢ IsUnit 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_one_or_eq_of_dvd_of_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c p a : M
pp : Prime p
hxp : a ∣ p
⊢ a = 1 ∨ a = p
Tactic:
have : p ∣ a ∨ a ∣ 1 := pp.left_dvd_or_dvd_right_of_dvd_mul (show a ∣ p * 1 from by simpa using hxp)
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 p a : M
pp : Prime p
hxp : a ∣ p
this : p ∣ a ∨ a ∣ 1
⊢ a = 1 ∨ a = p
Theorem: LO.FirstOrder.Arith.Model.eq_one_or_eq_of_dvd_of_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c p a : M
pp : Prime p
hxp : a ∣ p
this : p ∣ a ∨ a ∣ 1
⊢ a = 1 ∨ a = p
Tactic:
rcases this with (hx | hx)
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 p a : M
pp : Prime p
hxp : a ∣ p
hx : p ∣ a
⊢ a = 1 ∨ a = p

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 p a : M
pp : Prime p
hxp : a ∣ p
hx : a ∣ 1
⊢ a = 1 ∨ a = p
Theorem: LO.FirstOrder.Arith.Model.eq_one_or_eq_of_dvd_of_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 ⊧ₘ* 𝐏𝐀⁻
a✝ b c p a : M
pp : Prime p
hxp : a ∣ p
⊢ a ∣ p * 1
Tactic:
simpa using hxp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_one_or_eq_of_dvd_of_prime
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 p a : M
pp : Prime p
hxp : a ∣ p
hx : p ∣ a
⊢ a = 1 ∨ a = p
Tactic:
right
Proof state after:
case inl.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 p a : M
pp : Prime p
hxp : a ∣ p
hx : p ∣ a
⊢ a = p
Theorem: LO.FirstOrder.Arith.Model.eq_one_or_eq_of_dvd_of_prime
Proof state before:
case inl.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 p a : M
pp : Prime p
hxp : a ∣ p
hx : p ∣ a
⊢ a = p
Tactic:
exact dvd_antisymm hxp hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.eq_one_or_eq_of_dvd_of_prime
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 p a : M
pp : Prime p
hxp : a ∣ p
hx : a ∣ 1
⊢ a = 1 ∨ a = p
Tactic:
left
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 p a : M
pp : Prime p
hxp : a ∣ p
hx : a ∣ 1
⊢ a = 1
Theorem: LO.FirstOrder.Arith.Model.eq_one_or_eq_of_dvd_of_prime
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 p a : M
pp : Prime p
hxp : a ∣ p
hx : a ∣ 1
⊢ a = 1
Tactic:
exact dvd_one_iff.mp hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.isPrime_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
⊢ 𝚺₀-Predicate fun a => IsPrime a via isPrimedef
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 1 → M
⊢ (fun v => (fun a => IsPrime a) (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val isPrimedef)
Theorem: LO.FirstOrder.Arith.Model.isPrime_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 1 → M
⊢ (fun v => (fun a => IsPrime a) (v 0)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val isPrimedef)
Tactic:
simp [Semiformula.eval_substs, Matrix.comp_vecCons', Matrix.vecHead, Matrix.constant_eq_singleton,
  IsPrime, isPrimedef]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bit_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 ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Relation fun x x_1 => x ∈ x_1 via bitDef
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (fun v => (fun x x_1 => x ∈ x_1) (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val bitDef)
Theorem: LO.FirstOrder.Arith.Model.bit_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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (fun v => (fun x x_1 => x ∈ x_1) (v 0) (v 1)) v ↔ (Semiformula.Evalbm M v) (HSemiformula.val bitDef)
Tactic:
simp [bitDef, ←le_iff_lt_succ]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ∈ v 1 ↔ ∃ x ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)
Theorem: LO.FirstOrder.Arith.Model.bit_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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ∈ v 1 ↔ ∃ x ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ∈ v 1 → ∃ x ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (∃ x ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)) → v 0 ∈ v 1
Theorem: LO.FirstOrder.Arith.Model.bit_defined
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ v 0 ∈ v 1 → ∃ x ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : v 0 ∈ v 1
⊢ ∃ x ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)
Theorem: LO.FirstOrder.Arith.Model.bit_defined
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : v 0 ∈ v 1
⊢ ∃ x ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)
Tactic:
exact ⟨exp (v 0), by simp [h.le], rfl, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bit_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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
h : v 0 ∈ v 1
⊢ exp v 0 ≤ v 1
Tactic:
simp [h.le]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.bit_defined
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
⊢ (∃ x ≤ v 1, x = exp v 0 ∧ LenBit x (v 1)) → v 0 ∈ v 1
Tactic:
rintro ⟨_, _, rfl, h⟩
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
left✝ : exp v 0 ≤ v 1
h : LenBit (exp v 0) (v 1)
⊢ v 0 ∈ v 1
Theorem: LO.FirstOrder.Arith.Model.bit_defined
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 ⊧ₘ* 𝐈𝚺₁
v : Fin 2 → M
left✝ : exp v 0 ≤ v 1
h : LenBit (exp v 0) (v 1)
⊢ v 0 ∈ v 1
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.not_mem_of_lt_exp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i a : M
h : a < exp i
H : i ∈ a
⊢ False
Tactic:
have := lt_of_le_of_lt (exp_le_of_mem H) 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 ⊧ₘ* 𝐈𝚺₁
i a : M
h : a < exp i
H : i ∈ a
this : exp i < exp i
⊢ False
Theorem: LO.FirstOrder.Arith.Model.not_mem_of_lt_exp
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i a : M
h : a < exp i
H : i ∈ a
this : exp i < exp i
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.ball_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∀ x ∈ f v, P v x
Tactic:
have : Definable ℒₒᵣ (Γ, m + 1) (fun v ↦ ∀ x < f v, x ∈ f v → P v x) :=
  .ball_lt hf (.imp (by simpa using Definable.comp₂ (by simp) (hf.retraction _) (by simp)) 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 ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∀ x < f v, x ∈ f v → P v x
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∀ x ∈ f v, P v x
Theorem: LO.FirstOrder.Arith.Model.Definable.ball_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
this : Definable ℒₒᵣ (Γ, m + 1) fun v => ∀ x < f v, x ∈ f v → P v x
⊢ Definable ℒₒᵣ (Γ, m + 1) fun v => ∀ x ∈ f v, P v x
Tactic:
exact this.of_iff <| by intro v; exact ⟨fun h x _ hxv ↦ h x hxv, fun h x hx ↦ h x (lt_of_mem hx) hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.ball_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ Definable ℒₒᵣ (Γ.alt, m + 1) fun w => w 0 ∈ f fun x => w x.succ
Tactic:
simpa using Definable.comp₂ (by simp) (hf.retraction _) (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.ball_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ DefinableFunction ℒₒᵣ (𝚺, m + 1) fun w => w 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.Definable.ball_mem
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
k : ℕ
Γ : SigmaPiDelta
m : ℕ
P : (Fin k → M) → M → Prop
f : (Fin k → M) → M
hf : DefinableFunction ℒₒᵣ (𝚺, m + 1) f
h : Definable ℒₒᵣ (Γ, m + 1) fun w => P (fun x => w x.succ) (w 0)
⊢ (Γ.alt, m + 1)-Relation Membership.mem
Tactic:
simp
Proof state after:
no goals