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

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p : Formula α
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p ↔ p ∈ t.tableau.1
Tactic:
induction p using rec' generalizing t with
| himp p q ihp ihq =>
  constructor;
  . contrapose;
    simp_all;
    intro h;
    replace h := t.not_mem₁_iff_mem₂.mp h;
    have : (𝓓)-Consistent (insert p t.tableau.1, {q}) := by
      simp only [Tableau.ParametricConsistent];
      intro Γ Δ hΓ hΔ;
      replace hΓ : ∀ r, r ∈ Γ.remove p → r ∈ t.tableau.1 := by
        intro r hr;
        have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr;
        have := by simpa using hΓ r hr₁;
        simp_all;
      by_contra hC;
      have : 𝓓 ⊢! (Γ.remove p).conj' ⟶ (p ⟶ q) := imp_trans! (andImplyIffImplyImply'!.mp $ implyLeftRemoveConj' hC) (by
        apply deduct'!;
        apply deduct!;
        have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp);
        have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this;
        exact disj_allsame'! (by simpa using hΔ) this;
      )
      have : 𝓓 ⊬! (Γ.remove p).conj' ⟶ (p ⟶ q) := by simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all));
      contradiction;
    obtain ⟨t', ⟨⟨_, _⟩, _⟩⟩ := by simpa [Set.insert_subset_iff] using lindenbaum this;
    existsi t';
    simp_all;
    apply t'.not_mem₁_iff_mem₂.mpr;
    assumption;
  . simp [Satisfies.imp_def];
    intro h t' htt' hp;
    replace hp := ihp.mp hp;
    have hpq := htt' h;
    apply ihq.mpr;
    apply t'.not_mem₂_iff_mem₁.mp;
    exact not_mem₂
      (by simp_all)
      (show 𝓓 ⊢! [p, p ⟶ q].conj' ⟶ q by
        simp;
        apply andImplyIffImplyImply'!.mpr;
        apply deduct'!;
        apply deduct!;
        exact by_axm! ⨀ (by_axm! (p := p));
      );
| _ => simp [Satisfies.iff_models, Satisfies, *];
State after:
no goals

State before:
case himp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p ⟶ q ↔ p ⟶ q ∈ t.tableau.1
Tactic:
constructor
State after:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p ⟶ q → p ⟶ q ∈ t.tableau.1

case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 → t ⊧ p ⟶ q

State before:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p ⟶ q → p ⟶ q ∈ t.tableau.1

case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 → t ⊧ p ⟶ q
Tactic:
. contrapose;
  simp_all;
  intro h;
  replace h := t.not_mem₁_iff_mem₂.mp h;
  have : (𝓓)-Consistent (insert p t.tableau.1, {q}) := by
    simp only [Tableau.ParametricConsistent];
    intro Γ Δ hΓ hΔ;
    replace hΓ : ∀ r, r ∈ Γ.remove p → r ∈ t.tableau.1 := by
      intro r hr;
      have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr;
      have := by simpa using hΓ r hr₁;
      simp_all;
    by_contra hC;
    have : 𝓓 ⊢! (Γ.remove p).conj' ⟶ (p ⟶ q) := imp_trans! (andImplyIffImplyImply'!.mp $ implyLeftRemoveConj' hC) (by
      apply deduct'!;
      apply deduct!;
      have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp);
      have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this;
      exact disj_allsame'! (by simpa using hΔ) this;
    )
    have : 𝓓 ⊬! (Γ.remove p).conj' ⟶ (p ⟶ q) := by simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all));
    contradiction;
  obtain ⟨t', ⟨⟨_, _⟩, _⟩⟩ := by simpa [Set.insert_subset_iff] using lindenbaum this;
  existsi t';
  simp_all;
  apply t'.not_mem₁_iff_mem₂.mpr;
  assumption;
State after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 → t ⊧ p ⟶ q

