Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
induction n generalizing Ω₁ Ω₂ with
| zero =>
  simp_all;
  constructor;
  . intro h; subst h; tauto;
  . intro h; apply intro_equality; simpa;
| succ n ih =>
  constructor;
  . simp;
    intro Ω₃ h₁₃ h₃₂ p h;
    exact ih.mp h₃₂ $ h₁₃ h;
  . intro h;
    obtain ⟨Ω, hΩ⟩ := lindenbaum (L := L) (T := (□''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory)) $ by
      apply intro_union_ParametricConsistent;
      intro Γ Δ hΓ hΔ hC;
      replace hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory := by simpa using hΓ;
      have dΓconj : Ω₁.theory *⊢[L]! □Γ.conj' := membership_iff.mp $ iff_mem_box_conj'.mpr hΓ;
      have hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory := by
        intro p hp;
        simpa using hΔ (◇^[n]p) (by simp_all);
      have hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory := iff_mem_conj'.mpr hΔ₂;
      have : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj') := imp_trans! (andImplyIffImplyImply'!.mp hC)
        $ contra₂'! $ imp_trans! (conj₂'! multidiaDuality!)
        $ imp_trans! iff_conj'multidia_multidiaconj'! $ by
          apply conj'conj'_subset;
          intro q hq;
          obtain ⟨r, _, _⟩ := by simpa using hΔ q hq;
          subst_vars;
          simpa;
      have : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj') := by simpa only [UnaryModalOperator.multimop_succ] using imply_box_distribute'! this;
      have : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory := iff_mem_neg.mp $ h $ membership_iff.mpr $ (Context.of! this) ⨀ dΓconj;
      contradiction;
    existsi Ω;
    constructor;
    . intro p hp;
      apply hΩ;
      simp_all;
    . apply ih.mpr;
      apply multibox_multidia.mpr;
      intro p hp;
      apply hΩ;
      simp_all;
State after:
no goals

State before:
case zero
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[0] Ω₂ ↔ ∀ {p : Formula α}, □^[0]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
simp_all
State after:
case zero
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ ↔ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory

State before:
case zero
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ ↔ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
constructor
State after:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ → ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory

case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂

State before:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ → ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory

case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂
Tactic:
. intro h; subst h; tauto;
State after:
case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂

State before:
case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂
Tactic:
. intro h; apply intro_equality; simpa;
State after:
no goals

State before:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ = Ω₂ → ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
intro h
State after:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ = Ω₂
⊢ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory

State before:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
h : Ω₁ = Ω₂
⊢ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
subst h
State after:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ : (CanonicalFrame L).World
⊢ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₁.theory

State before:
case zero.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ : (CanonicalFrame L).World
⊢ ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₁.theory
Tactic:
tauto
State after:
no goals

State before:
case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ = Ω₂
Tactic:
intro h
State after:
case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ = Ω₂

State before:
case zero.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ = Ω₂
Tactic:
apply intro_equality
State after:
case zero.mpr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory

State before:
case zero.mpr.h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ p ∈ Ω₁.theory, p ∈ Ω₂.theory
Tactic:
simpa
State after:
no goals

State before:
case succ
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n + 1] Ω₂ ↔ ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
constructor
State after:
case succ.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n + 1] Ω₂ → ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory

case succ.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n + 1] Ω₂

State before:
case succ.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n + 1] Ω₂ → ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory

case succ.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n + 1] Ω₂
Tactic:
. simp;
  intro Ω₃ h₁₃ h₃₂ p h;
  exact ih.mp h₃₂ $ h₁₃ h;
State after:
case succ.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n + 1] Ω₂

