internlm/Lean-Github huggingface dataset:
Theorem: Partrec.mergep
Proof state before:
case H
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
pk : Partrec k
hk : ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a
a✝ : α
a : σ
⊢ a ∈ k a✝ ↔ a ∈ f.merge g a✝
Tactic:
simp[hk, merge_iff hf hg H]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.HomClass.val_term
Proof state before:
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : HomClass F L M₁ M₂
φ : F
n : ℕ
μ : Type u_6
e : Fin n → M₁
ε : μ → M₁
t : Semiterm L μ n
⊢ φ (Semiterm.val s₁ e ε t) = Semiterm.val s₂ (⇑φ ∘ e) (⇑φ ∘ ε) t
Tactic:
induction t <;> simp [*, Semiterm.val_func, HomClass.func, Function.comp]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_hom_iff_of_open
Proof state before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝¹ : ℕ
e₁ : Fin x✝¹ → M₁
ε₁ : μ → M₁
x✝ : ⊤.Open
⊢ (Eval s₁ e₁ ε₁) ⊤ ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_hom_iff_of_open
Proof state before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝¹ : ℕ
e₁ : Fin x✝¹ → M₁
ε₁ : μ → M₁
x✝ : ⊥.Open
⊢ (Eval s₁ e₁ ε₁) ⊥ ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) ⊥
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_hom_iff_of_open
Proof state before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝¹ : ℕ
e₁ : Fin x✝¹ → M₁
ε₁ : μ → M₁
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝¹
x✝ : (rel r v).Open
⊢ (Eval s₁ e₁ ε₁) (rel r v) ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) (rel r v)
Tactic:
simp [Function.comp, eval_rel, ←EmbeddingClass.rel φ, HomClass.val_term]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_hom_iff_of_open
Proof state before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝¹ : ℕ
e₁ : Fin x✝¹ → M₁
ε₁ : μ → M₁
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝¹
x✝ : (nrel r v).Open
⊢ (Eval s₁ e₁ ε₁) (nrel r v) ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) (nrel r v)
Tactic:
simp [Function.comp, eval_nrel, ←EmbeddingClass.rel φ, HomClass.val_term]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_hom_iff_of_open
Proof state before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : (p ⋏ q).Open
⊢ (Eval s₁ e₁ ε₁) (p ⋏ q) ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) (p ⋏ q)
Tactic:
simp at h ⊢
Proof state after:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : p.Open ∧ q.Open
⊢ (Eval s₁ e₁ ε₁) p ∧ (Eval s₁ e₁ ε₁) q ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) p ∧ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) q
Theorem: LO.FirstOrder.Semiformula.eval_hom_iff_of_open
Proof state before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : p.Open ∧ q.Open
⊢ (Eval s₁ e₁ ε₁) p ∧ (Eval s₁ e₁ ε₁) q ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) p ∧ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) q
Tactic:
simp [eval_hom_iff_of_open h.1, eval_hom_iff_of_open h.2]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_hom_iff_of_open
Proof state before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : (p ⋎ q).Open
⊢ (Eval s₁ e₁ ε₁) (p ⋎ q) ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) (p ⋎ q)
Tactic:
simp at h ⊢
Proof state after:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : p.Open ∧ q.Open
⊢ (Eval s₁ e₁ ε₁) p ∨ (Eval s₁ e₁ ε₁) q ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) p ∨ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) q
Theorem: LO.FirstOrder.Semiformula.eval_hom_iff_of_open
Proof state before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : p.Open ∧ q.Open
⊢ (Eval s₁ e₁ ε₁) p ∨ (Eval s₁ e₁ ε₁) q ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) p ∨ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) q
Tactic:
simp [eval_hom_iff_of_open h.1, eval_hom_iff_of_open h.2]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_hom_univClosure
Proof state before:
n✝ : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁ : Fin n✝ → M₁
ε₁✝ : μ → M₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
⊢ (Evalf s₂ (⇑φ ∘ ε₁)) (∀* p) → (Evalf s₁ ε₁) (∀* p)
Tactic:
simp
Proof state after:
n✝ : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁ : Fin n✝ → M₁
ε₁✝ : μ → M₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
⊢ (∀ (e : Fin n → M₂), (Eval s₂ e (⇑φ ∘ ε₁)) p) → ∀ (e : Fin n → M₁), (Eval s₁ e ε₁) p
Theorem: LO.FirstOrder.Semiformula.eval_hom_univClosure
Proof state before:
n✝ : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁ : Fin n✝ → M₁
ε₁✝ : μ → M₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
⊢ (∀ (e : Fin n → M₂), (Eval s₂ e (⇑φ ∘ ε₁)) p) → ∀ (e : Fin n → M₁), (Eval s₁ e ε₁) p
Tactic:
intro h e₁
Proof state after:
n✝ : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n✝ → M₁
ε₁✝ : μ → M₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
h : ∀ (e : Fin n → M₂), (Eval s₂ e (⇑φ ∘ ε₁)) p
e₁ : Fin n → M₁
⊢ (Eval s₁ e₁ ε₁) p
Theorem: LO.FirstOrder.Semiformula.eval_hom_univClosure
Proof state before:
n✝ : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n✝ → M₁
ε₁✝ : μ → M₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
h : ∀ (e : Fin n → M₂), (Eval s₂ e (⇑φ ∘ ε₁)) p
e₁ : Fin n → M₁
⊢ (Eval s₁ e₁ ε₁) p
Tactic:
exact (eval_hom_iff_of_open φ hp).mpr (h (φ ∘ e₁))
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.ElementaryEquiv.refl
Proof state before:
L : Language
M✝ : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M✝
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M✝
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
M : Type u_5
inst✝¹ : Nonempty M
inst✝ : Structure L M
σ : Sentence L
⊢ M ⊧ₘ σ ↔ M ⊧ₘ σ
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.ElementaryEquiv.modelsTheory
Proof state before:
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝³ : Nonempty M
inst✝² : Nonempty M₁
inst✝¹ : Nonempty M₂
inst✝ : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
h : M₁ ≡ₑ[L] M₂
T : Theory L
⊢ M₁ ⊧ₘ* T ↔ M₂ ⊧ₘ* T
Tactic:
simp [modelsTheory_iff, h.models]
Proof state after:
no goals
Theorem: LO.FirstOrder.Structure.ElementaryEquiv.ofEquiv
Proof state before:
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁴ : Nonempty M
inst✝³ : Nonempty M₁
inst✝² : Nonempty M₂
inst✝¹ : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
N : Type u_5
inst✝ : Nonempty N
φ : M ≃ N
σ : Sentence L
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ
Tactic:
letI : Structure L N := Structure.ofEquiv φ
Proof state after:
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁴ : Nonempty M
inst✝³ : Nonempty M₁
inst✝² : Nonempty M₂
inst✝¹ : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
N : Type u_5
inst✝ : Nonempty N
φ : M ≃ N
σ : Sentence L
this : Structure L N := Structure.ofEquiv φ
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ
Theorem: LO.FirstOrder.Structure.ElementaryEquiv.ofEquiv
Proof state before:
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁴ : Nonempty M
inst✝³ : Nonempty M₁
inst✝² : Nonempty M₂
inst✝¹ : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
N : Type u_5
inst✝ : Nonempty N
φ : M ≃ N
σ : Sentence L
this : Structure L N := Structure.ofEquiv φ
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ
Tactic:
simp [models_iff, Empty.eq_elim, Structure.eval_ofEquiv_iff]
Proof state after:
no goals
Theorem: LO.FirstOrder.models_hom_iff_of_open
Proof state before:
n : ℕ
μ : Sort ?u.85351
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : Structure.EmbeddingClass F L M₁ M₂
φ : F
e₁ : Fin n → M₁
ε₁ : μ → M₁
σ : Sentence L
hσ : Semiformula.Open σ
⊢ M₁ ⊧ₘ σ ↔ M₂ ⊧ₘ σ
Tactic:
simpa[Matrix.empty_eq, Empty.eq_elim] using
  Semiformula.eval_hom_iff_of_open (e₁ := finZeroElim) (ε₁ := Empty.elim) φ hσ
