internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝¹ : Formula α
f : realization L α
p✝ p : Formula α
e : Axioms.Four p = p✝
⊢ T ⊢! f[β] p✝
Tactic:
subst_vars
Proof state after:
case hMaxm.inr.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝ : Formula α
f : realization L α
p : Formula α
⊢ T ⊢! f[β] Axioms.Four p
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hMaxm.inr.intro
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p✝ : Formula α
f : realization L α
p : Formula α
⊢ T ⊢! f[β] Axioms.Four p
Tactic:
apply HilbertBernays₃.D3s (T₀ := T₀)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hLoeb
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
hasLoeb✝ : 𝐊𝟒(𝐋).rules.loeb = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐋) ⊢! □p✝ ⟶ p✝
ih : T ⊢! f[β] □p✝ ⟶ p✝
⊢ T ⊢! f[β] p✝
Tactic:
exact Loeb.LT T₀ ih
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hHenkin
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
hasHenkin✝ : 𝐊𝟒(𝐋).rules.henkin = true
p✝ : Formula α
hp✝ : 𝐊𝟒(𝐋) ⊢! □p✝ ⟷ p✝
a✝ : T ⊢! f[β] □p✝ ⟷ p✝
⊢ T ⊢! f[β] p✝
Tactic:
simp_all only [Bool.false_eq_true]
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hMdp
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
hpq✝ : 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝
hp✝ : 𝐊𝟒(𝐋) ⊢! p✝
ihpq : T ⊢! f[β] p✝ ⟶ q✝
ihp : T ⊢! f[β] p✝
⊢ T ⊢! f[β] q✝
Tactic:
simp [interpretation] at ihpq
Proof state after:
case hMdp
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
hpq✝ : 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝
hp✝ : 𝐊𝟒(𝐋) ⊢! p✝
ihpq : T ⊢! (f[β] p✝) ⟶ f[β] q✝
ihp : T ⊢! f[β] p✝
⊢ T ⊢! f[β] q✝
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hMdp
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
hpq✝ : 𝐊𝟒(𝐋) ⊢! p✝ ⟶ q✝
hp✝ : 𝐊𝟒(𝐋) ⊢! p✝
ihpq : T ⊢! (f[β] p✝) ⟶ f[β] q✝
ihp : T ⊢! f[β] p✝
⊢ T ⊢! f[β] q✝
Tactic:
exact ihpq ⨀ ihp
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hDne
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
⊢ T ⊢! f[β] ~~p✝ ⟶ p✝
Tactic:
dsimp [interpretation]
Proof state after:
case hDne
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
⊢ T ⊢! (((f[β] p✝) ⟶ ⊥) ⟶ ⊥) ⟶ f[β] p✝
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hDne
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ : Formula α
⊢ T ⊢! (((f[β] p✝) ⟶ ⊥) ⟶ ⊥) ⟶ f[β] p✝
Tactic:
exact imp_trans! (conj₁'! $ iffComm'! NegationEquiv.negneg_equiv!) dne!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hDisj₃
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ r✝ : Formula α
⊢ T ⊢! f[β] (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
first
| apply verum!;
| apply imply₁!;
| apply imply₂!;
| apply conj₁!;
| apply conj₂!;
| apply conj₃!;
| apply disj₁!;
| apply disj₂!;
| apply disj₃!;
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hVerum
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
⊢ T ⊢! f[β] ⊤
Tactic:
apply verum!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hImply₁
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⟶ q✝ ⟶ p✝
Tactic:
apply imply₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hImply₂
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ r✝ : Formula α
⊢ T ⊢! f[β] (p✝ ⟶ q✝ ⟶ r✝) ⟶ (p✝ ⟶ q✝) ⟶ p✝ ⟶ r✝
Tactic:
apply imply₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hConj₁
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⋏ q✝ ⟶ p✝
Tactic:
apply conj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hConj₂
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⋏ q✝ ⟶ q✝
Tactic:
apply conj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hConj₃
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⟶ q✝ ⟶ p✝ ⋏ q✝
Tactic:
apply conj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hDisj₁
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] p✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₁!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hDisj₂
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ : Formula α
⊢ T ⊢! f[β] q✝ ⟶ p✝ ⋎ q✝
Tactic:
apply disj₂!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_K4Loeb
Proof state before:
case hDisj₃
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
f : realization L α
p✝ q✝ r✝ : Formula α
⊢ T ⊢! f[β] (p✝ ⟶ r✝) ⟶ (q✝ ⟶ r✝) ⟶ p✝ ⋎ q✝ ⟶ r✝
Tactic:
apply disj₃!
Proof state after:
no goals
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_GL
Proof state before:
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ ∀ {f : realization L α}, T ⊢! f[β] p
Tactic:
apply arithmetical_soundness_K4Loeb (T₀ := T₀)
Proof state after:
case h
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p
Theorem: LO.Modal.Standard.Provability.arithmetical_soundness_GL
Proof state before:
case h
α : Type u_1
inst✝⁵ : DecidableEq α
L : Language
inst✝⁴ : Semiterm.Operator.GoedelNumber L (Sentence L)
inst✝³ : DecidableEq (Sentence L)
T₀ T : FirstOrder.Theory L
inst✝² : T₀ ≼ T
inst✝¹ : Diagonalization T₀
β : ProvabilityPredicate L L
inst✝ : β.HilbertBernays T₀ T
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p
Tactic:
exact (System.reducible_iff.mp reducible_GL_K4Loeb) h
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Theory.coe_indH_subset_indH
Proof state before:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
⊢ ⇑(Semiformula.lMap Language.oringEmb) '' indScheme ℒₒᵣ (Hierarchy Γ ν) ⊆ indScheme L (Hierarchy Γ ν)
Tactic:
simp [Theory.indH, Theory.indScheme]
Proof state after:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
⊢ ∀ (a : Sentence ℒₒᵣ) (x : Semiformula ℒₒᵣ ℕ 1),
    Hierarchy Γ ν x → a = ∀ᶠ* succInd x → ∃ p, Hierarchy Γ ν p ∧ (Semiformula.lMap Language.oringEmb) a = ∀ᶠ* succInd p