State before:
case succ.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n + 1] Ω₂
Tactic:
. intro h;
  obtain ⟨Ω, hΩ⟩ := lindenbaum (L := L) (T := (□''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory)) $ by
    apply intro_union_ParametricConsistent;
    intro Γ Δ hΓ hΔ hC;
    replace hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory := by simpa using hΓ;
    have dΓconj : Ω₁.theory *⊢[L]! □Γ.conj' := membership_iff.mp $ iff_mem_box_conj'.mpr hΓ;
    have hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory := by
      intro p hp;
      simpa using hΔ (◇^[n]p) (by simp_all);
    have hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory := iff_mem_conj'.mpr hΔ₂;
    have : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj') := imp_trans! (andImplyIffImplyImply'!.mp hC)
      $ contra₂'! $ imp_trans! (conj₂'! multidiaDuality!)
      $ imp_trans! iff_conj'multidia_multidiaconj'! $ by
        apply conj'conj'_subset;
        intro q hq;
        obtain ⟨r, _, _⟩ := by simpa using hΔ q hq;
        subst_vars;
        simpa;
    have : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj') := by simpa only [UnaryModalOperator.multimop_succ] using imply_box_distribute'! this;
    have : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory := iff_mem_neg.mp $ h $ membership_iff.mpr $ (Context.of! this) ⨀ dΓconj;
    contradiction;
  existsi Ω;
  constructor;
  . intro p hp;
    apply hΩ;
    simp_all;
  . apply ih.mpr;
    apply multibox_multidia.mpr;
    intro p hp;
    apply hΩ;
    simp_all;
State after:
no goals

State before:
case succ.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ Ω₁ ≺^[n + 1] Ω₂ → ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
simp
State after:
case succ.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ ∀ (x : MCT L),
    (∀ {p : Formula α}, □p ∈ Ω₁.theory → p ∈ x.theory) →
      RelItr (fun x x_1 => ∀ {p : Formula α}, □p ∈ x.theory → p ∈ x_1.theory) n x Ω₂ →
        ∀ {p : Formula α}, UnaryModalOperator.mop true ((UnaryModalOperator.mop true)^[n] p) ∈ Ω₁.theory → p ∈ Ω₂.theory

State before:
case succ.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ ∀ (x : MCT L),
    (∀ {p : Formula α}, □p ∈ Ω₁.theory → p ∈ x.theory) →
      RelItr (fun x x_1 => ∀ {p : Formula α}, □p ∈ x.theory → p ∈ x_1.theory) n x Ω₂ →
        ∀ {p : Formula α}, UnaryModalOperator.mop true ((UnaryModalOperator.mop true)^[n] p) ∈ Ω₁.theory → p ∈ Ω₂.theory
Tactic:
intro Ω₃ h₁₃ h₃₂ p h
State after:
case succ.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
Ω₃ : MCT L
h₁₃ : ∀ {p : Formula α}, □p ∈ Ω₁.theory → p ∈ Ω₃.theory
h₃₂ : RelItr (fun x x_1 => ∀ {p : Formula α}, □p ∈ x.theory → p ∈ x_1.theory) n Ω₃ Ω₂
p : Formula α
h : UnaryModalOperator.mop true ((UnaryModalOperator.mop true)^[n] p) ∈ Ω₁.theory
⊢ p ∈ Ω₂.theory

State before:
case succ.mp
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
Ω₃ : MCT L
h₁₃ : ∀ {p : Formula α}, □p ∈ Ω₁.theory → p ∈ Ω₃.theory
h₃₂ : RelItr (fun x x_1 => ∀ {p : Formula α}, □p ∈ x.theory → p ∈ x_1.theory) n Ω₃ Ω₂
p : Formula α
h : UnaryModalOperator.mop true ((UnaryModalOperator.mop true)^[n] p) ∈ Ω₁.theory
⊢ p ∈ Ω₂.theory
Tactic:
exact ih.mp h₃₂ $ h₁₃ h
State after:
no goals

State before:
case succ.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
⊢ (∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory) → Ω₁ ≺^[n + 1] Ω₂
Tactic:
intro h
State after:
case succ.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ ≺^[n + 1] Ω₂

State before:
case succ.mpr
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ Ω₁ ≺^[n + 1] Ω₂
Tactic:
obtain ⟨Ω, hΩ⟩ := lindenbaum (L := L) (T := (□''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory)) $ by
  apply intro_union_ParametricConsistent;
  intro Γ Δ hΓ hΔ hC;
  replace hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory := by simpa using hΓ;
  have dΓconj : Ω₁.theory *⊢[L]! □Γ.conj' := membership_iff.mp $ iff_mem_box_conj'.mpr hΓ;
  have hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory := by
    intro p hp;
    simpa using hΔ (◇^[n]p) (by simp_all);
  have hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory := iff_mem_conj'.mpr hΔ₂;
  have : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj') := imp_trans! (andImplyIffImplyImply'!.mp hC)
    $ contra₂'! $ imp_trans! (conj₂'! multidiaDuality!)
    $ imp_trans! iff_conj'multidia_multidiaconj'! $ by
      apply conj'conj'_subset;
      intro q hq;
      obtain ⟨r, _, _⟩ := by simpa using hΔ q hq;
      subst_vars;
      simpa;
  have : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj') := by simpa only [UnaryModalOperator.multimop_succ] using imply_box_distribute'! this;
  have : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory := iff_mem_neg.mp $ h $ membership_iff.mpr $ (Context.of! this) ⨀ dΓconj;
  contradiction;
