Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_Dot3 (Logic/Modal/Standard/Kripke/Dot3.lean)

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
⊢ Connected (CanonicalFrame 𝓓).Rel
Tactic:
dsimp only [Connected]
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
⊢ ∀ ⦃x y z : MCT 𝓓⦄,
    □''⁻¹x.theory ⊆ y.theory ∧ □''⁻¹x.theory ⊆ z.theory → □''⁻¹y.theory ⊆ z.theory ∨ □''⁻¹z.theory ⊆ y.theory

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
⊢ ∀ ⦃x y z : MCT 𝓓⦄,
    □''⁻¹x.theory ⊆ y.theory ∧ □''⁻¹x.theory ⊆ z.theory → □''⁻¹y.theory ⊆ z.theory ∨ □''⁻¹z.theory ⊆ y.theory
Tactic:
intro X Y Z ⟨hXY, hXZ⟩
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
⊢ □''⁻¹Y.theory ⊆ Z.theory ∨ □''⁻¹Z.theory ⊆ Y.theory

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
⊢ □''⁻¹Y.theory ⊆ Z.theory ∨ □''⁻¹Z.theory ⊆ Y.theory
Tactic:
by_contra hC
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬(□''⁻¹Y.theory ⊆ Z.theory ∨ □''⁻¹Z.theory ⊆ Y.theory)
⊢ False

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬(□''⁻¹Y.theory ⊆ Z.theory ∨ □''⁻¹Z.theory ⊆ Y.theory)
⊢ False
Tactic:
push_neg at hC
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬□''⁻¹Y.theory ⊆ Z.theory ∧ ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬□''⁻¹Y.theory ⊆ Z.theory ∧ ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False
Tactic:
have ⟨nhYZ, nhZY⟩ := hC
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬□''⁻¹Y.theory ⊆ Z.theory ∧ ¬□''⁻¹Z.theory ⊆ Y.theory
nhYZ : ¬□''⁻¹Y.theory ⊆ Z.theory
nhZY : ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
hC : ¬□''⁻¹Y.theory ⊆ Z.theory ∧ ¬□''⁻¹Z.theory ⊆ Y.theory
nhYZ : ¬□''⁻¹Y.theory ⊆ Z.theory
nhZY : ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False
Tactic:
clear hC
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhYZ : ¬□''⁻¹Y.theory ⊆ Z.theory
nhZY : ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhYZ : ¬□''⁻¹Y.theory ⊆ Z.theory
nhZY : ¬□''⁻¹Z.theory ⊆ Y.theory
⊢ False
Tactic:
simp only [Set.not_subset] at nhYZ nhZY
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhYZ : ∃ a ∈ □''⁻¹Y.theory, a ∉ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
⊢ False

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhYZ : ∃ a ∈ □''⁻¹Y.theory, a ∉ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
⊢ False
Tactic:
obtain ⟨p, hpY, hpZ⟩ := nhYZ
State after:
case intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
p : Formula α
hpY : p ∈ □''⁻¹Y.theory
hpZ : p ∉ Z.theory
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
p : Formula α
hpY : p ∈ □''⁻¹Y.theory
hpZ : p ∉ Z.theory
⊢ False
Tactic:
replace hpY : □p ∈ Y.theory := hpY
State after:
case intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
nhZY : ∃ a ∈ □''⁻¹Z.theory, a ∉ Y.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
⊢ False
Tactic:
obtain ⟨q, hqZ, hqY⟩ := nhZY
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqZ : q ∈ □''⁻¹Z.theory
hqY : q ∉ Y.theory
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqZ : q ∈ □''⁻¹Z.theory
hqY : q ∉ Y.theory
⊢ False
Tactic:
replace hqZ : □q ∈ Z.theory := hqZ
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ False
Tactic:
have hpqX : □(□p ⟶ q) ∉ X.theory := by
  apply iff_mem_box.not.mpr; push_neg;
  use Y;
  constructor;
  . assumption;
  . apply iff_mem_imp.not.mpr; simp [hpY, hqY];
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ False
Tactic:
have hqpX : □(□q ⟶ p) ∉ X.theory := by
  apply iff_mem_box.not.mpr; push_neg;
  use Z;
  constructor;
  . assumption;
  . apply iff_mem_imp.not.mpr; simp [hpZ, hqZ];
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ False
Tactic:
have : (□(□p ⟶ q) ⋎ □(□q ⟶ p)) ∉ X.theory := by
  apply iff_mem_or.not.mpr; push_neg; exact ⟨hpqX, hqpX⟩;
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ False
Tactic:
have : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ X.theory := by
  apply subset_axiomset _
  exact hAx (by aesop);
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this✝ : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ X.theory
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this✝ : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ X.theory
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □(□p ⟶ q) ∉ X.theory
Tactic:
apply iff_mem_box.not.mpr
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ¬∀ {Ω' : MCT 𝓓}, □''⁻¹X.theory ⊆ Ω'.theory → □p ⟶ q ∈ Ω'.theory

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ¬∀ {Ω' : MCT 𝓓}, □''⁻¹X.theory ⊆ Ω'.theory → □p ⟶ q ∈ Ω'.theory
Tactic:
push_neg
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ∃ Ω', □''⁻¹X.theory ⊆ Ω'.theory ∧ □p ⟶ q ∉ Ω'.theory

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ∃ Ω', □''⁻¹X.theory ⊆ Ω'.theory ∧ □p ⟶ q ∉ Ω'.theory
Tactic:
use Y
State after:
case h
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □''⁻¹X.theory ⊆ Y.theory ∧ □p ⟶ q ∉ Y.theory

State before:
case h
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □''⁻¹X.theory ⊆ Y.theory ∧ □p ⟶ q ∉ Y.theory
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □''⁻¹X.theory ⊆ Y.theory

case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □p ⟶ q ∉ Y.theory

State before:
case h.left
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □''⁻¹X.theory ⊆ Y.theory

case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □p ⟶ q ∉ Y.theory
Tactic:
. assumption;
State after:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □p ⟶ q ∉ Y.theory

State before:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □p ⟶ q ∉ Y.theory
Tactic:
. apply iff_mem_imp.not.mpr; simp [hpY, hqY];
State after:
no goals

State before:
case h.left
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □''⁻¹X.theory ⊆ Y.theory
Tactic:
assumption
State after:
no goals

State before:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ □p ⟶ q ∉ Y.theory
Tactic:
apply iff_mem_imp.not.mpr
State after:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ¬(□p ∈ Y.theory → q ∈ Y.theory)

State before:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
⊢ ¬(□p ∈ Y.theory → q ∈ Y.theory)
Tactic:
simp [hpY, hqY]
State after:
no goals

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □(□q ⟶ p) ∉ X.theory
Tactic:
apply iff_mem_box.not.mpr
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ¬∀ {Ω' : MCT 𝓓}, □''⁻¹X.theory ⊆ Ω'.theory → □q ⟶ p ∈ Ω'.theory

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ¬∀ {Ω' : MCT 𝓓}, □''⁻¹X.theory ⊆ Ω'.theory → □q ⟶ p ∈ Ω'.theory
Tactic:
push_neg
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ∃ Ω', □''⁻¹X.theory ⊆ Ω'.theory ∧ □q ⟶ p ∉ Ω'.theory

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ∃ Ω', □''⁻¹X.theory ⊆ Ω'.theory ∧ □q ⟶ p ∉ Ω'.theory
Tactic:
use Z
State after:
case h
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.theory ∧ □q ⟶ p ∉ Z.theory

State before:
case h
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.theory ∧ □q ⟶ p ∉ Z.theory
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.theory

case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory

State before:
case h.left
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.theory

case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory
Tactic:
. assumption;
State after:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory

State before:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory
Tactic:
. apply iff_mem_imp.not.mpr; simp [hpZ, hqZ];
State after:
no goals

State before:
case h.left
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □''⁻¹X.theory ⊆ Z.theory
Tactic:
assumption
State after:
no goals

State before:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ □q ⟶ p ∉ Z.theory
Tactic:
apply iff_mem_imp.not.mpr
State after:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ¬(□q ∈ Z.theory → p ∈ Z.theory)

State before:
case h.right
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
⊢ ¬(□q ∈ Z.theory → p ∈ Z.theory)
Tactic:
simp [hpZ, hqZ]
State after:
no goals

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
Tactic:
apply iff_mem_or.not.mpr
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ ¬(□(□p ⟶ q) ∈ X.theory ∨ □(□q ⟶ p) ∈ X.theory)

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ ¬(□(□p ⟶ q) ∈ X.theory ∨ □(□q ⟶ p) ∈ X.theory)
Tactic:
push_neg
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ∉ X.theory ∧ □(□q ⟶ p) ∉ X.theory

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ∉ X.theory ∧ □(□q ⟶ p) ∉ X.theory
Tactic:
exact ⟨hpqX, hqpX⟩
State after:
no goals

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ X.theory
Tactic:
apply subset_axiomset _
State after:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ Ax(𝓓)

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ Ax(𝓓)
Tactic:
exact hAx (by aesop)
State after:
no goals

State before:
α : Type u_1
inst✝³ : Inhabited α
inst✝² : DecidableEq α
F : Frame' α
atleast : Atleast 2 α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.Normal
inst✝ : Inhabited (MCT 𝓓)
hAx : .𝟯 ⊆ Ax(𝓓)
X Y Z : MCT 𝓓
hXY : □''⁻¹X.theory ⊆ Y.theory
hXZ : □''⁻¹X.theory ⊆ Z.theory
p : Formula α
hpZ : p ∉ Z.theory
hpY : □p ∈ Y.theory
q : Formula α
hqY : q ∉ Y.theory
hqZ : □q ∈ Z.theory
hpqX : □(□p ⟶ q) ∉ X.theory
hqpX : □(□q ⟶ p) ∉ X.theory
this : □(□p ⟶ q) ⋎ □(□q ⟶ p) ∉ X.theory
⊢ □(□p ⟶ q) ⋎ □(□q ⟶ p) ∈ .𝟯
Tactic:
aesop
State after:
no goals