internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof state before:
L : Language
Δ : List (SyntacticFormula L)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ ⊤ ∈ ⊤ :: Δ ∧ (Evalfm M ε) ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩)
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩)
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩)
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 :>ₙ ε)
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩)
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 :>ₙ ε)
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩)
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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]
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩)
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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 ε
Proof state after:
no goals
Theorem: LO.FirstOrder.Derivation.sound
Proof 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⟩)
Proof 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
Theorem: LO.FirstOrder.Derivation.sound
Proof 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
Proof state after:
no goals