Theorem: LO.FirstOrder.Completeness.chainSet_ex (Logic/FirstOrder/Completeness/SearchTree.lean)

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
⊢ [→ t].hom p ∈ ⛓️
Tactic:
have : ∃ s, ∃' p ∈ ⛓️[s] := by simpa[chainSet] using h
State after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
this : ∃ s, ∃' p ∈ ⛓️[s]
⊢ [→ t].hom p ∈ ⛓️

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
this : ∃ s, ∃' p ∈ ⛓️[s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
rcases this with ⟨s, hs⟩
State after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
⊢ [→ t].hom p ∈ ⛓️

State before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
have : ⛓️[(encode $ Code.ex p t).pair s + 1] ≺[Code.ex p t] ⛓️[(encode $ Code.ex p t).pair s] := chain_spec' nwf _ _
State after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
this : ⛓️[(encode (Code.ex p t)).pair s + 1] ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️

State before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
this : ⛓️[(encode (Code.ex p t)).pair s + 1] ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
generalize hΔ : ⛓️[(encode $ Code.ex p t).pair s + 1] = Δ at this
State after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = Δ
this : Δ ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️

State before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = Δ
this : Δ ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
rcases this
State after:
case intro.ex
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
a✝ : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = [→ t].hom p :: ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️

case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️

State before:
case intro.ex
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
a✝ : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = [→ t].hom p :: ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️

case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
{ exact Set.mem_iUnion.mpr ⟨(encode $ Code.ex p t).pair s + 1, by simp[hΔ]⟩ }
State after:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️

State before:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
{ have : ∃' p ∈ ⛓️[(encode $ Code.ex p t).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
  contradiction }
State after:
no goals

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
⊢ ∃ s, ∃' p ∈ ⛓️[s]
Tactic:
simpa[chainSet] using h
State after:
no goals

State before:
case intro.ex
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
a✝ : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = [→ t].hom p :: ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
exact Set.mem_iUnion.mpr ⟨(encode $ Code.ex p t).pair s + 1, by simp[hΔ]⟩
State after:
no goals

State before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
a✝ : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = [→ t].hom p :: ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ {x | x ∈ ⛓️[(encode (Code.ex p t)).pair s + 1]}
Tactic:
simp[hΔ]
State after:
no goals

State before:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
have : ∃' p ∈ ⛓️[(encode $ Code.ex p t).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
State after:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
this : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️

State before:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
this : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
contradiction
State after:
no goals