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

State before:
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p ∈ rel r v :: nrel r v :: Δ, (Evalfm M ε) p
Tactic:
by_cases h : s.rel r (Semiterm.valm M ![] ε ∘ v)
State after:
case pos
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ ∃ p ∈ rel r v :: nrel r v :: Δ, (Evalfm M ε) p

case neg
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : ¬Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ ∃ p ∈ rel r v :: nrel r v :: Δ, (Evalfm M ε) p

State before:
case pos
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ ∃ p ∈ rel r v :: nrel r v :: Δ, (Evalfm M ε) p
Tactic:
exact ⟨rel r v, by simp, h⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ rel r v ∈ rel r v :: nrel r v :: Δ
Tactic:
simp
State after:
no goals

State before:
case neg
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : ¬Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ ∃ p ∈ rel r v :: nrel r v :: Δ, (Evalfm M ε) p
Tactic:
exact ⟨nrel r v, by simp, h⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
k✝ : ℕ
r : L.Rel k✝
v : Fin k✝ → Semiterm L ℕ 0
M : Type u_1
s : Structure L M
ε : ℕ → M
h : ¬Structure.rel r (Semiterm.valm M ![] ε ∘ v)
⊢ nrel r v ∈ rel r v :: nrel r v :: Δ
Tactic:
simp
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ⊤ ∈ ⊤ :: Δ ∧ (Evalfm M ε) ⊤
Tactic:
simp
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1
Tactic:
have : Evalfm M ε p ∨ Evalfm M ε q ∨ ∃ q ∈ Δ, Evalfm M ε q := by simpa using sound d M ε
State after:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (Evalfm M ε) p ∨ (Evalfm M ε) q ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (Evalfm M ε) p ∨ (Evalfm M ε) q ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1
Tactic:
rcases this with (hp | hq | ⟨r, hr, hhr⟩)
State after:
case inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1

case inr.inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hq : (Evalfm M ε) q
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1

case inr.inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ (Evalfm M ε) p ∨ (Evalfm M ε) q ∨ ∃ q ∈ Δ, (Evalfm M ε) q
Tactic:
simpa using sound d M ε
State after:
no goals

State before:
case inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨p ⋎ q, by simp, by simp [hp]⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
⊢ p ⋎ q ∈ p ⋎ q :: Δ
Tactic:
simp
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
⊢ (Evalfm M ε) (p ⋎ q)
Tactic:
simp [hp]
State after:
no goals

State before:
case inr.inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hq : (Evalfm M ε) q
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨p ⋎ q, by simp, by simp [hq]⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hq : (Evalfm M ε) q
⊢ p ⋎ q ∈ p ⋎ q :: Δ
Tactic:
simp
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hq : (Evalfm M ε) q
⊢ (Evalfm M ε) (p ⋎ q)
Tactic:
simp [hq]
State after:
no goals