State before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 → t ⊧ p ⟶ q
Tactic:
. simp [Satisfies.imp_def];
  intro h t' htt' hp;
  replace hp := ihp.mp hp;
  have hpq := htt' h;
  apply ihq.mpr;
  apply t'.not_mem₂_iff_mem₁.mp;
  exact not_mem₂
    (by simp_all)
    (show 𝓓 ⊢! [p, p ⟶ q].conj' ⟶ q by
      simp;
      apply andImplyIffImplyImply'!.mpr;
      apply deduct'!;
      apply deduct!;
      exact by_axm! ⨀ (by_axm! (p := p));
    );
State after:
no goals

State before:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p ⟶ q → p ⟶ q ∈ t.tableau.1
Tactic:
contrapose
State after:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∉ t.tableau.1 → ¬t ⊧ p ⟶ q

State before:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∉ t.tableau.1 → ¬t ⊧ p ⟶ q
Tactic:
simp_all
State after:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
⊢ p ⟶ q ∉ t.tableau.1 → ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1

State before:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
⊢ p ⟶ q ∉ t.tableau.1 → ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
intro h
State after:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∉ t.tableau.1
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1

State before:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∉ t.tableau.1
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
replace h := t.not_mem₁_iff_mem₂.mp h
State after:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1

State before:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
have : (𝓓)-Consistent (insert p t.tableau.1, {q}) := by
  simp only [Tableau.ParametricConsistent];
  intro Γ Δ hΓ hΔ;
  replace hΓ : ∀ r, r ∈ Γ.remove p → r ∈ t.tableau.1 := by
    intro r hr;
    have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr;
    have := by simpa using hΓ r hr₁;
    simp_all;
  by_contra hC;
  have : 𝓓 ⊢! (Γ.remove p).conj' ⟶ (p ⟶ q) := imp_trans! (andImplyIffImplyImply'!.mp $ implyLeftRemoveConj' hC) (by
    apply deduct'!;
    apply deduct!;
    have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp);
    have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this;
    exact disj_allsame'! (by simpa using hΔ) this;
  )
  have : 𝓓 ⊬! (Γ.remove p).conj' ⟶ (p ⟶ q) := by simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all));
  contradiction;
State after:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1

State before:
case himp.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
obtain ⟨t', ⟨⟨_, _⟩, _⟩⟩ := by simpa [Set.insert_subset_iff] using lindenbaum this;
State after:
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1

State before:
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ ∃ x, t.tableau.1 ⊆ x.tableau.1 ∧ p ∈ x.tableau.1 ∧ q ∉ x.tableau.1
Tactic:
existsi t'
State after:
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ t.tableau.1 ⊆ t'.tableau.1 ∧ p ∈ t'.tableau.1 ∧ q ∉ t'.tableau.1

State before:
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ t.tableau.1 ⊆ t'.tableau.1 ∧ p ∈ t'.tableau.1 ∧ q ∉ t'.tableau.1
Tactic:
simp_all
State after:
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ q ∉ t'.tableau.1

State before:
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ q ∉ t'.tableau.1
Tactic:
apply t'.not_mem₁_iff_mem₂.mpr
State after:
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ q ∈ t'.tableau.2

