Theorem: LO.Propositional.Superintuitionistic.Tableau.consistent_either (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
⊢ (𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2)
Tactic:
by_contra hC
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬((𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2))
⊢ False

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬((𝓓)-Consistent (insert p t.1, t.2) ∨ (𝓓)-Consistent (t.1, insert p t.2))
⊢ False
Tactic:
push_neg at hC
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
⊢ False

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
⊢ False
Tactic:
have ⟨hC₁, hC₂⟩ := hC
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
⊢ False

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
⊢ False
Tactic:
obtain ⟨Γ₁, Δ₁, hΓ₁, hΔ₁, h₁⟩ := iff_not_ParametricConsistent_insert₁.mp hC₁
State after:
case intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! p ⋏ Γ₁.conj' ⟶ Δ₁.disj'
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! p ⋏ Γ₁.conj' ⟶ Δ₁.disj'
⊢ False
Tactic:
replace h₁ := imply_left_and_comm'! h₁
State after:
case intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
⊢ False
Tactic:
obtain ⟨Γ₂, Δ₂, hΓ₂, hΔ₂, h₂⟩ := iff_not_ParametricConsistent_insert₂.mp hC₂
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
⊢ False
Tactic:
have : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj' := imp_trans! (conj₁'! iff_concat_conj!) $ imp_trans! (cut! h₁ h₂) (conj₂'! iff_concact_disj!)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False
Tactic:
have : 𝓓 ⊬! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj' := hCon (by simp; rintro q (hq₁ | hq₂); exact hΓ₁ q hq₁; exact hΓ₂ q hq₂) (by simp; rintro q (hq₁ | hq₂); exact hΔ₁ q hq₁; exact hΔ₂ q hq₂)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this✝ : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
this : 𝓓 ⊬! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this✝ : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
this : 𝓓 ⊬! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ p ∈ Γ₁ ++ Γ₂, p ∈ t.1
Tactic:
simp
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ (p : Formula α), p ∈ Γ₁ ∨ p ∈ Γ₂ → p ∈ t.1

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ (p : Formula α), p ∈ Γ₁ ∨ p ∈ Γ₂ → p ∈ t.1
Tactic:
rintro q (hq₁ | hq₂)
State after:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₁ : q ∈ Γ₁
⊢ q ∈ t.1

case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Γ₂
⊢ q ∈ t.1

State before:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₁ : q ∈ Γ₁
⊢ q ∈ t.1

case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Γ₂
⊢ q ∈ t.1
Tactic:
exact hΓ₁ q hq₁
State after:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Γ₂
⊢ q ∈ t.1

State before:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Γ₂
⊢ q ∈ t.1
Tactic:
exact hΓ₂ q hq₂
State after:
no goals

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ p ∈ Δ₁ ++ Δ₂, p ∈ t.2
Tactic:
simp
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ (p : Formula α), p ∈ Δ₁ ∨ p ∈ Δ₂ → p ∈ t.2

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ ∀ (p : Formula α), p ∈ Δ₁ ∨ p ∈ Δ₂ → p ∈ t.2
Tactic:
rintro q (hq₁ | hq₂)
State after:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₁ : q ∈ Δ₁
⊢ q ∈ t.2

case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Δ₂
⊢ q ∈ t.2

State before:
case inl
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₁ : q ∈ Δ₁
⊢ q ∈ t.2

case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Δ₂
⊢ q ∈ t.2
Tactic:
exact hΔ₁ q hq₁
State after:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Δ₂
⊢ q ∈ t.2

State before:
case inr
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
q : Formula α
hq₂ : q ∈ Δ₂
⊢ q ∈ t.2
Tactic:
exact hΔ₂ q hq₂
State after:
no goals