Theorem: LO.Modal.Standard.Kripke.definability_canonicalFrame_GeachAxiom (Logic/Modal/Standard/Kripke/Geach/Completeness.lean)

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
⊢ GeachConfluent t (CanonicalFrame L)
Tactic:
have : L.Normal := ⟨⟩
State after:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
⊢ GeachConfluent t (CanonicalFrame L)

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
⊢ GeachConfluent t (CanonicalFrame L)
Tactic:
intro Ω₁ Ω₂ Ω₃ h
State after:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
h : Ω₁ ≺^[t.i] Ω₂ ∧ Ω₁ ≺^[t.j] Ω₃
⊢ ∃ u, Ω₂ ≺^[t.m] u ∧ Ω₃ ≺^[t.n] u

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
h : Ω₁ ≺^[t.i] Ω₂ ∧ Ω₁ ≺^[t.j] Ω₃
⊢ ∃ u, Ω₂ ≺^[t.m] u ∧ Ω₃ ≺^[t.n] u
Tactic:
have ⟨r₁₂, r₁₃⟩ := h
State after:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
h : Ω₁ ≺^[t.i] Ω₂ ∧ Ω₁ ≺^[t.j] Ω₃
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
⊢ ∃ u, Ω₂ ≺^[t.m] u ∧ Ω₃ ≺^[t.n] u

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
h : Ω₁ ≺^[t.i] Ω₂ ∧ Ω₁ ≺^[t.j] Ω₃
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
⊢ ∃ u, Ω₂ ≺^[t.m] u ∧ Ω₃ ≺^[t.n] u
Tactic:
clear h
State after:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
⊢ ∃ u, Ω₂ ≺^[t.m] u ∧ Ω₃ ≺^[t.n] u

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
⊢ ∃ u, Ω₂ ≺^[t.m] u ∧ Ω₃ ≺^[t.n] u
Tactic:
have ⟨Ω, hΩ⟩ := MaximalParametricConsistentTheory.lindenbaum (L := L) (T := ((□''⁻¹^[t.m]Ω₂.theory) ∪ (□''⁻¹^[t.n]Ω₃.theory))) $ by
  apply intro_union_ParametricConsistent;
  intro Γ Δ hΓ hΔ hC;
  replace hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory := by simpa using hΓ;
  have hΓconj : □^[t.m](Γ.conj') ∈ Ω₂.theory := iff_mem_multibox_conj'.mpr hΓ;
  replace hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory := by simpa using hΔ;
  have : □^[t.n](Δ.conj') ∈ Ω₃.theory := iff_mem_multibox_conj'.mpr hΔ;
  have : □^[t.j](◇^[t.n](Γ.conj')) ∈ Ω₁.theory := iff_mem_imp.mp
    (membership_iff.mpr $ Context.of! ⟨Deduction.maxm (by apply hAx; simp_all)⟩)
    (multiframe_def_multidia.mp r₁₂ hΓconj)
  have : ◇^[t.n]Γ.conj' ∈ Ω₃.theory := multiframe_def_multibox.mp r₁₃ this;
  have : L ⊢! □^[t.n](Δ.conj') ⋏ ◇^[t.n](Γ.conj') ⟶ ⊥ := by
    apply andImplyIffImplyImply'!.mpr;
    exact imp_trans!
      (show L ⊢! □^[t.n](Δ.conj') ⟶ □^[t.n](~Γ.conj') by exact imply_multibox_distribute'! $ contra₁'! $ andImplyIffImplyImply'!.mp hC)
      (show L ⊢! □^[t.n](~Γ.conj') ⟶ ~(◇^[t.n]Γ.conj') by exact contra₁'! $ conj₁'! $ multidiaDuality!);
  have : L ⊬! □^[t.n](Δ.conj') ⋏ ◇^[t.n](Γ.conj') ⟶ ⊥ := by simpa using Ω₃.consistent (Γ := [□^[t.n](Δ.conj'), ◇^[t.n](Γ.conj')]) (by simp_all)
  contradiction;
State after:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ ∃ u, Ω₂ ≺^[t.m] u ∧ Ω₃ ≺^[t.n] u

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ ∃ u, Ω₂ ≺^[t.m] u ∧ Ω₃ ≺^[t.n] u
Tactic:
existsi Ω
State after:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ Ω₂ ≺^[t.m] Ω ∧ Ω₃ ≺^[t.n] Ω

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ Ω₂ ≺^[t.m] Ω ∧ Ω₃ ≺^[t.n] Ω
Tactic:
simp [multiframe_def_multibox]
State after:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ (∀ {p : Formula α}, □^[t.m]p ∈ Ω₂.theory → p ∈ Ω.theory) ∧ ∀ {p : Formula α}, □^[t.n]p ∈ Ω₃.theory → p ∈ Ω.theory

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ (∀ {p : Formula α}, □^[t.m]p ∈ Ω₂.theory → p ∈ Ω.theory) ∧ ∀ {p : Formula α}, □^[t.n]p ∈ Ω₃.theory → p ∈ Ω.theory
Tactic:
constructor <;> { intros; apply hΩ; simp_all; }
State after:
no goals

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
⊢ (L)-Consistent (□''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory)
Tactic:
apply intro_union_ParametricConsistent
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
⊢ ∀ {Γ₁ Γ₂ : List (Formula α)},
    (∀ p ∈ Γ₁, p ∈ □''⁻¹^[t.m]Ω₂.theory) → (∀ p ∈ Γ₂, p ∈ □''⁻¹^[t.n]Ω₃.theory) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
⊢ ∀ {Γ₁ Γ₂ : List (Formula α)},
    (∀ p ∈ Γ₁, p ∈ □''⁻¹^[t.m]Ω₂.theory) → (∀ p ∈ Γ₂, p ∈ □''⁻¹^[t.n]Ω₃.theory) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Tactic:
intro Γ Δ hΓ hΔ hC
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ □''⁻¹^[t.m]Ω₂.theory
hΔ : ∀ p ∈ Δ, p ∈ □''⁻¹^[t.n]Ω₃.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ □''⁻¹^[t.m]Ω₂.theory
hΔ : ∀ p ∈ Δ, p ∈ □''⁻¹^[t.n]Ω₃.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False
Tactic:
replace hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory := by simpa using hΓ;
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ □''⁻¹^[t.n]Ω₃.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
⊢ False

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ □''⁻¹^[t.n]Ω₃.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
⊢ False
Tactic:
have hΓconj : □^[t.m](Γ.conj') ∈ Ω₂.theory := iff_mem_multibox_conj'.mpr hΓ
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ □''⁻¹^[t.n]Ω₃.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
⊢ False

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ □''⁻¹^[t.n]Ω₃.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
⊢ False
Tactic:
replace hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory := by simpa using hΔ;
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
⊢ False

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
⊢ False
Tactic:
have : □^[t.n](Δ.conj') ∈ Ω₃.theory := iff_mem_multibox_conj'.mpr hΔ
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this : □^[t.n]Δ.conj' ∈ Ω₃.theory
⊢ False

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this : □^[t.n]Δ.conj' ∈ Ω₃.theory
⊢ False
Tactic:
have : □^[t.j](◇^[t.n](Γ.conj')) ∈ Ω₁.theory := iff_mem_imp.mp
  (membership_iff.mpr $ Context.of! ⟨Deduction.maxm (by apply hAx; simp_all)⟩)
  (multiframe_def_multidia.mp r₁₂ hΓconj)
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝¹ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
⊢ False

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝¹ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
⊢ False
Tactic:
have : ◇^[t.n]Γ.conj' ∈ Ω₃.theory := multiframe_def_multibox.mp r₁₃ this
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ False

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ False
Tactic:
have : L ⊢! □^[t.n](Δ.conj') ⋏ ◇^[t.n](Γ.conj') ⟶ ⊥ := by
  apply andImplyIffImplyImply'!.mpr;
  exact imp_trans!
    (show L ⊢! □^[t.n](Δ.conj') ⟶ □^[t.n](~Γ.conj') by exact imply_multibox_distribute'! $ contra₁'! $ andImplyIffImplyImply'!.mp hC)
    (show L ⊢! □^[t.n](~Γ.conj') ⟶ ~(◇^[t.n]Γ.conj') by exact contra₁'! $ conj₁'! $ multidiaDuality!);
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝³ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝² : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝¹ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this✝ : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
this : L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
⊢ False

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝³ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝² : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝¹ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this✝ : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
this : L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊬! □^[t.n](Δ.conj') ⋏ ◇^[t.n](Γ.conj') ⟶ ⊥ := by simpa using Ω₃.consistent (Γ := [□^[t.n](Δ.conj'), ◇^[t.n](Γ.conj')]) (by simp_all)
State after:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝⁴ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝³ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝² : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this✝¹ : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
this✝ : L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
this : L ⊬! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
⊢ False

State before:
case h
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝⁴ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝³ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝² : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this✝¹ : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
this✝ : L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
this : L ⊬! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ □''⁻¹^[t.m]Ω₂.theory
hΔ : ∀ p ∈ Δ, p ∈ □''⁻¹^[t.n]Ω₃.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
Tactic:
simpa using hΓ
State after:
no goals

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ □''⁻¹^[t.n]Ω₃.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
⊢ ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
Tactic:
simpa using hΔ
State after:
no goals

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this : □^[t.n]Δ.conj' ∈ Ω₃.theory
⊢ ◇^[t.i](□^[t.m]Γ.conj') ⟶ □^[t.j](◇^[t.n]Γ.conj') ∈ Ax(L)
Tactic:
apply hAx
State after:
case a
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this : □^[t.n]Δ.conj' ∈ Ω₃.theory
⊢ ◇^[t.i](□^[t.m]Γ.conj') ⟶ □^[t.j](◇^[t.n]Γ.conj') ∈ 𝗴𝗲(t)

State before:
case a
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this : □^[t.n]Δ.conj' ∈ Ω₃.theory
⊢ ◇^[t.i](□^[t.m]Γ.conj') ⟶ □^[t.j](◇^[t.n]Γ.conj') ∈ 𝗴𝗲(t)
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
Tactic:
apply andImplyIffImplyImply'!.mpr
State after:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n]Δ.conj' ⟶ ◇^[t.n]Γ.conj' ⟶ ⊥

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n]Δ.conj' ⟶ ◇^[t.n]Γ.conj' ⟶ ⊥
Tactic:
exact imp_trans!
  (show L ⊢! □^[t.n](Δ.conj') ⟶ □^[t.n](~Γ.conj') by exact imply_multibox_distribute'! $ contra₁'! $ andImplyIffImplyImply'!.mp hC)
  (show L ⊢! □^[t.n](~Γ.conj') ⟶ ~(◇^[t.n]Γ.conj') by exact contra₁'! $ conj₁'! $ multidiaDuality!)
State after:
no goals

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n]Δ.conj' ⟶ □^[t.n](~Γ.conj')
Tactic:
exact imply_multibox_distribute'! $ contra₁'! $ andImplyIffImplyImply'!.mp hC
State after:
no goals

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝² : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝¹ : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
⊢ L ⊢! □^[t.n](~Γ.conj') ⟶ ~(◇^[t.n]Γ.conj')
Tactic:
exact contra₁'! $ conj₁'! $ multidiaDuality!
State after:
no goals

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝³ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝² : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝¹ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this✝ : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
this : L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
⊢ L ⊬! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
Tactic:
simpa using Ω₃.consistent (Γ := [□^[t.n](Δ.conj'), ◇^[t.n](Γ.conj')]) (by simp_all)
State after:
no goals

State before:
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this✝³ : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Γ Δ : List (Formula α)
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □^[t.m]p ∈ Ω₂.theory
hΓconj : □^[t.m]Γ.conj' ∈ Ω₂.theory
hΔ : ∀ p ∈ Δ, □^[t.n]p ∈ Ω₃.theory
this✝² : □^[t.n]Δ.conj' ∈ Ω₃.theory
this✝¹ : □^[t.j](◇^[t.n]Γ.conj') ∈ Ω₁.theory
this✝ : ◇^[t.n]Γ.conj' ∈ Ω₃.theory
this : L ⊢! □^[t.n]Δ.conj' ⋏ ◇^[t.n]Γ.conj' ⟶ ⊥
⊢ ∀ p ∈ [□^[t.n]Δ.conj', ◇^[t.n]Γ.conj'], p ∈ Ω₃.theory
Tactic:
simp_all
State after:
no goals

State before:
case right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, □^[t.n]p ∈ Ω₃.theory → p ∈ Ω.theory
Tactic:
intros
State after:
case right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
p✝ : Formula α
a✝ : □^[t.n]p✝ ∈ Ω₃.theory
⊢ p✝ ∈ Ω.theory

State before:
case right
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
p✝ : Formula α
a✝ : □^[t.n]p✝ ∈ Ω₃.theory
⊢ p✝ ∈ Ω.theory
Tactic:
apply hΩ
State after:
case right.a
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
p✝ : Formula α
a✝ : □^[t.n]p✝ ∈ Ω₃.theory
⊢ p✝ ∈ □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory

State before:
case right.a
α : Type u_1
Λ : AxiomSet α
inst✝³ : Inhabited α
inst✝² : DecidableEq α
t : Axioms.Geach.Taple
L : DeductionParameter α
inst✝¹ : L.HasNecOnly
includeK : L.IncludeK
inst✝ : Inhabited (MCT L)
hAx : 𝗴𝗲(t) ⊆ Ax(L)
this : L.Normal
Ω₁ Ω₂ Ω₃ : (CanonicalFrame L).World
r₁₂ : Ω₁ ≺^[t.i] Ω₂
r₁₃ : Ω₁ ≺^[t.j] Ω₃
Ω : MCT L
hΩ : □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory ⊆ Ω.theory
p✝ : Formula α
a✝ : □^[t.n]p✝ ∈ Ω₃.theory
⊢ p✝ ∈ □''⁻¹^[t.m]Ω₂.theory ∪ □''⁻¹^[t.n]Ω₃.theory
Tactic:
simp_all
State after:
no goals