Theorem: LO.FirstOrder.Arith.Theory.coe_indH_subset_indH
Proof state before:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
⊢ ∀ (a : Sentence ℒₒᵣ) (x : Semiformula ℒₒᵣ ℕ 1),
    Hierarchy Γ ν x → a = ∀ᶠ* succInd x → ∃ p, Hierarchy Γ ν p ∧ (Semiformula.lMap Language.oringEmb) a = ∀ᶠ* succInd p
Tactic:
rintro _ p Hp rfl
Proof state after:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
p : Semiformula ℒₒᵣ ℕ 1
Hp : Hierarchy Γ ν p
⊢ ∃ p_1, Hierarchy Γ ν p_1 ∧ (Semiformula.lMap Language.oringEmb) (∀ᶠ* succInd p) = ∀ᶠ* succInd p_1
Theorem: LO.FirstOrder.Arith.Theory.coe_indH_subset_indH
Proof state before:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
p : Semiformula ℒₒᵣ ℕ 1
Hp : Hierarchy Γ ν p
⊢ ∃ p_1, Hierarchy Γ ν p_1 ∧ (Semiformula.lMap Language.oringEmb) (∀ᶠ* succInd p) = ∀ᶠ* succInd p_1
Tactic:
exact ⟨Semiformula.lMap (Language.oringEmb : ℒₒᵣ →ᵥ L) p, Hierarchy.oringEmb Hp,
  by simp [Formula.lMap_fvUnivClosure, succInd, Semiformula.lMap_substs]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Arith.Theory.coe_indH_subset_indH