Proof state after:
no goals
Theorem: LO.FirstOrder.models_hom_univClosure
Proof state before:
n✝ : ℕ
μ : Sort ?u.89010
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : Structure.EmbeddingClass F L M₁ M₂
φ : F
e₁ : Fin n✝ → M₁
ε₁ : μ → M₁
n : ℕ
σ : Semisentence L n
hσ : Semiformula.Open σ
⊢ M₂ ⊧ₘ ∀* σ → M₁ ⊧ₘ ∀* σ
Tactic:
simpa[Matrix.empty_eq, Empty.eq_elim, models_iff] using
  Semiformula.eval_hom_univClosure (ε₁ := Empty.elim) φ hσ
Proof state after:
no goals
Theorem: LO.FirstOrder.ElementaryEquiv.ofEquiv
Proof state before:
n : ℕ
μ : Sort ?u.123142
N : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Nonempty M
inst✝⁵ : Nonempty M₁
inst✝⁴ : Nonempty M₂
inst✝³ : Nonempty M₃
s✝ : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝² : FunLike F M₁ M₂
inst✝¹ : Structure.EmbeddingClass F L M₁ M₂
φ✝ : F
e₁ : Fin n → M₁
ε₁ : μ → M₁
s : Structure L M
φ : M ≃ N
inst✝ : Nonempty N
σ : Sentence L
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ
Tactic:
letI : Structure L N := Structure.ofEquiv φ
Proof state after:
n : ℕ
μ : Sort ?u.123142
N : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Nonempty M
inst✝⁵ : Nonempty M₁
inst✝⁴ : Nonempty M₂
inst✝³ : Nonempty M₃
s✝ : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝² : FunLike F M₁ M₂
inst✝¹ : Structure.EmbeddingClass F L M₁ M₂
φ✝ : F
e₁ : Fin n → M₁
ε₁ : μ → M₁
s : Structure L M
φ : M ≃ N
inst✝ : Nonempty N
σ : Sentence L
this : Structure L N := Structure.ofEquiv φ
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ
Theorem: LO.FirstOrder.ElementaryEquiv.ofEquiv
Proof state before:
n : ℕ
μ : Sort ?u.123142
N : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Nonempty M
inst✝⁵ : Nonempty M₁
inst✝⁴ : Nonempty M₂
inst✝³ : Nonempty M₃
s✝ : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝² : FunLike F M₁ M₂
inst✝¹ : Structure.EmbeddingClass F L M₁ M₂
φ✝ : F
e₁ : Fin n → M₁
ε₁ : μ → M₁
s : Structure L M
φ : M ≃ N
inst✝ : Nonempty N
σ : Sentence L
this : Structure L N := Structure.ofEquiv φ
⊢ M ⊧ₘ σ ↔ N ⊧ₘ σ
Tactic:
simp [models_iff, Empty.eq_elim, Structure.eval_ofEquiv_iff]
Proof state after:
no goals
Theorem: LO.Modal.Standard.GoedelTranslation.atom_def
Proof state before:
α : Type ?u.2441
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
p q : Superintuitionistic.Formula α
α✝ : Type u_1
a : α✝
⊢ Superintuitionistic.Formula.atom aᵍ = □Formula.atom a
Tactic:
simp [GoedelTranslation]
Proof state after:
no goals
Theorem: LO.Modal.Standard.GoedelTranslation.falsum_def
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
p q : Superintuitionistic.Formula α
⊢ ⊥ᵍ = ⊥
Tactic:
simp [GoedelTranslation]
Proof state after:
no goals
Theorem: LO.Modal.Standard.GoedelTranslation.verum_def
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
p q : Superintuitionistic.Formula α
⊢ ⊤ᵍ = ⊤
Tactic:
simp [GoedelTranslation]
Proof state after:
no goals
Theorem: LO.Modal.Standard.GoedelTranslation.and_def
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
p q : Superintuitionistic.Formula α
⊢ (p ⋏ q)ᵍ = pᵍ ⋏ qᵍ
Tactic:
simp [GoedelTranslation]
Proof state after:
no goals
Theorem: LO.Modal.Standard.GoedelTranslation.or_def
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
p q : Superintuitionistic.Formula α
⊢ (p ⋎ q)ᵍ = pᵍ ⋎ qᵍ
Tactic:
simp [GoedelTranslation]
Proof state after:
no goals
Theorem: LO.Modal.Standard.GoedelTranslation.imp_def
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
p q : Superintuitionistic.Formula α
⊢ (p ⟶ q)ᵍ = □(pᵍ ⟶ qᵍ)
Tactic:
simp [GoedelTranslation]
Proof state after:
no goals
Theorem: LO.Modal.Standard.GoedelTranslation.neg_def'
Proof state before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
inst✝ : Encodable α
p q : Superintuitionistic.Formula α
⊢ (~p)ᵍ = □~pᵍ
Tactic:
simp [GoedelTranslation, NegAbbrev.neg]
Proof state after:
no goals
Theorem: LO.Modal.Standard.axiomTc_GTranslate!
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! pᵍ ⟶ □pᵍ
Tactic:
induction p using Superintuitionistic.Formula.rec' with
| hatom => simp only [GoedelTranslation.atom_def, axiomFour!];
| himp => simp only [GoedelTranslation.imp_def, axiomFour!];
| hfalsum => simp only [GoedelTranslation.falsum_def, efq!];
| hverum => exact dhyp! (nec! verum!);
| hand p q ihp ihq =>
  simp only [GoedelTranslation.and_def];
  exact imp_trans! (andReplace! ihp ihq) collect_box_and!
