Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.mem_multibox_dual (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ □^[n]p ∈ Ω.theory ↔ ~(◇^[n](~p)) ∈ Ω.theory
Tactic:
simp [membership_iff]
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p ↔ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p ↔ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p → Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! □^[n]p

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p → Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! □^[n]p
Tactic:
. intro h;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h;
  apply Context.provable_iff.mpr;
  existsi Γ;
  constructor;
  . assumption;
  . exact FiniteContext.provable_iff.mpr $ imp_trans! (FiniteContext.provable_iff.mp hΓ₂) (conj₁'! multiboxDuality!);
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! □^[n]p

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! □^[n]p
Tactic:
. intro h;
  obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h;
  apply Context.provable_iff.mpr;
  existsi Γ;
  constructor;
  . assumption;
  . exact FiniteContext.provable_iff.mpr $ imp_trans! (FiniteContext.provable_iff.mp hΓ₂) (conj₂'! multiboxDuality!);
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! □^[n]p → Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
intro h
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h
State after:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

State before:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
apply Context.provable_iff.mpr
State after:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Ω.theory) ∧ Δ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

State before:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Ω.theory) ∧ Δ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
existsi Γ
State after:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ (∀ q ∈ Γ, q ∈ Ω.theory) ∧ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

State before:
case mp.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ (∀ q ∈ Γ, q ∈ Ω.theory) ∧ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
constructor
State after:
case mp.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∀ q ∈ Γ, q ∈ Ω.theory

case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

State before:
case mp.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∀ q ∈ Γ, q ∈ Ω.theory

case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
. assumption;
State after:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥

State before:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
. exact FiniteContext.provable_iff.mpr $ imp_trans! (FiniteContext.provable_iff.mp hΓ₂) (conj₁'! multiboxDuality!);
State after:
no goals

State before:
case mp.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ ∀ q ∈ Γ, q ∈ Ω.theory
Tactic:
assumption
State after:
no goals

State before:
case mp.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! □^[n]p
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! □^[n]p
⊢ Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Tactic:
exact FiniteContext.provable_iff.mpr $ imp_trans! (FiniteContext.provable_iff.mp hΓ₂) (conj₁'! multiboxDuality!)
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
⊢ Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥ → Ω.theory *⊢[L]! □^[n]p
Tactic:
intro h
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ Ω.theory *⊢[L]! □^[n]p

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ Ω.theory *⊢[L]! □^[n]p
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h
State after:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ Ω.theory *⊢[L]! □^[n]p

State before:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ Ω.theory *⊢[L]! □^[n]p
Tactic:
apply Context.provable_iff.mpr
State after:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Ω.theory) ∧ Δ ⊢[L]! □^[n]p

State before:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Ω.theory) ∧ Δ ⊢[L]! □^[n]p
Tactic:
existsi Γ
State after:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ (∀ q ∈ Γ, q ∈ Ω.theory) ∧ Γ ⊢[L]! □^[n]p

State before:
case mpr.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ (∀ q ∈ Γ, q ∈ Ω.theory) ∧ Γ ⊢[L]! □^[n]p
Tactic:
constructor
State after:
case mpr.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ ∀ q ∈ Γ, q ∈ Ω.theory

case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ Γ ⊢[L]! □^[n]p

State before:
case mpr.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ ∀ q ∈ Γ, q ∈ Ω.theory

case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ Γ ⊢[L]! □^[n]p
Tactic:
. assumption;
State after:
case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ Γ ⊢[L]! □^[n]p

State before:
case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ Γ ⊢[L]! □^[n]p
Tactic:
. exact FiniteContext.provable_iff.mpr $ imp_trans! (FiniteContext.provable_iff.mp hΓ₂) (conj₂'! multiboxDuality!);
State after:
no goals

State before:
case mpr.intro.intro.left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ ∀ q ∈ Γ, q ∈ Ω.theory
Tactic:
assumption
State after:
no goals

State before:
case mpr.intro.intro.right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
n : ℕ
h : Ω.theory *⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
Γ : List (Formula α)
hΓ₁ : ∀ q ∈ Γ, q ∈ Ω.theory
hΓ₂ : Γ ⊢[L]! ◇^[n](p ⟶ ⊥) ⟶ ⊥
⊢ Γ ⊢[L]! □^[n]p
Tactic:
exact FiniteContext.provable_iff.mpr $ imp_trans! (FiniteContext.provable_iff.mp hΓ₂) (conj₂'! multiboxDuality!)
State after:
no goals