Theorem: LO.FirstOrder.sound (Logic/FirstOrder/Basic/Soundness.lean)

State before:
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
⊢ s ⊧ σ
Tactic:
rcases s.nonempty with ⟨x⟩
State after:
case intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
⊢ s ⊧ σ

State before:
case intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
⊢ s ⊧ σ
Tactic:
rcases Derivation.sound b.derivation s.Dom (fun _ ↦ x) with ⟨p, hp, h⟩
State after:
case intro.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
p : SyntacticFormula L
hp : p ∈ List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) b.antecedent ++ [σ])
h : (Evalfm s.Dom fun x_1 => x) p
⊢ s ⊧ σ

State before:
case intro.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
p : SyntacticFormula L
hp : p ∈ List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) b.antecedent ++ [σ])
h : (Evalfm s.Dom fun x_1 => x) p
⊢ s ⊧ σ
Tactic:
simp at hp
State after:
case intro.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
p : SyntacticFormula L
h : (Evalfm s.Dom fun x_1 => x) p
hp : (∃ a ∈ b.antecedent, ~Rew.emb.hom a = p) ∨ p = Rew.emb.hom σ
⊢ s ⊧ σ

State before:
case intro.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
p : SyntacticFormula L
h : (Evalfm s.Dom fun x_1 => x) p
hp : (∃ a ∈ b.antecedent, ~Rew.emb.hom a = p) ∨ p = Rew.emb.hom σ
⊢ s ⊧ σ
Tactic:
rcases hp with (⟨π, hπ, rfl⟩ | rfl)
State after:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
⊢ s ⊧ σ

case intro.intro.intro.inr
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
h : (Evalfm s.Dom fun x_1 => x) (Rew.emb.hom σ)
⊢ s ⊧ σ

State before:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
⊢ s ⊧ σ
Tactic:
have : s ⊧ π := hT.RealizeSet (Gentzen.Disjconseq.subset b π hπ)
State after:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this : s ⊧ π
⊢ s ⊧ σ

State before:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this : s ⊧ π
⊢ s ⊧ σ
Tactic:
have : ¬s ⊧ π := by simpa using h
State after:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this✝ : s ⊧ π
this : ¬s ⊧ π
⊢ s ⊧ σ

State before:
case intro.intro.intro.inl.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this✝ : s ⊧ π
this : ¬s ⊧ π
⊢ s ⊧ σ
Tactic:
contradiction
State after:
no goals

State before:
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this : s ⊧ π
⊢ ¬s ⊧ π
Tactic:
simpa using h
State after:
no goals

State before:
case intro.intro.intro.inr
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
h : (Evalfm s.Dom fun x_1 => x) (Rew.emb.hom σ)
⊢ s ⊧ σ
Tactic:
simpa using h
State after:
no goals