| hor p q ihp ihq =>
  simp only [GoedelTranslation.or_def];
  exact imp_trans! (disj₃''! (implyOrLeft'! ihp) (implyOrRight'! ihq)) collect_box_or!
Proof state after:
no goals
Theorem: LO.Modal.Standard.axiomTc_GTranslate!
Proof state before:
case hatom
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
a✝ : α
⊢ m𝓓 ⊢! Superintuitionistic.Formula.atom a✝ᵍ ⟶ □Superintuitionistic.Formula.atom a✝ᵍ
Tactic:
simp only [GoedelTranslation.atom_def, axiomFour!]
Proof state after:
no goals
Theorem: LO.Modal.Standard.axiomTc_GTranslate!
Proof state before:
case himp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p✝ q✝ : Superintuitionistic.Formula α
a✝¹ : m𝓓 ⊢! p✝ᵍ ⟶ □p✝ᵍ
a✝ : m𝓓 ⊢! q✝ᵍ ⟶ □q✝ᵍ
⊢ m𝓓 ⊢! (p✝ ⟶ q✝)ᵍ ⟶ □(p✝ ⟶ q✝)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def, axiomFour!]
Proof state after:
no goals
Theorem: LO.Modal.Standard.axiomTc_GTranslate!
Proof state before:
case hfalsum
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! ⊥ᵍ ⟶ □⊥ᵍ
Tactic:
simp only [GoedelTranslation.falsum_def, efq!]
Proof state after:
no goals
Theorem: LO.Modal.Standard.axiomTc_GTranslate!
Proof state before:
case hverum
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! ⊤ᵍ ⟶ □⊤ᵍ
Tactic:
exact dhyp! (nec! verum!)
Proof state after:
no goals
Theorem: LO.Modal.Standard.axiomTc_GTranslate!
Proof state before:
case hand
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! (p ⋏ q)ᵍ ⟶ □(p ⋏ q)ᵍ
Tactic:
simp only [GoedelTranslation.and_def]
Proof state after:
case hand
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! pᵍ ⋏ qᵍ ⟶ □(pᵍ ⋏ qᵍ)
Theorem: LO.Modal.Standard.axiomTc_GTranslate!
Proof state before:
case hand
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! pᵍ ⋏ qᵍ ⟶ □(pᵍ ⋏ qᵍ)
Tactic:
exact imp_trans! (andReplace! ihp ihq) collect_box_and!
Proof state after:
no goals
Theorem: LO.Modal.Standard.axiomTc_GTranslate!
Proof state before:
case hor
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! (p ⋎ q)ᵍ ⟶ □(p ⋎ q)ᵍ
Tactic:
simp only [GoedelTranslation.or_def]
Proof state after:
case hor
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! pᵍ ⋎ qᵍ ⟶ □(pᵍ ⋎ qᵍ)
Theorem: LO.Modal.Standard.axiomTc_GTranslate!
Proof state before:
case hor
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p✝ q✝ r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
p q : Superintuitionistic.Formula α
ihp : m𝓓 ⊢! pᵍ ⟶ □pᵍ
ihq : m𝓓 ⊢! qᵍ ⟶ □qᵍ
⊢ m𝓓 ⊢! pᵍ ⋎ qᵍ ⟶ □(pᵍ ⋎ qᵍ)
Tactic:
exact imp_trans! (disj₃''! (implyOrLeft'! ihp) (implyOrRight'! ihq)) collect_box_or!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! (p ⟶ q ⟶ p)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def]
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! □(pᵍ ⟶ □(qᵍ ⟶ pᵍ))
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₁
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : K4 m𝓓
⊢ m𝓓 ⊢! □(pᵍ ⟶ □(qᵍ ⟶ pᵍ))
Tactic:
exact nec! $ imp_trans! axiomTc_GTranslate! $ axiomK'! $ nec! $ imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.provable_efq_of_provable_S4.case_imply₂
Proof state before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ m𝓓 ⊢! ((p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r)ᵍ
Tactic:
simp only [GoedelTranslation.imp_def]
Proof state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
inst✝¹ : Encodable α
i𝓓 : Superintuitionistic.DeductionParameter α
m𝓓 : DeductionParameter α
p q r : Superintuitionistic.Formula α
inst✝ : S4 m𝓓
⊢ m𝓓 ⊢! □(□(pᵍ ⟶ □(qᵍ ⟶ rᵍ)) ⟶ □(□(pᵍ ⟶ qᵍ) ⟶ □(pᵍ ⟶ rᵍ)))