Theorem: LO.System.multiboxconj'_of_conj'multibox! (Logic/Modal/Standard/HilbertStyle.lean)

State before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
⊢ 𝓢 ⊢! □^[n]Γ.conj'
Tactic:
apply multiboxConj'_iff!.mpr
State after:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
⊢ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p

State before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
⊢ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
Tactic:
intro p hp
State after:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
p : F
hp : p ∈ Γ
⊢ 𝓢 ⊢! □^[n]p

State before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
p : F
hp : p ∈ Γ
⊢ 𝓢 ⊢! □^[n]p
Tactic:
exact iff_provable_list_conj.mp d (□^[n]p) (by aesop)
State after:
no goals

State before:
F : Type u_1
inst✝⁷ : StandardModalLogicalConnective F
inst✝⁶ : DecidableEq F
S : Type u_2
inst✝⁵ : System F S
p✝ q r : F
Γ Δ : List F
𝓢 : S
inst✝⁴ : Classical 𝓢
inst✝³ : System.NegationEquiv 𝓢
inst✝² : Necessitation 𝓢
inst✝¹ inst✝ : HasAxiomK 𝓢
n : ℕ
d : 𝓢 ⊢! (□'^[n]Γ).conj'
p : F
hp : p ∈ Γ
⊢ □^[n]p ∈ □'^[n]Γ
Tactic:
aesop
State after:
no goals