State after:
case succ.mpr.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ Ω₁ ≺^[n + 1] Ω₂

State before:
case succ.mpr.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ Ω₁ ≺^[n + 1] Ω₂
Tactic:
existsi Ω
State after:
case succ.mpr.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ (fun x x_1 => x ≺ x_1) Ω₁ Ω ∧ RelItr (fun x x_1 => x ≺ x_1) n Ω Ω₂

State before:
case succ.mpr.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ (fun x x_1 => x ≺ x_1) Ω₁ Ω ∧ RelItr (fun x x_1 => x ≺ x_1) n Ω Ω₂
Tactic:
constructor
State after:
case succ.mpr.intro.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ (fun x x_1 => x ≺ x_1) Ω₁ Ω

case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ RelItr (fun x x_1 => x ≺ x_1) n Ω Ω₂

State before:
case succ.mpr.intro.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ (fun x x_1 => x ≺ x_1) Ω₁ Ω

case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ RelItr (fun x x_1 => x ≺ x_1) n Ω Ω₂
Tactic:
. intro p hp;
  apply hΩ;
  simp_all;
State after:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ RelItr (fun x x_1 => x ≺ x_1) n Ω Ω₂

State before:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ RelItr (fun x x_1 => x ≺ x_1) n Ω Ω₂
Tactic:
. apply ih.mpr;
  apply multibox_multidia.mpr;
  intro p hp;
  apply hΩ;
  simp_all;
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ (L)-Consistent (□''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory)
Tactic:
apply intro_union_ParametricConsistent
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ {Γ₁ Γ₂ : List (Formula α)},
    (∀ p ∈ Γ₁, p ∈ □''⁻¹Ω₁.theory) → (∀ p ∈ Γ₂, p ∈ ◇''^[n]Ω₂.theory) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
⊢ ∀ {Γ₁ Γ₂ : List (Formula α)},
    (∀ p ∈ Γ₁, p ∈ □''⁻¹Ω₁.theory) → (∀ p ∈ Γ₂, p ∈ ◇''^[n]Ω₂.theory) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Tactic:
intro Γ Δ hΓ hΔ hC
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ □''⁻¹Ω₁.theory
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ □''⁻¹Ω₁.theory
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False
Tactic:
replace hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory := by simpa using hΓ;
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
⊢ False

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
⊢ False
Tactic:
have dΓconj : Ω₁.theory *⊢[L]! □Γ.conj' := membership_iff.mp $ iff_mem_box_conj'.mpr hΓ
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
⊢ False

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
⊢ False
Tactic:
have hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory := by
  intro p hp;
  simpa using hΔ (◇^[n]p) (by simp_all);
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
⊢ False

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
⊢ False
Tactic:
have hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory := iff_mem_conj'.mpr hΔ₂
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ False

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ False
Tactic:
have : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj') := imp_trans! (andImplyIffImplyImply'!.mp hC)
  $ contra₂'! $ imp_trans! (conj₂'! multidiaDuality!)
  $ imp_trans! iff_conj'multidia_multidiaconj'! $ by
    apply conj'conj'_subset;
    intro q hq;
    obtain ⟨r, _, _⟩ := by simpa using hΔ q hq;
    subst_vars;
    simpa;
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
⊢ False

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
⊢ False
Tactic:
have : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj') := by simpa only [UnaryModalOperator.multimop_succ] using imply_box_distribute'! this;
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this✝ : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
this : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
⊢ False

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this✝ : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
this : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
⊢ False
Tactic:
have : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory := iff_mem_neg.mp $ h $ membership_iff.mpr $ (Context.of! this) ⨀ dΓconj
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this✝¹ : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
this✝ : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
this : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory
⊢ False

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this✝¹ : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
this✝ : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
this : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ □''⁻¹Ω₁.theory
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ ∀ p ∈ Γ, □p ∈ Ω₁.theory
Tactic:
simpa using hΓ
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
⊢ ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
Tactic:
intro p hp
State after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
p : Formula α
hp : p ∈ ◇'⁻¹^[n]Δ
⊢ p ∈ Ω₂.theory

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
p : Formula α
hp : p ∈ ◇'⁻¹^[n]Δ
⊢ p ∈ Ω₂.theory
Tactic:
simpa using hΔ (◇^[n]p) (by simp_all)
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
p : Formula α
hp : p ∈ ◇'⁻¹^[n]Δ
⊢ ◇^[n]p ∈ Δ
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ L ⊢! (◇'^[n]◇'⁻¹^[n]Δ).conj' ⟶ Δ.conj'
Tactic:
apply conj'conj'_subset
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ ∀ p ∈ Δ, p ∈ ◇'^[n]◇'⁻¹^[n]Δ

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ ∀ p ∈ Δ, p ∈ ◇'^[n]◇'⁻¹^[n]Δ
Tactic:
intro q hq
State after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
⊢ q ∈ ◇'^[n]◇'⁻¹^[n]Δ

