Theorem: LO.System.collect_multibox_conj'! (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 : ℕ
⊢ 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simpa using dhyp! multiboxverum!;
| hsingle => simp;
| hcons p Γ h ih =>
  simp_all;
  exact imp_trans! (implyRightAnd! (generalConj'! (by simp)) (imp_trans! (by simp) ih)) collect_multibox_and!;
State after:
no goals

State before:
case hnil
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 : ℕ
⊢ 𝓢 ⊢! (□'^[n][]).conj' ⟶ □^[n][].conj'
Tactic:
simpa using dhyp! multiboxverum!
State after:
no goals

State before:
case hsingle
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 : ℕ
a✝ : F
⊢ 𝓢 ⊢! (□'^[n][a✝]).conj' ⟶ □^[n][a✝].conj'
Tactic:
simp
State after:
no goals

State before:
case hcons
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 : ℕ
p : F
Γ : List F
h : Γ ≠ []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ 𝓢 ⊢! (□'^[n](p :: Γ)).conj' ⟶ □^[n](p :: Γ).conj'
Tactic:
simp_all
State after:
case hcons
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 : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ 𝓢 ⊢! (□'^[n](p :: Γ)).conj' ⟶ □^[n](p ⋏ Γ.conj')

State before:
case hcons
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 : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ 𝓢 ⊢! (□'^[n](p :: Γ)).conj' ⟶ □^[n](p ⋏ Γ.conj')
Tactic:
exact imp_trans! (implyRightAnd! (generalConj'! (by simp)) (imp_trans! (by simp) ih)) collect_multibox_and!
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 : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ □^[n]p ∈ □'^[n](p :: Γ)
Tactic:
simp
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 : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! (□'^[n]Γ).conj' ⟶ □^[n]Γ.conj'
⊢ 𝓢 ⊢! (□'^[n](p :: Γ)).conj' ⟶ (□'^[n]Γ).conj'
Tactic:
simp
State after:
no goals