Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.iff_mem₁_and (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; constructor <;> exact mdp₁ h (by simp)
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:
. rintro ⟨hp, hq⟩;
  by_contra hC;
  have : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj' := by simp;
  have : 𝓓 ⊬! [p, q].conj' ⟶ [p ⋏ q].disj' := t.consistent (by aesop) (by simpa using t.not_mem₁_iff_mem₂.mp hC);
  contradiction;
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:
constructor <;> exact mdp₁ h (by 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
⊢ 𝓓 ⊢! p ⋏ q ⟶ q
Tactic:
simp
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:
rintro ⟨hp, hq⟩
State after:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
⊢ p ⋏ q ∈ t.tableau.1

State before:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
⊢ p ⋏ q ∈ t.tableau.1
Tactic:
by_contra hC
State after:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
⊢ False

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

State before:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ False
Tactic:
have : 𝓓 ⊬! [p, q].conj' ⟶ [p ⋏ q].disj' := t.consistent (by aesop) (by simpa using t.not_mem₁_iff_mem₂.mp hC)
State after:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this✝ : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
this : 𝓓 ⊬! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ False

State before:
case mpr.intro
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p q : Formula α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
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 α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
⊢ 𝓓 ⊢! [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 α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ ∀ p_1 ∈ [p, q], p_1 ∈ t.tableau.1
Tactic:
aesop
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 α
hp : p ∈ t.tableau.1
hq : q ∈ t.tableau.1
hC : p ⋏ q ∉ t.tableau.1
this : 𝓓 ⊢! [p, q].conj' ⟶ [p ⋏ q].disj'
⊢ ∀ p_1 ∈ [p ⋏ q], p_1 ∈ t.tableau.2
Tactic:
simpa using t.not_mem₁_iff_mem₂.mp hC
State after:
no goals