State before:
case himp.mp.intro.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
t' : SaturatedConsistentTableau 𝓓
right✝¹ : q ∈ t'.tableau.2
left✝ : p ∈ t'.tableau.1
right✝ : t.tableau.1 ⊆ t'.tableau.1
⊢ q ∈ t'.tableau.2
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
⊢ (𝓓)-Consistent (insert p t.tableau.1, {q})
Tactic:
simp only [Tableau.ParametricConsistent]
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
⊢ ∀ {Γ Δ : List (Formula α)}, (∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1) → (∀ p ∈ Δ, p ∈ {q}) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
⊢ ∀ {Γ Δ : List (Formula α)}, (∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1) → (∀ p ∈ Δ, p ∈ {q}) → 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
intro Γ Δ hΓ hΔ
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
replace hΓ : ∀ r, r ∈ Γ.remove p → r ∈ t.tableau.1 := by
  intro r hr;
  have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr;
  have := by simpa using hΓ r hr₁;
  simp_all;
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
⊢ 𝓓 ⊬! Γ.conj' ⟶ Δ.disj'
Tactic:
by_contra hC
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ False
Tactic:
have : 𝓓 ⊢! (Γ.remove p).conj' ⟶ (p ⟶ q) := imp_trans! (andImplyIffImplyImply'!.mp $ implyLeftRemoveConj' hC) (by
  apply deduct'!;
  apply deduct!;
  have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp);
  have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this;
  exact disj_allsame'! (by simpa using hΔ) this;
)
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ False

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ False
Tactic:
have : 𝓓 ⊬! (Γ.remove p).conj' ⟶ (p ⟶ q) := by simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all));
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
this : 𝓓 ⊬! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ False

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
this : 𝓓 ⊬! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
⊢ ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
Tactic:
intro r hr
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
⊢ r ∈ t.tableau.1

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
⊢ r ∈ t.tableau.1
Tactic:
have ⟨hr₁, hr₂⟩ := List.mem_remove_iff.mp hr
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
⊢ r ∈ t.tableau.1

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
⊢ r ∈ t.tableau.1
Tactic:
have := by simpa using hΓ r hr₁;
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
this : r = p ∨ r ∈ t.tableau.1
⊢ r ∈ t.tableau.1

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
this : r = p ∨ r ∈ t.tableau.1
⊢ r ∈ t.tableau.1
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 ∈ insert p t.tableau.1
hΔ : ∀ p ∈ Δ, p ∈ {q}
r : Formula α
hr : r ∈ List.remove p Γ
hr₁ : r ∈ Γ
hr₂ : r ≠ p
⊢ ?m.615290
Tactic:
simpa using hΓ r hr₁
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ 𝓓 ⊢! (p ⟶ Δ.disj') ⟶ p ⟶ q
Tactic:
apply deduct'!
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ [p ⟶ Δ.disj'] ⊢[𝓓]! p ⟶ q

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ [p ⟶ Δ.disj'] ⊢[𝓓]! p ⟶ q
Tactic:
apply deduct!
State after:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q

State before:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
Tactic:
have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p := by_axm! (by simp)
State after:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q

State before:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
Tactic:
have : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj' := (by_axm! (by simp)) ⨀ this
State after:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj'
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q

State before:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj'
⊢ [p, p ⟶ Δ.disj'] ⊢[𝓓]! q
Tactic:
exact disj_allsame'! (by simpa using hΔ) this
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
⊢ p ∈ [p, p ⟶ Δ.disj']
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
⊢ p ⟶ Δ.disj' ∈ [p, p ⟶ Δ.disj']
Tactic:
simp
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this✝ : [p, p ⟶ Δ.disj'] ⊢[𝓓]! p
this : [p, p ⟶ Δ.disj'] ⊢[𝓓]! Δ.disj'
⊢ ∀ q_1 ∈ Δ, q_1 = q
Tactic:
simpa using hΔ
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ 𝓓 ⊬! (List.remove p Γ).conj' ⟶ p ⟶ q
Tactic:
simpa only [List.disj'_singleton] using (t.consistent hΓ (show ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2 by simp_all))
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ {q}
hΓ : ∀ r ∈ List.remove p Γ, r ∈ t.tableau.1
hC : 𝓓 ⊢! Γ.conj' ⟶ Δ.disj'
this : 𝓓 ⊢! (List.remove p Γ).conj' ⟶ p ⟶ q
⊢ ∀ r ∈ [p ⟶ q], r ∈ t.tableau.2
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
t : (CanonicalModel 𝓓).World
ihp : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, Satisfies (CanonicalModel 𝓓) t q ↔ q ∈ t.tableau.1
h : p ⟶ q ∈ t.tableau.2
this : (𝓓)-Consistent (insert p t.tableau.1, {q})
⊢ ?m.706390
Tactic:
simpa [Set.insert_subset_iff] using lindenbaum this
State after:
no goals

State before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 → t ⊧ p ⟶ q
Tactic:
simp [Satisfies.imp_def]
State after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 →
    ∀ {w' : (CanonicalModel 𝓓).Frame.World},
      t.tableau.1 ⊆ w'.tableau.1 → Satisfies (CanonicalModel 𝓓) w' p → Satisfies (CanonicalModel 𝓓) w' q

State before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ p ⟶ q ∈ t.tableau.1 →
    ∀ {w' : (CanonicalModel 𝓓).Frame.World},
      t.tableau.1 ⊆ w'.tableau.1 → Satisfies (CanonicalModel 𝓓) w' p → Satisfies (CanonicalModel 𝓓) w' q
Tactic:
intro h t' htt' hp
State after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : Satisfies (CanonicalModel 𝓓) t' p
⊢ Satisfies (CanonicalModel 𝓓) t' q

State before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : Satisfies (CanonicalModel 𝓓) t' p
⊢ Satisfies (CanonicalModel 𝓓) t' q
Tactic:
replace hp := ihp.mp hp
State after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
⊢ Satisfies (CanonicalModel 𝓓) t' q

State before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
⊢ Satisfies (CanonicalModel 𝓓) t' q
Tactic:
have hpq := htt' h
State after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ Satisfies (CanonicalModel 𝓓) t' q

State before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ Satisfies (CanonicalModel 𝓓) t' q
Tactic:
apply ihq.mpr
State after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ q ∈ t'.tableau.1

State before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ q ∈ t'.tableau.1
Tactic:
apply t'.not_mem₂_iff_mem₁.mp
State after:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ q ∉ t'.tableau.2

State before:
case himp.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ q ∉ t'.tableau.2
Tactic:
exact not_mem₂
  (by simp_all)
  (show 𝓓 ⊢! [p, p ⟶ q].conj' ⟶ q by
    simp;
    apply andImplyIffImplyImply'!.mpr;
    apply deduct'!;
    apply deduct!;
    exact by_axm! ⨀ (by_axm! (p := p));
  )
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ ∀ p_1 ∈ [p, 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 α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ 𝓓 ⊢! [p, p ⟶ q].conj' ⟶ q
Tactic:
simp
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ 𝓓 ⊢! p ⋏ (p ⟶ q) ⟶ q

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ 𝓓 ⊢! p ⋏ (p ⟶ q) ⟶ q
Tactic:
apply andImplyIffImplyImply'!.mpr
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ 𝓓 ⊢! p ⟶ (p ⟶ q) ⟶ q

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ 𝓓 ⊢! p ⟶ (p ⟶ q) ⟶ q
Tactic:
apply deduct'!
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ [p] ⊢[𝓓]! (p ⟶ q) ⟶ q

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ [p] ⊢[𝓓]! (p ⟶ q) ⟶ q
Tactic:
apply deduct!
State after:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ [p ⟶ q, p] ⊢[𝓓]! q

State before:
case h.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p q : Formula α
ihp : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p ↔ p ∈ t.tableau.1
ihq : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q ↔ q ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
h : p ⟶ q ∈ t.tableau.1
t' : (CanonicalModel 𝓓).Frame.World
htt' : t.tableau.1 ⊆ t'.tableau.1
hp : p ∈ t'.tableau.1
hpq : p ⟶ q ∈ t'.tableau.1
⊢ [p ⟶ q, p] ⊢[𝓓]! q
Tactic:
exact by_axm! ⨀ (by_axm! (p := p))
State after:
no goals

State before:
case hor
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
𝓓 : DeductionParameter α
inst✝² : 𝓓.IncludeEFQ
inst✝¹ : Encodable α
inst✝ : Inhabited (SCT 𝓓)
t✝ : SCT 𝓓
p✝ q✝ : Formula α
a✝¹ : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ p✝ ↔ p✝ ∈ t.tableau.1
a✝ : ∀ {t : (CanonicalModel 𝓓).World}, t ⊧ q✝ ↔ q✝ ∈ t.tableau.1
t : (CanonicalModel 𝓓).World
⊢ t ⊧ p✝ ⋎ q✝ ↔ p✝ ⋎ q✝ ∈ t.tableau.1
Tactic:
simp [Satisfies.iff_models, Satisfies, *]
State after:
no goals