internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.sUnion_graph
Proof state before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u ↔ ∃ c ∈ s, x ∈ c
Tactic:
constructor
Proof state after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u → ∃ c ∈ s, x ∈ c

case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ (∃ c ∈ s, x ∈ c) → x ∈ u
Theorem: LO.FirstOrder.Arith.Model.sUnion_graph
Proof state before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ x ∈ u → ∃ c ∈ s, x ∈ c
Tactic:
intro hx
Proof state after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
hx : x ∈ u
⊢ ∃ c ∈ s, x ∈ c
Theorem: LO.FirstOrder.Arith.Model.sUnion_graph
Proof state before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
hx : x ∈ u
⊢ ∃ c ∈ s, x ∈ c
Tactic:
exact h x (lt_of_lt_of_le (lt_of_mem hx) (by simp)) |>.mp hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_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 ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
hx : x ∈ u
⊢ u ≤ u + s
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_graph
Proof state before:
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x : M
⊢ (∃ c ∈ s, x ∈ c) → x ∈ u
Tactic:
rintro ⟨c, hc, hx⟩
Proof state after:
case h.mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x c : M
hc : c ∈ s
hx : x ∈ c
⊢ x ∈ u
Theorem: LO.FirstOrder.Arith.Model.sUnion_graph
Proof state before:
case h.mpr.intro.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x c : M
hc : c ∈ s
hx : x ∈ c
⊢ x ∈ u
Tactic:
exact h x (lt_of_lt_of_le (lt_trans _ _ _ (lt_of_mem hx) (lt_of_mem hc)) (by simp)) |>.mpr ⟨c, hc, hx⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_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 ⊧ₘ* 𝐈𝚺₁
u s : M
h : ∀ x < u + s, x ∈ u ↔ ∃ t ∈ s, x ∈ t
x c : M
hc : c ∈ s
hx : x ∈ c
⊢ s ≤ u + s
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sUnion_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 ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Function₁ fun x => ⋃ʰᶠ x via sUnionDef
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 (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => (fun x => ⋃ʰᶠ x) (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val sUnionDef)
Theorem: LO.FirstOrder.Arith.Model.sUnion_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 (Nat.succ 1) → M
⊢ (fun v => v 0 = (fun v => (fun x => ⋃ʰᶠ x) (v 0)) fun x => v x.succ) v ↔
    (Semiformula.Evalbm M v) (HSemiformula.val sUnionDef)
Tactic:
simp [sUnionDef, sUnion_graph]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_cup_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 ∈ b ∪ c ↔ a ∈ b ∨ a ∈ c
Tactic:
simp [Union.union, union]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_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 ⊧ₘ* 𝐈𝚺₁
u s t : M
⊢ u = s ∪ t → ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
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 ⊧ₘ* 𝐈𝚺₁
s t : M
⊢ ∀ x < s ∪ t + s + t, x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t
Theorem: LO.FirstOrder.Arith.Model.union_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 ⊧ₘ* 𝐈𝚺₁
s t : M
⊢ ∀ x < s ∪ t + s + t, x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_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 ⊧ₘ* 𝐈𝚺₁
u s t : M
⊢ (∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t) → u = s ∪ t
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 ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
⊢ u = s ∪ t
Theorem: LO.FirstOrder.Arith.Model.union_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 ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
⊢ u = s ∪ t
Tactic:
apply mem_ext
Proof state after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
⊢ ∀ (i : M), i ∈ u ↔ i ∈ s ∪ t
Theorem: LO.FirstOrder.Arith.Model.union_graph
Proof state before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
⊢ ∀ (i : M), i ∈ u ↔ i ∈ s ∪ t
Tactic:
intro x
Proof state after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
⊢ x ∈ u ↔ x ∈ s ∪ t
Theorem: LO.FirstOrder.Arith.Model.union_graph
Proof state before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
⊢ x ∈ u ↔ x ∈ s ∪ t
Tactic:
simp
Proof state after:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
⊢ x ∈ u ↔ x ∈ s ∨ x ∈ t
Theorem: LO.FirstOrder.Arith.Model.union_graph
Proof state before:
case h
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
⊢ x ∈ u ↔ x ∈ s ∨ x ∈ t
Tactic:
constructor
Proof state after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
⊢ x ∈ u → x ∈ s ∨ x ∈ t

case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
⊢ x ∈ s ∨ x ∈ t → x ∈ u
Theorem: LO.FirstOrder.Arith.Model.union_graph
Proof state before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
⊢ x ∈ u → x ∈ s ∨ x ∈ t
Tactic:
intro hx
Proof state after:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
hx : x ∈ u
⊢ x ∈ s ∨ x ∈ t
Theorem: LO.FirstOrder.Arith.Model.union_graph
Proof state before:
case h.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
hx : x ∈ u
⊢ x ∈ s ∨ x ∈ t
Tactic:
exact h x (lt_of_lt_of_le (lt_of_mem hx) (by simp [add_assoc])) |>.mp hx
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_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 ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
hx : x ∈ u
⊢ u ≤ u + s + t
Tactic:
simp [add_assoc]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_graph
Proof state before:
case h.mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
⊢ x ∈ s ∨ x ∈ t → x ∈ u
Tactic:
rintro (hx | hx)
Proof state after:
case h.mpr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
hx : x ∈ s
⊢ x ∈ u

case h.mpr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
hx : x ∈ t
⊢ x ∈ u
Theorem: LO.FirstOrder.Arith.Model.union_graph
Proof state before:
case h.mpr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
hx : x ∈ s
⊢ x ∈ u
Tactic:
exact h x (lt_of_lt_of_le (lt_of_mem hx) (by simp )) |>.mpr (Or.inl hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_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 ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
hx : x ∈ s
⊢ s ≤ u + s + t
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_graph
Proof state before:
case h.mpr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
hx : x ∈ t
⊢ x ∈ u
Tactic:
exact h x (lt_of_lt_of_le (lt_of_mem hx) (by simp )) |>.mpr (Or.inr hx)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_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 ⊧ₘ* 𝐈𝚺₁
u s t : M
h : ∀ x < u + s + t, x ∈ u ↔ x ∈ s ∨ x ∈ t
x : M
hx : x ∈ t
⊢ t ≤ u + s + t
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_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 ⊧ₘ* 𝐈𝚺₁
⊢ 𝚺₀-Function₂ fun x x_1 => x ∪ x_1 via unionDef
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 (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 unionDef)
Theorem: LO.FirstOrder.Arith.Model.union_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 (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 unionDef)
Tactic:
simp [unionDef, union_graph]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.insert_eq_union_singleton
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 s x : M
⊢ x ∈ insert a s ↔ x ∈ {a} ∪ s
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 : M
⊢ 0 < 2 * (a + b) + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 : M
⊢ ∀ i ∈ a ∪ b, i < log (2 * (a + b) + 1)
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 : M
⊢ ∀ (i : M), i ∈ a ∨ i ∈ b → i < log (2 * (a + b) + 1)
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 : M
⊢ ∀ (i : M), i ∈ a ∨ i ∈ b → i < log (2 * (a + b) + 1)
Tactic:
rintro i (hi | hi)
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 i : M
hi : i ∈ a
⊢ i < log (2 * (a + b) + 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 i : M
hi : i ∈ b
⊢ i < log (2 * (a + b) + 1)
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ a
⊢ i < log (2 * (a + b) + 1)
Tactic:
calc
  i ≤ log (a + b) := le_trans (le_log_of_mem hi) (log_monotone (by simp))
  _ < log (2 * (a + b)) := by simp [log_two_mul_of_pos (show 0 < a + b from by simp [pos_of_nonempty hi])]
  _ ≤ log (2 * (a + b) + 1) := log_monotone (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ a
⊢ a ≤ a + b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ a
⊢ log (a + b) < log (2 * (a + b))
Tactic:
simp [log_two_mul_of_pos (show 0 < a + b from by simp [pos_of_nonempty hi])]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ a
⊢ 0 < a + b
Tactic:
simp [pos_of_nonempty hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ a
⊢ 2 * (a + b) ≤ 2 * (a + b) + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ b
⊢ i < log (2 * (a + b) + 1)
Tactic:
calc
  i ≤ log (a + b) := le_trans (le_log_of_mem hi) (log_monotone (by simp))
  _ < log (2 * (a + b)) := by simp [log_two_mul_of_pos (show 0 < a + b from by simp [pos_of_nonempty hi])]
  _ ≤ log (2 * (a + b) + 1) := log_monotone (by simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ b
⊢ b ≤ a + b
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ b
⊢ log (a + b) < log (2 * (a + b))
Tactic:
simp [log_two_mul_of_pos (show 0 < a + b from by simp [pos_of_nonempty hi])]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ b
⊢ 0 < a + b
Tactic:
simp [pos_of_nonempty hi]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_polybound
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 i : M
hi : i ∈ b
⊢ 2 * (a + b) ≤ 2 * (a + b) + 1
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.union_comm
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 : M
⊢ ∀ (i : M), i ∈ a ∪ b ↔ i ∈ b ∪ a
Tactic:
simp [or_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sInter_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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ ∃! u, ∀ (x : M), x ∈ u ↔ s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
Tactic:
have : 𝚺₁-Predicate fun x ↦ s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t := by definability
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
⊢ ∃! u, ∀ (x : M), x ∈ u ↔ s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
Theorem: LO.FirstOrder.Arith.Model.sInter_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 ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
⊢ ∃! u, ∀ (x : M), x ∈ u ↔ s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
Tactic:
exact finite_comprehension₁! this
  ⟨s, fun i ↦ by
    rintro ⟨hs, h⟩
    have : log s ∈ s := log_mem_of_pos <| pos_iff_ne_zero.mpr hs
    exact _root_.trans (lt_of_mem <| h (log s) this) (lt_of_mem this)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sInter_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 ⊧ₘ* 𝐈𝚺₁
s : M
⊢ 𝚺₁-Predicate fun x => s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.sInter_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 ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
i : M
⊢ (s ≠ ∅ ∧ ∀ t ∈ s, i ∈ t) → i < s
Tactic:
rintro ⟨hs, h⟩
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 ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
i : M
hs : s ≠ ∅
h : ∀ t ∈ s, i ∈ t
⊢ i < s
Theorem: LO.FirstOrder.Arith.Model.sInter_exists_unique
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 ⊧ₘ* 𝐈𝚺₁
s : M
this : 𝚺₁-Predicate fun x => s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
i : M
hs : s ≠ ∅
h : ∀ t ∈ s, i ∈ t
⊢ i < s
Tactic:
have : log s ∈ s := log_mem_of_pos <| pos_iff_ne_zero.mpr hs
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 ⊧ₘ* 𝐈𝚺₁
s : M
this✝ : 𝚺₁-Predicate fun x => s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
i : M
hs : s ≠ ∅
h : ∀ t ∈ s, i ∈ t
this : log s ∈ s
⊢ i < s
Theorem: LO.FirstOrder.Arith.Model.sInter_exists_unique
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 ⊧ₘ* 𝐈𝚺₁
s : M
this✝ : 𝚺₁-Predicate fun x => s ≠ ∅ ∧ ∀ t ∈ s, x ∈ t
i : M
hs : s ≠ ∅
h : ∀ t ∈ s, i ∈ t
this : log s ∈ s
⊢ i < s
Tactic:
exact _root_.trans (lt_of_mem <| h (log s) this) (lt_of_mem this)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_sInter_iff_empty
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 : M), i ∈ ⋂ʰᶠ ∅ ↔ i ∈ ∅
Tactic:
simp [mem_sInter_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_sInter_iff_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 ⊧ₘ* 𝐈𝚺₁
x s : M
h : s ≠ ∅
⊢ x ∈ ⋂ʰᶠ s ↔ ∀ t ∈ s, x ∈ t
Tactic:
simp [mem_sInter_iff, h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_inter_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 ∈ b ∩ c ↔ a ∈ b ∧ a ∈ c
Tactic:
simp [Inter.inter, inter, mem_sInter_iff_of_pos (s := {b, c}) (nonempty_iff.mpr ⟨b, by simp⟩)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.mem_inter_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
⊢ b ∈ {b, c}
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.inter_comm
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 : M
⊢ ∀ (i : M), i ∈ a ∩ b ↔ i ∈ b ∩ a
Tactic:
simp [and_comm]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.inter_eq_self_of_subset
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 : M
h : a ⊆ b
⊢ ∀ (i : M), i ∈ a ∩ b ↔ i ∈ a
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 : M
h : a ⊆ b
⊢ ∀ i ∈ a, i ∈ b
Theorem: LO.FirstOrder.Arith.Model.inter_eq_self_of_subset
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 : M
h : a ⊆ b
⊢ ∀ i ∈ a, i ∈ b
Tactic:
intro i hi
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 : M
h : a ⊆ b
i : M
hi : i ∈ a
⊢ i ∈ b
Theorem: LO.FirstOrder.Arith.Model.inter_eq_self_of_subset
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 : M
h : a ⊆ b
i : M
hi : i ∈ a
⊢ i ∈ b
Tactic:
exact h hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.product_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 ⊧ₘ* 𝐈𝚺₁
a b : M
⊢ ∃! u, ∀ (x : M), x ∈ u ↔ ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫
Tactic:
have : 𝚺₁-Predicate fun x ↦ ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫ := by definability
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 : M
this : 𝚺₁-Predicate fun x => ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫
⊢ ∃! u, ∀ (x : M), x ∈ u ↔ ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫
Theorem: LO.FirstOrder.Arith.Model.product_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 ⊧ₘ* 𝐈𝚺₁
a b : M
this : 𝚺₁-Predicate fun x => ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫
⊢ ∃! u, ∀ (x : M), x ∈ u ↔ ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫
Tactic:
exact finite_comprehension₁! this
  ⟨⟪log a, log b⟫ + 1, fun i ↦ by
    rintro ⟨y, hy, z, hz, rfl⟩
    simp [lt_succ_iff_le]
    exact pair_le_pair (le_log_of_mem hy) (le_log_of_mem hz)⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.product_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 ⊧ₘ* 𝐈𝚺₁
a b : M
⊢ 𝚺₁-Predicate fun x => ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.product_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 ⊧ₘ* 𝐈𝚺₁
a b : M
this : 𝚺₁-Predicate fun x => ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫
i : M
⊢ (∃ y ∈ a, ∃ z ∈ b, i = ⟪y, z⟫) → i < ⟪log a, log b⟫ + 1
Tactic:
rintro ⟨y, hy, z, hz, rfl⟩
Proof state after:
case intro.intro.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 : M
this : 𝚺₁-Predicate fun x => ∃ y ∈ a, ∃ z ∈ b, x = ⟪y, z⟫
y : M
hy : y ∈ a
z : M
hz : z ∈ b
⊢ ⟪y, z⟫ < ⟪log a, log b⟫ + 1