State before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
⊢ q ∈ ◇'^[n]◇'⁻¹^[n]Δ
Tactic:
obtain ⟨r, _, _⟩ := by simpa using hΔ q hq;
State after:
case h.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
r : Formula α
left✝ : r ∈ Ω₂.theory
right✝ : (UnaryModalOperator.mop false)^[n] r = q
⊢ q ∈ ◇'^[n]◇'⁻¹^[n]Δ

State before:
case h.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
r : Formula α
left✝ : r ∈ Ω₂.theory
right✝ : (UnaryModalOperator.mop false)^[n] r = q
⊢ q ∈ ◇'^[n]◇'⁻¹^[n]Δ
Tactic:
subst_vars
State after:
case h.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
r : Formula α
left✝ : r ∈ Ω₂.theory
hq : (UnaryModalOperator.mop false)^[n] r ∈ Δ
⊢ (UnaryModalOperator.mop false)^[n] r ∈ ◇'^[n]◇'⁻¹^[n]Δ

State before:
case h.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
r : Formula α
left✝ : r ∈ Ω₂.theory
hq : (UnaryModalOperator.mop false)^[n] r ∈ Δ
⊢ (UnaryModalOperator.mop false)^[n] r ∈ ◇'^[n]◇'⁻¹^[n]Δ
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
⊢ ?m.521811
Tactic:
simpa using hΔ q hq
State after:
no goals

State before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
⊢ L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
Tactic:
simpa only [UnaryModalOperator.multimop_succ] using imply_box_distribute'! this
State after:
no goals

State before:
case succ.mpr.intro.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ (fun x x_1 => x ≺ x_1) Ω₁ Ω
Tactic:
intro p hp
State after:
case succ.mpr.intro.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ □''⁻¹Ω₁.theory
⊢ p ∈ Ω.theory

State before:
case succ.mpr.intro.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ □''⁻¹Ω₁.theory
⊢ p ∈ Ω.theory
Tactic:
apply hΩ
State after:
case succ.mpr.intro.left.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ □''⁻¹Ω₁.theory
⊢ p ∈ □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory

State before:
case succ.mpr.intro.left.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ □''⁻¹Ω₁.theory
⊢ p ∈ □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory
Tactic:
simp_all
State after:
no goals

State before:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ RelItr (fun x x_1 => x ≺ x_1) n Ω Ω₂
Tactic:
apply ih.mpr
State after:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω.theory → p ∈ Ω₂.theory

State before:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω.theory → p ∈ Ω₂.theory
Tactic:
apply multibox_multidia.mpr
State after:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω.theory

State before:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω.theory
Tactic:
intro p hp
State after:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ Ω₂.theory
⊢ ◇^[n]p ∈ Ω.theory

State before:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ Ω₂.theory
⊢ ◇^[n]p ∈ Ω.theory
Tactic:
apply hΩ
State after:
case succ.mpr.intro.right.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ Ω₂.theory
⊢ ◇^[n]p ∈ □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory

State before:
case succ.mpr.intro.right.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ Ω₂.theory
⊢ ◇^[n]p ∈ □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory
Tactic:
simp_all
State after:
no goals