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

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
⊢ Disjoint t.1 t.2
Tactic:
by_contra h
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
⊢ False

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
⊢ False
Tactic:
obtain ⟨T, hp₁, hp₂, hp⟩ := by simpa [Disjoint] using h;
State after:
case intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp : ¬T ⊆ ∅
⊢ False

State before:
case intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp : ¬T ⊆ ∅
⊢ False
Tactic:
obtain ⟨p, hp, _⟩ := Set.not_subset.mp hp
State after:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
⊢ False

State before:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
⊢ False
Tactic:
simp [ParametricConsistent] at hCon
State after:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
⊢ False

State before:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
⊢ False
Tactic:
have : 𝓓 ⊬! [p].conj' ⟶ [p].disj' := hCon
  (by simp_all; apply hp₁; assumption)
  (by simp_all; apply hp₂; assumption)
State after:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
this : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
⊢ False

State before:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
this : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
⊢ False
Tactic:
have : 𝓓 ⊢! [p].conj' ⟶ [p].disj' := by simp;
State after:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
this✝ : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
this : 𝓓 ⊢! [p].conj' ⟶ [p].disj'
⊢ False

State before:
case intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
this✝ : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
this : 𝓓 ⊢! [p].conj' ⟶ [p].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
h : ¬Disjoint t.1 t.2
⊢ ?m.113495
Tactic:
simpa [Disjoint] using h
State after:
no goals

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
⊢ ∀ p_1 ∈ [p], p_1 ∈ t.1
Tactic:
simp_all
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
⊢ p ∈ t.1

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
⊢ p ∈ t.1
Tactic:
apply hp₁
State after:
case a
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
⊢ p ∈ T

State before:
case a
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
⊢ p ∈ T
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
⊢ ∀ p_1 ∈ [p], p_1 ∈ t.2
Tactic:
simp_all
State after:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
⊢ p ∈ t.2

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
⊢ p ∈ t.2
Tactic:
apply hp₂
State after:
case a
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
⊢ p ∈ T

State before:
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : ∀ {Γ Δ : List (Formula α)}, (∀ p ∈ Γ, p ∈ t.1) → (∀ p ∈ Δ, p ∈ t.2) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
h : ¬Disjoint t.1 t.2
T : Theory α
hp₁ : T ⊆ t.1
hp₂ : T ⊆ t.2
hp✝ : ¬T ⊆ ∅
p : Formula α
hp : p ∈ T
right✝ : p ∉ ∅
this : 𝓓 ⊬! [p].conj' ⟶ [p].disj'
⊢ 𝓓 ⊢! [p].conj' ⟶ [p].disj'
Tactic:
simp
State after:
no goals