Proof state before:
L : Language
inst✝¹ : L.ORing
ξ : Type u_1
inst✝ : DecidableEq ξ
Γ : Polarity
ν : ℕ
p : Semiformula ℒₒᵣ ℕ 1
Hp : Hierarchy Γ ν p
⊢ (Semiformula.lMap Language.oringEmb) (∀ᶠ* succInd p) = ∀ᶠ* succInd ((Semiformula.lMap Language.oringEmb) p)
Tactic:
simp [Formula.lMap_fvUnivClosure, succInd, Semiformula.lMap_substs]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiterm.val_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
e : Fin n → Uprod A 𝓤
ε : μ → Uprod A 𝓤
t : Semiterm L μ n
⊢ valm (Uprod A 𝓤) e ε t = { val := fun i => val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) t }
Tactic:
induction t <;> simp[*, val_func]
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
e : Fin n✝ → Uprod A 𝓤
⊢ Set.univ ∈ 𝓤
Tactic:
case hverum => exact Filter.univ_mem
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → Uprod A 𝓤
⊢ {i | Structure.rel r fun x => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v x)} ∉ 𝓤 ↔
    {i | ¬Structure.rel r fun i_1 => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v i_1)} ∈ 𝓤
Tactic:
case hnrel k r v =>
  exact Ultrafilter.compl_mem_iff_not_mem.symm
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
a✝ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤 ∧
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝ ∧
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈
      𝓤
Tactic:
case hand =>
  exact Filter.inter_mem_iff.symm
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p q : Semiformula L μ n✝
ihp :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
ihq :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤 ∨
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p ∨
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈
      𝓤
Tactic:
case hor p q ihp ihq =>
  exact Ultrafilter.union_mem_iff.symm
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
e : Fin n✝ → Uprod A 𝓤
⊢ Set.univ ∈ 𝓤
Tactic:
exact Filter.univ_mem
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n✝
e : Fin n✝ → Uprod A 𝓤
⊢ {i | Structure.rel r fun x => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v x)} ∉ 𝓤 ↔
    {i | ¬Structure.rel r fun i_1 => Semiterm.val (s i) (fun x => (e x).val i) (fun x => (ε x).val i) (v i_1)} ∈ 𝓤
Tactic:
exact Ultrafilter.compl_mem_iff_not_mem.symm
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p✝ q✝ : Semiformula L μ n✝
a✝¹ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤
a✝ :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q✝ ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝} ∈ 𝓤 ∧
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p✝ ∧
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q✝} ∈
      𝓤
Tactic:
exact Filter.inter_mem_iff.symm
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p q : Semiformula L μ n✝
ihp :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
ihq :
  ∀ {e : Fin n✝ → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) q ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤 ∨
      {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈ 𝓤 ↔
    {i |
        (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p ∨
          (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) q} ∈
      𝓤
Tactic:
exact Ultrafilter.union_mem_iff.symm
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤) ↔
    {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
constructor
Proof state after:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤) →
    {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤

case mpr
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤 →
    ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
Theorem: LO.FirstOrder.Semiformula.eval_Uprod
Proof state before:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
⊢ (∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤) →
    {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
Tactic:
intro h
Proof state after:
case mp
n : ℕ
L : Language
μ : Type v
I : Type u
A : I → Type u
inst✝ : ∀ (i : I), Nonempty (A i)
s : (i : I) → Structure L (A i)
𝓤 : Ultrafilter I
ε : μ → Uprod A 𝓤
n✝ : ℕ
p : Semiformula L μ (n✝ + 1)
a✝ :
  ∀ {e : Fin (n✝ + 1) → Uprod A 𝓤},
    (Evalm (Uprod A 𝓤) e ε) p ↔ {i | (Eval (s i) (fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤
e : Fin n✝ → Uprod A 𝓤
h : ∀ (x : Uprod A 𝓤), {i | (Eval (s i) (fun x_1 => ((x :> e) x_1).val i) fun x => (ε x).val i) p} ∈ 𝓤
⊢ {i | ∀ (x : A i), (Eval (s i) (x :> fun x => (e x).val i) fun x => (ε x).val i) p} ∈ 𝓤