State before:
case inr.inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋎ q :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨r, by simp [hr], hhr⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
d : Derivation (p :: q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ r ∈ p ⋎ q :: Δ
Tactic:
simp [hr]
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1
Tactic:
have : Evalfm M ε p ∨ ∃ r ∈ Δ, Evalfm M ε r := by simpa using sound dp M ε
State after:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (Evalfm M ε) p ∨ ∃ r ∈ Δ, (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (Evalfm M ε) p ∨ ∃ r ∈ Δ, (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1
Tactic:
rcases this with (hp | ⟨r, hr, hhr⟩)
State after:
case inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1

case inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ (Evalfm M ε) p ∨ ∃ r ∈ Δ, (Evalfm M ε) r
Tactic:
simpa using sound dp M ε
State after:
no goals

State before:
case inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1
Tactic:
have : Evalfm M ε q ∨ ∃ r ∈ Δ, Evalfm M ε r := by simpa using sound dq M ε
State after:
case inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
this : (Evalfm M ε) q ∨ ∃ r ∈ Δ, (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1

State before:
case inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
this : (Evalfm M ε) q ∨ ∃ r ∈ Δ, (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1
Tactic:
rcases this with (hq | ⟨r, hr, hhr⟩)
State after:
case inl.inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
hq : (Evalfm M ε) q
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1

case inl.inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
⊢ (Evalfm M ε) q ∨ ∃ r ∈ Δ, (Evalfm M ε) r
Tactic:
simpa using sound dq M ε
State after:
no goals

State before:
case inl.inl
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
hq : (Evalfm M ε) q
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨p ⋏ q, by simp, by simp [hp, hq]⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
hq : (Evalfm M ε) q
⊢ p ⋏ q ∈ p ⋏ q :: Δ
Tactic:
simp
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
hq : (Evalfm M ε) q
⊢ (Evalfm M ε) (p ⋏ q)
Tactic:
simp [hp, hq]
State after:
no goals

State before:
case inl.inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨r, by simp [hr], hhr⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalfm M ε) p
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ r ∈ p ⋏ q :: Δ
Tactic:
simp [hr]
State after:
no goals

State before:
case inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ ∃ p_1 ∈ p ⋏ q :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨r, by simp [hr], hhr⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p q : SyntacticFormula L
dp : Derivation (p :: Δ)
dq : Derivation (q :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
r : SyntacticFormula L
hr : r ∈ Δ
hhr : (Evalfm M ε) r
⊢ r ∈ p ⋏ q :: Δ
Tactic:
simp [hr]
State after:
no goals

State before:
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p_1 ∈ (∀' p) :: Δ, (Evalfm M ε) p_1
Tactic:
have : (∀ a : M, Evalm M ![a] ε p) ∨ ∃ q ∈ Δ, Evalfm M ε q := by
  simpa[shifts, shiftEmb, Matrix.vecConsLast_vecEmpty, forall_or_right]
    using fun a : M => sound d M (a :>ₙ ε)
State after:
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (∀ (a : M), (Evalm M ![a] ε) p) ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p_1 ∈ (∀' p) :: Δ, (Evalfm M ε) p_1

State before:
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (∀ (a : M), (Evalm M ![a] ε) p) ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p_1 ∈ (∀' p) :: Δ, (Evalfm M ε) p_1
Tactic:
rcases this with (hp | ⟨q, hq, hhq⟩)
State after:
case inl
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : ∀ (a : M), (Evalm M ![a] ε) p
⊢ ∃ p_1 ∈ (∀' p) :: Δ, (Evalfm M ε) p_1

case inr.intro.intro
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
q : SyntacticSemiformula L 0
hq : q ∈ Δ
hhq : (Evalfm M ε) q
⊢ ∃ p_1 ∈ (∀' p) :: Δ, (Evalfm M ε) p_1

State before:
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ (∀ (a : M), (Evalm M ![a] ε) p) ∨ ∃ q ∈ Δ, (Evalfm M ε) q
Tactic:
simpa[shifts, shiftEmb, Matrix.vecConsLast_vecEmpty, forall_or_right]
  using fun a : M => sound d M (a :>ₙ ε)
State after:
no goals

State before:
case inl
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : ∀ (a : M), (Evalm M ![a] ε) p
⊢ ∃ p_1 ∈ (∀' p) :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨∀' p, by simp, hp⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : ∀ (a : M), (Evalm M ![a] ε) p
⊢ ∀' p ∈ (∀' p) :: Δ
Tactic:
simp
State after:
no goals

State before:
case inr.intro.intro
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
q : SyntacticSemiformula L 0
hq : q ∈ Δ
hhq : (Evalfm M ε) q
⊢ ∃ p_1 ∈ (∀' p) :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨q, by simp [hq], hhq⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
q : SyntacticSemiformula L 0
hq : q ∈ Δ
hhq : (Evalfm M ε) q
⊢ q ∈ (∀' p) :: Δ
Tactic:
simp [hq]
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p_1 ∈ (∃' p) :: Δ, (Evalfm M ε) p_1
Tactic:
have : Evalm M ![t.valm M ![] ε] ε p ∨ ∃ p ∈ Δ, Evalfm M ε p := by
  simpa[eval_substs, Matrix.constant_eq_singleton] using sound d M ε
State after:
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (Evalm M ![Semiterm.valm M ![] ε t] ε) p ∨ ∃ p ∈ Δ, (Evalfm M ε) p
⊢ ∃ p_1 ∈ (∃' p) :: Δ, (Evalfm M ε) p_1

State before:
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
this : (Evalm M ![Semiterm.valm M ![] ε t] ε) p ∨ ∃ p ∈ Δ, (Evalfm M ε) p
⊢ ∃ p_1 ∈ (∃' p) :: Δ, (Evalfm M ε) p_1
Tactic:
rcases this with (hp | ⟨q, hq, hhq⟩)
State after:
case inl
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalm M ![Semiterm.valm M ![] ε t] ε) p
⊢ ∃ p_1 ∈ (∃' p) :: Δ, (Evalfm M ε) p_1

case inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
q : SyntacticFormula L
hq : q ∈ Δ
hhq : (Evalfm M ε) q
⊢ ∃ p_1 ∈ (∃' p) :: Δ, (Evalfm M ε) p_1

State before:
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ (Evalm M ![Semiterm.valm M ![] ε t] ε) p ∨ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
simpa[eval_substs, Matrix.constant_eq_singleton] using sound d M ε
State after:
no goals

State before:
case inl
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalm M ![Semiterm.valm M ![] ε t] ε) p
⊢ ∃ p_1 ∈ (∃' p) :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨∃' p, by simp, t.valm M ![] ε, hp⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hp : (Evalm M ![Semiterm.valm M ![] ε t] ε) p
⊢ ∃' p ∈ (∃' p) :: Δ
Tactic:
simp
State after:
no goals

State before:
case inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
q : SyntacticFormula L
hq : q ∈ Δ
hhq : (Evalfm M ε) q
⊢ ∃ p_1 ∈ (∃' p) :: Δ, (Evalfm M ε) p_1
Tactic:
exact ⟨q, by simp [hq], hhq⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
q : SyntacticFormula L
hq : q ∈ Δ
hhq : (Evalfm M ε) q
⊢ q ∈ (∃' p) :: Δ
Tactic:
simp [hq]
State after:
no goals

State before:
L : Language
Γ Δ : Sequent L
d : Derivation Δ
ss : Δ ⊆ Γ
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p ∈ Γ, (Evalfm M ε) p
Tactic:
have : ∃ p ∈ Δ, Evalfm M ε p := sound d M ε
State after:
L : Language
Γ Δ : Sequent L
d : Derivation Δ
ss : Δ ⊆ Γ
M : Type u_1
s : Structure L M
ε : ℕ → M
this : ∃ p ∈ Δ, (Evalfm M ε) p
⊢ ∃ p ∈ Γ, (Evalfm M ε) p

State before:
L : Language
Γ Δ : Sequent L
d : Derivation Δ
ss : Δ ⊆ Γ
M : Type u_1
s : Structure L M
ε : ℕ → M
this : ∃ p ∈ Δ, (Evalfm M ε) p
⊢ ∃ p ∈ Γ, (Evalfm M ε) p
Tactic:
rcases this with ⟨p, hp, h⟩
State after:
case intro.intro
L : Language
Γ Δ : Sequent L
d : Derivation Δ
ss : Δ ⊆ Γ
M : Type u_1
s : Structure L M
ε : ℕ → M
p : SyntacticFormula L
hp : p ∈ Δ
h : (Evalfm M ε) p
⊢ ∃ p ∈ Γ, (Evalfm M ε) p

State before:
case intro.intro
L : Language
Γ Δ : Sequent L
d : Derivation Δ
ss : Δ ⊆ Γ
M : Type u_1
s : Structure L M
ε : ℕ → M
p : SyntacticFormula L
hp : p ∈ Δ
h : (Evalfm M ε) p
⊢ ∃ p ∈ Γ, (Evalfm M ε) p
Tactic:
exact ⟨p, ss hp, h⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
have h : Evalfm M ε p ∨ ∃ q ∈ Δ, Evalfm M ε q := by simpa using sound d M ε
State after:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p

State before:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
have hn : ¬Evalfm M ε p ∨ ∃ q ∈ Δ, Evalfm M ε q := by simpa using sound dn M ε
State after:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
hn : ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p

State before:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
hn : ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
rcases h with (h | ⟨q, h, hq⟩)
State after:
case inl
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hn : ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
h : (Evalfm M ε) p
⊢ ∃ p ∈ Δ, (Evalfm M ε) p

case inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hn : ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
q : SyntacticFormula L
h : q ∈ Δ
hq : (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p

State before:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ (Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
Tactic:
simpa using sound d M ε
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
Tactic:
simpa using sound dn M ε
State after:
no goals

State before:
case inl
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hn : ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
h : (Evalfm M ε) p
⊢ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
rcases hn with (hn | ⟨q, hn, hq⟩)
State after:
case inl.inl
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p
hn : ¬(Evalfm M ε) p
⊢ ∃ p ∈ Δ, (Evalfm M ε) p

case inl.inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p
q : SyntacticFormula L
hn : q ∈ Δ
hq : (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p

State before:
case inl.inl
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p
hn : ¬(Evalfm M ε) p
⊢ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
contradiction
State after:
no goals

State before:
case inl.inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p
q : SyntacticFormula L
hn : q ∈ Δ
hq : (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
exact ⟨q, by simp [hn], hq⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p
q : SyntacticFormula L
hn : q ∈ Δ
hq : (Evalfm M ε) q
⊢ q ∈ Δ
Tactic:
simp [hn]
State after:
no goals

State before:
case inr.intro.intro
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hn : ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
q : SyntacticFormula L
h : q ∈ Δ
hq : (Evalfm M ε) q
⊢ ∃ p ∈ Δ, (Evalfm M ε) p
Tactic:
exact ⟨q, by simp [h], hq⟩
State after:
no goals

State before:
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
hn : ¬(Evalfm M ε) p ∨ ∃ q ∈ Δ, (Evalfm M ε) q
q : SyntacticFormula L
h : q ∈ Δ
hq : (Evalfm M ε) q
⊢ q ∈ Δ
Tactic:
simp [h]
State after:
no goals