Theorem: LO.FirstOrder.Completeness.chainSet_id (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 Γ)
σ : Sentence L
h : σ ∈ T
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
have : ⛓️[(encode $ Code.id σ).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode $ Code.id σ).pair 0] := chain_spec' nwf _ _
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 Γ)
σ : Sentence L
h : σ ∈ T
this : ⛓️[(encode (Code.id σ)).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️

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 Γ)
σ : Sentence L
h : σ ∈ T
this : ⛓️[(encode (Code.id σ)).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
generalize hΔ : ⛓️[(encode $ Code.id σ).pair 0 + 1] = Δ
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 Γ)
σ : Sentence L
h : σ ∈ T
this : ⛓️[(encode (Code.id σ)).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = Δ
⊢ ~Rew.emb.hom σ ∈ ⛓️

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 Γ)
σ : Sentence L
h : σ ∈ T
this : ⛓️[(encode (Code.id σ)).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = Δ
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
rw[hΔ] at this
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 Γ)
σ : Sentence L
h : σ ∈ T
Δ : Sequent L
this : Δ ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = Δ
⊢ ~Rew.emb.hom σ ∈ ⛓️

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 Γ)
σ : Sentence L
h : σ ∈ T
Δ : Sequent L
this : Δ ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = Δ
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
rcases this
State after:
case id
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 Γ)
σ : Sentence L
h hσ✝ : σ ∈ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ~Rew.emb.hom σ :: ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️

case idRefl
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 Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️

State before:
case id
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 Γ)
σ : Sentence L
h hσ✝ : σ ∈ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ~Rew.emb.hom σ :: ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️

case idRefl
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 Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
{ exact Set.mem_iUnion.mpr ⟨(encode $ Code.id σ).pair 0 + 1, by simp[hΔ]⟩ }
State after:
case idRefl
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 Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️

State before:
case idRefl
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 Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
{ contradiction }
State after:
no goals

State before:
case id
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 Γ)
σ : Sentence L
h hσ✝ : σ ∈ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ~Rew.emb.hom σ :: ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
exact Set.mem_iUnion.mpr ⟨(encode $ Code.id σ).pair 0 + 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 Γ)
σ : Sentence L
h hσ✝ : σ ∈ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ~Rew.emb.hom σ :: ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ {x | x ∈ ⛓️[(encode (Code.id σ)).pair 0 + 1]}
Tactic:
simp[hΔ]
State after:
no goals

State before:
case idRefl
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 Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
contradiction
State after:
no goals