internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
⊢ ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₁.get hx
Tactic:
rintro (hy | hy)
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₁
⊢ y = h₁.get hx

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₂
⊢ y = h₁.get hx
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₁
⊢ y = h₁.get hx
Tactic:
exact h₁.get_uniq hx hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₂
⊢ y = h₁.get hx
Tactic:
by_contra
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₂
x✝ : ¬y = h₁.get hx
⊢ False
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₁
y : M
hy : ⟪x, y⟫ ∈ m₂
x✝ : ¬y = h₁.get hx
⊢ False
Tactic:
exact Disjoint.not_of_mem hx (mem_domain_of_pair_mem hy) disjoint
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
⊢ ⟪x, h₂.get hx⟫ ∈ m₁ ∨ ⟪x, h₂.get hx⟫ ∈ m₂
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
⊢ ∀ (y : M), ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₂.get hx
Tactic:
intro y
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
⊢ ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₂.get hx
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
⊢ ⟪x, y⟫ ∈ m₁ ∨ ⟪x, y⟫ ∈ m₂ → y = h₂.get hx
Tactic:
rintro (hy | hy)
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₁
⊢ y = h₂.get hx

case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₂
⊢ y = h₂.get hx
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₁
⊢ y = h₂.get hx
Tactic:
by_contra
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₁
x✝ : ¬y = h₂.get hx
⊢ False
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₁
x✝ : ¬y = h₂.get hx
⊢ False
Tactic:
exact Disjoint.not_of_mem hx (mem_domain_of_pair_mem hy) disjoint.symm
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.union_of_disjoint_domain
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 ⊧ₘ* 𝐈𝚺₁
m₁ m₂ : M
h₁ : IsMapping m₁
h₂ : IsMapping m₂
disjoint : Disjoint (domain m₁) (domain m₂)
x : M
hx : x ∈ domain m₂
y : M
hy : ⟪x, y⟫ ∈ m₂
⊢ y = h₂.get hx
Tactic:
exact h₂.get_uniq hx hy
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.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 ⊧ₘ* 𝐈𝚺₁
x y : M
⊢ IsMapping {⟪x, y⟫}
Tactic:
intro x
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x✝ y x : M
⊢ x ∈ domain {⟪x✝, y⟫} → ∃! y_1, ⟪x, y_1⟫ ∈ {⟪x✝, y⟫}
Theorem: LO.FirstOrder.Arith.Model.IsMapping.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 ⊧ₘ* 𝐈𝚺₁
x✝ y x : M
⊢ x ∈ domain {⟪x✝, y⟫} → ∃! y_1, ⟪x, y_1⟫ ∈ {⟪x✝, y⟫}
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 ⊧ₘ* 𝐈𝚺₁
x✝ y x : M
⊢ x = x✝ → ∃! y_1, x = x✝ ∧ y_1 = y
Theorem: LO.FirstOrder.Arith.Model.IsMapping.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 ⊧ₘ* 𝐈𝚺₁
x✝ y x : M
⊢ x = x✝ → ∃! y_1, x = x✝ ∧ y_1 = y
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 ⊧ₘ* 𝐈𝚺₁
y x : M
⊢ ∃! y_1, x = x ∧ y_1 = y
Theorem: LO.FirstOrder.Arith.Model.IsMapping.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 ⊧ₘ* 𝐈𝚺₁
y x : M
⊢ ∃! y_1, x = x ∧ y_1 = y
Tactic:
exact ExistsUnique.intro y (by simp) (by rintro _ ⟨_, rfl⟩; simp)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.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 ⊧ₘ* 𝐈𝚺₁
y x : M
⊢ x = x ∧ y = y
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.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 ⊧ₘ* 𝐈𝚺₁
y x : M
⊢ ∀ (y_1 : M), x = x ∧ y_1 = y → y_1 = y
Tactic:
rintro _ ⟨_, 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 ⊧ₘ* 𝐈𝚺₁
x y✝ : M
left✝ : x = x
⊢ y✝ = y✝
Theorem: LO.FirstOrder.Arith.Model.IsMapping.singleton
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 ⊧ₘ* 𝐈𝚺₁
x y✝ : M
left✝ : x = x
⊢ y✝ = y✝
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.insert
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 y m : M
h : IsMapping m
disjoint : x ∉ domain m
⊢ IsMapping (Insert.insert ⟪x, y⟫ m)
Tactic:
simp [insert_eq_union_singleton]
Proof state after:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y m : M
h : IsMapping m
disjoint : x ∉ domain m
⊢ IsMapping ({⟪x, y⟫} ∪ m)
Theorem: LO.FirstOrder.Arith.Model.IsMapping.insert
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 y m : M
h : IsMapping m
disjoint : x ∉ domain m
⊢ IsMapping ({⟪x, y⟫} ∪ m)
Tactic:
exact IsMapping.union_of_disjoint_domain (by simp) h (by simpa)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.insert
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 y m : M
h : IsMapping m
disjoint : x ∉ domain m
⊢ IsMapping {⟪x, y⟫}
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.insert
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 y m : M
h : IsMapping m
disjoint : x ∉ domain m
⊢ Disjoint (domain {⟪x, y⟫}) (domain m)
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.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 ⊧ₘ* 𝐈𝚺₁
m m' : M
h : IsMapping m
ss : m' ⊆ m
x : M
hx : x ∈ domain m'
⊢ ∃! y, ⟪x, y⟫ ∈ m'
Tactic:
rcases mem_domain_iff.mp hx with ⟨y, hy⟩
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 ⊧ₘ* 𝐈𝚺₁
m m' : M
h : IsMapping m
ss : m' ⊆ m
x : M
hx : x ∈ domain m'
y : M
hy : ⟪x, y⟫ ∈ m'
⊢ ∃! y, ⟪x, y⟫ ∈ m'
Theorem: LO.FirstOrder.Arith.Model.IsMapping.of_subset
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 ⊧ₘ* 𝐈𝚺₁
m m' : M
h : IsMapping m
ss : m' ⊆ m
x : M
hx : x ∈ domain m'
y : M
hy : ⟪x, y⟫ ∈ m'
⊢ ∃! y, ⟪x, y⟫ ∈ m'
Tactic:
have : ∃! y, ⟪x, y⟫ ∈ m := h x (domain_subset_domain_of_subset ss 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 ⊧ₘ* 𝐈𝚺₁
m m' : M
h : IsMapping m
ss : m' ⊆ m
x : M
hx : x ∈ domain m'
y : M
hy : ⟪x, y⟫ ∈ m'
this : ∃! y, ⟪x, y⟫ ∈ m
⊢ ∃! y, ⟪x, y⟫ ∈ m'
Theorem: LO.FirstOrder.Arith.Model.IsMapping.of_subset
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 ⊧ₘ* 𝐈𝚺₁
m m' : M
h : IsMapping m
ss : m' ⊆ m
x : M
hx : x ∈ domain m'
y : M
hy : ⟪x, y⟫ ∈ m'
this : ∃! y, ⟪x, y⟫ ∈ m
⊢ ∃! y, ⟪x, y⟫ ∈ m'
Tactic:
exact ExistsUnique.intro y hy (fun y' hy' ↦ this.unique (ss hy') (ss hy))
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.restr_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 ⊧ₘ* 𝐈𝚺₁
f s : M
⊢ ∃! g, ∀ (x : M), x ∈ g ↔ x ∈ f ∧ π₁ x ∈ s
Tactic:
have : 𝚺₁-Predicate fun x ↦ x ∈ f ∧ π₁ x ∈ s := 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 ⊧ₘ* 𝐈𝚺₁
f s : M
this : 𝚺₁-Predicate fun x => x ∈ f ∧ π₁ x ∈ s
⊢ ∃! g, ∀ (x : M), x ∈ g ↔ x ∈ f ∧ π₁ x ∈ s
Theorem: LO.FirstOrder.Arith.Model.restr_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 ⊧ₘ* 𝐈𝚺₁
f s : M
this : 𝚺₁-Predicate fun x => x ∈ f ∧ π₁ x ∈ s
⊢ ∃! g, ∀ (x : M), x ∈ g ↔ x ∈ f ∧ π₁ x ∈ s
Tactic:
exact finite_comprehension₁! this
  ⟨f, fun i ↦ by rintro ⟨hi, _⟩; exact lt_of_mem hi⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.restr_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 ⊧ₘ* 𝐈𝚺₁
f s : M
⊢ 𝚺₁-Predicate fun x => x ∈ f ∧ π₁ x ∈ s
Tactic:
definability
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.restr_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 ⊧ₘ* 𝐈𝚺₁
f s : M
this : 𝚺₁-Predicate fun x => x ∈ f ∧ π₁ x ∈ s
i : M
⊢ i ∈ f ∧ π₁ i ∈ s → i < f
Tactic:
rintro ⟨hi, _⟩
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 ⊧ₘ* 𝐈𝚺₁
f s : M
this : 𝚺₁-Predicate fun x => x ∈ f ∧ π₁ x ∈ s
i : M
hi : i ∈ f
right✝ : π₁ i ∈ s
⊢ i < f
Theorem: LO.FirstOrder.Arith.Model.restr_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 ⊧ₘ* 𝐈𝚺₁
f s : M
this : 𝚺₁-Predicate fun x => x ∈ f ∧ π₁ x ∈ s
i : M
hi : i ∈ f
right✝ : π₁ i ∈ s
⊢ i < f
Tactic:
exact lt_of_mem hi
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.pair_mem_restr_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 ⊧ₘ* 𝐈𝚺₁
x y f s : M
⊢ ⟪x, y⟫ ∈ f ↾ s ↔ ⟪x, y⟫ ∈ f ∧ x ∈ s
Tactic:
simp [mem_restr_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.restr_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 ⊧ₘ* 𝐈𝚺₁
f : M
⊢ ∀ (i : M), i ∈ f ↾ ∅ ↔ i ∈ ∅
Tactic:
simp [mem_restr_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.restr_le_self
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f s : M
⊢ f ↾ s ⊆ f
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.IsMapping.restr
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
m : M
h : IsMapping m
s : M
⊢ m ↾ s ⊆ m
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_restr
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f s : M
⊢ ∀ (i : M), i ∈ domain (f ↾ s) ↔ i ∈ domain f ∩ s
Tactic:
simp [mem_domain_iff, pair_mem_restr_iff, exists_and_right, mem_inter_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.domain_restr_of_subset_domain
Proof state before:
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f s : M
h : s ⊆ domain f
⊢ domain (f ↾ s) = s
Tactic:
simp [domain_restr, inter_comm, inter_eq_self_of_subset h]
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.omegaOne.mem_iff
Proof state before:
σ : Sentence ℒₒᵣ
⊢ σ ∈ 𝛀₁ → σ = omegaOneAxiom
Tactic:
rintro ⟨⟩
Proof state after:
case omega

⊢ omegaOneAxiom = omegaOneAxiom
Theorem: LO.FirstOrder.Arith.omegaOne.mem_iff
Proof state before:
case omega

⊢ omegaOneAxiom = omegaOneAxiom
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.omegaOne.mem_iff
Proof state before:
σ : Sentence ℒₒᵣ
⊢ σ = omegaOneAxiom → σ ∈ 𝛀₁
Tactic:
rintro rfl
Proof state after:
⊢ omegaOneAxiom ∈ 𝛀₁
Theorem: LO.FirstOrder.Arith.omegaOne.mem_iff
Proof state before:
⊢ omegaOneAxiom ∈ 𝛀₁
Tactic:
exact Theory.omegaOne.omega
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_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 ⊧ₘ* 𝐈𝚫₀
⊢ M ⊧ₘ omegaOneAxiom ↔ ∀ (x : M), ∃ y, Exponential (‖x‖ ^ 2) y
Tactic:
simp [models_def, omegaOneAxiom, length_defined.df.iff, Exponential.defined.df.iff, sq, ←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 ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1) ↔ ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_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 ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1) ↔ ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
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 ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1) → ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y

case mpr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y) → ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_iff
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 ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1) → ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
Tactic:
intro h x
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 ⊧ₘ* 𝐈𝚫₀
h : ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
x : M
⊢ ∃ y, Exponential (‖x‖ * ‖x‖) y
Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_iff
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 ⊧ₘ* 𝐈𝚫₀
h : ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
x : M
⊢ ∃ y, Exponential (‖x‖ * ‖x‖) y
Tactic:
rcases h x with ⟨y, _, _, rfl, h⟩
Proof state after:
case mp.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 ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
x y : M
left✝ : ‖x‖ ≤ x
h : Exponential (‖x‖ * ‖x‖) y
⊢ ∃ y, Exponential (‖x‖ * ‖x‖) y
Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_iff
Proof state before:
case mp.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 ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
x y : M
left✝ : ‖x‖ ≤ x
h : Exponential (‖x‖ * ‖x‖) y
⊢ ∃ y, Exponential (‖x‖ * ‖x‖) y
Tactic:
exact ⟨y, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_iff
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 ⊧ₘ* 𝐈𝚫₀
⊢ (∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y) → ∀ (x : M), ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
Tactic:
intro h x
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 ⊧ₘ* 𝐈𝚫₀
h : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x : M
⊢ ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_iff
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 ⊧ₘ* 𝐈𝚫₀
h : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x : M
⊢ ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
Tactic:
rcases h x with ⟨y, h⟩
Proof state after:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x y : M
h : Exponential (‖x‖ * ‖x‖) y
⊢ ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_iff
Proof state before:
case mpr.intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x y : M
h : Exponential (‖x‖ * ‖x‖) y
⊢ ∃ x_1, ∃ x_2 ≤ x, x_2 = ‖x‖ ∧ Exponential (x_2 * x_2) x_1
Tactic:
exact ⟨y, ‖x‖, by simp, rfl, h⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.models_Omega₁_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 ⊧ₘ* 𝐈𝚫₀
h✝ : ∀ (x : M), ∃ y, Exponential (‖x‖ * ‖x‖) y
x y : M
h : Exponential (‖x‖ * ‖x‖) y
⊢ ‖x‖ ≤ x
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.exists_unique_exponential_sq_length
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 : M
⊢ ∃! y, Exponential (‖x‖ ^ 2) y
Tactic:
rcases exists_exponential_sq_length x with ⟨y, 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
h : Exponential (‖x‖ ^ 2) y
⊢ ∃! y, Exponential (‖x‖ ^ 2) y
Theorem: LO.FirstOrder.Arith.Model.exists_unique_exponential_sq_length
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
h : Exponential (‖x‖ ^ 2) y
⊢ ∃! y, Exponential (‖x‖ ^ 2) y
Tactic:
exact ExistsUnique.intro y h (fun y' h' ↦ h'.uniq h)
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Model.hash_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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
wlog le : 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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
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 ⊧ₘ* 𝐈𝚫₀ + 𝛀₁] (x y : M), x ≤ y → ∃! z, Exponential (‖x‖ * ‖y‖) z
le : ¬x ≤ y
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z

M✝ : Type u_1
inst✝¹¹ : Zero M✝
inst✝¹⁰ : One M✝
inst✝⁹ : Add M✝
inst✝⁸ : Mul M✝
inst✝⁷ : LT M✝
inst✝⁶ : M✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Theorem: LO.FirstOrder.Arith.Model.hash_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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z
Tactic:
rcases exists_exponential_sq_length y with ⟨z, 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✝ ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
x y : M
le : x ≤ y
z : M
h : Exponential (‖y‖ ^ 2) z
⊢ ∃! z, Exponential (‖x‖ * ‖y‖) z