Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_or (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋎ q ∈ t.tableau.1 ↔ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋎ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∨ q ∈ t.tableau.1

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1

State before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋎ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∨ q ∈ t.tableau.1

case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1
Tactic:
. intro h;
  by_contra hC; simp [not_or] at hC;
  have : p ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.1;
  have : q ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.2;
  have : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj' := by simp;
  have : 𝓓 ⊬! [p ⋎ q].conj' ⟶ [p, q].disj' := t.consistent (by simp_all) (by simp_all);
  contradiction;
State after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1

State before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1
Tactic:
. intro h;
  cases h with
  | inl h => exact mdp₁ h disj₁!
  | inr h => exact mdp₁ h disj₂!
State after:
no goals

State before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ⋎ q ∈ t.tableau.1 → p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1

State before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
Tactic:
by_contra hC
State after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : ¬(p ∈ t.tableau.1 ∨ q ∈ t.tableau.1)
⊢ False

State before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : ¬(p ∈ t.tableau.1 ∨ q ∈ t.tableau.1)
⊢ False
Tactic:
simp [not_or] at hC
State after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
⊢ False

State before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
⊢ False
Tactic:
have : p ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.1
State after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this : p ∈ t.tableau.2
⊢ False

State before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this : p ∈ t.tableau.2
⊢ False
Tactic:
have : q ∈ t.tableau.2 := t.not_mem₁_iff_mem₂.mp hC.2
State after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝ : p ∈ t.tableau.2
this : q ∈ t.tableau.2
⊢ False

State before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝ : p ∈ t.tableau.2
this : q ∈ t.tableau.2
⊢ False
Tactic:
have : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj' := by simp;
State after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝¹ : p ∈ t.tableau.2
this✝ : q ∈ t.tableau.2
this : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ False

State before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝¹ : p ∈ t.tableau.2
this✝ : q ∈ t.tableau.2
this : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ False
Tactic:
have : 𝓓 ⊬! [p ⋎ q].conj' ⟶ [p, q].disj' := t.consistent (by simp_all) (by simp_all)
State after:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝² : p ∈ t.tableau.2
this✝¹ : q ∈ t.tableau.2
this✝ : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
this : 𝓓 ⊬! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ False

State before:
case mp
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝² : p ∈ t.tableau.2
this✝¹ : q ∈ t.tableau.2
this✝ : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
this : 𝓓 ⊬! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝ : p ∈ t.tableau.2
this : q ∈ t.tableau.2
⊢ 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝¹ : p ∈ t.tableau.2
this✝ : q ∈ t.tableau.2
this : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ ∀ p_1 ∈ [p ⋎ q], p_1 ∈ t.tableau.1
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ⋎ q ∈ t.tableau.1
hC : p ∉ t.tableau.1 ∧ q ∉ t.tableau.1
this✝¹ : p ∈ t.tableau.2
this✝ : q ∈ t.tableau.2
this : 𝓓 ⊢! [p ⋎ q].conj' ⟶ [p, q].disj'
⊢ ∀ p_1 ∈ [p, q], p_1 ∈ t.tableau.2
Tactic:
simp_all
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
⊢ p ∈ t.tableau.1 ∨ q ∈ t.tableau.1 → p ⋎ q ∈ t.tableau.1
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
⊢ p ⋎ q ∈ t.tableau.1

State before:
case mpr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ∈ t.tableau.1 ∨ q ∈ t.tableau.1
⊢ p ⋎ q ∈ t.tableau.1
Tactic:
cases h with
| inl h => exact mdp₁ h disj₁!
| inr h => exact mdp₁ h disj₂!
State after:
no goals

State before:
case mpr.inl
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : p ∈ t.tableau.1
⊢ p ⋎ q ∈ t.tableau.1
Tactic:
exact mdp₁ h disj₁!
State after:
no goals

State before:
case mpr.inr
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
h : q ∈ t.tableau.1
⊢ p ⋎ q ∈ t.tableau.1
Tactic:
exact mdp₁ h disj₂!
State after:
no goals