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

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ □^[n]Γ.conj' ∈ Ω.theory ↔ ∀ p ∈ Γ, □^[n]p ∈ Ω.theory
Tactic:
simp only [iff_mem_multibox, iff_mem_conj']
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) ↔
    ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) ↔
    ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) →
    ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) →
    ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
Tactic:
. intro h p hp Ω' hΩ';
  exact (h hΩ') p hp;
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
Tactic:
. intro h Ω' hΩ' p hp;
  exact @h p hp Ω' hΩ';
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory) →
    ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Tactic:
intro h p hp Ω' hΩ'
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
Γ : List (Formula α)
n : ℕ
h : ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
p : Formula α
hp : p ∈ Γ
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
⊢ p ∈ Ω'.theory

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
Γ : List (Formula α)
n : ℕ
h : ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
p : Formula α
hp : p ∈ Γ
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
⊢ p ∈ Ω'.theory
Tactic:
exact (h hΩ') p hp
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
Γ : List (Formula α)
n : ℕ
⊢ (∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory) →
    ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → ∀ p ∈ Γ, p ∈ Ω'.theory
Tactic:
intro h Ω' hΩ' p hp
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
Γ : List (Formula α)
n : ℕ
h : ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
p : Formula α
hp : p ∈ Γ
⊢ p ∈ Ω'.theory

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ : Formula α
Γ : List (Formula α)
n : ℕ
h : ∀ p ∈ Γ, ∀ {Ω' : MCT L}, □''⁻¹^[n]Ω.theory ⊆ Ω'.theory → p ∈ Ω'.theory
Ω' : MCT L
hΩ' : □''⁻¹^[n]Ω.theory ⊆ Ω'.theory
p : Formula α
hp : p ∈ Γ
⊢ p ∈ Ω'.theory
Tactic:
exact @h p hp Ω' hΩ'
State after:
no goals