Theorem: LO.System.multiboxConj'_iff! (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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simp;
| hsingle => simp;
| hcons p Γ h ih =>
  simp_all;
  constructor;
  . intro h;
    have := distribute_multibox_and'! h;
    constructor;
    . exact conj₁'! this;
    . exact ih.mp (conj₂'! this);
  . rintro ⟨h₁, h₂⟩;
    exact collect_multibox_and'! $ conj₃'! h₁ (ih.mpr h₂);
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' ↔ ∀ p ∈ [], 𝓢 ⊢! □^[n]p
Tactic:
simp
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' ↔ ∀ p ∈ [a✝], 𝓢 ⊢! □^[n]p
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ 𝓢 ⊢! □^[n](p :: Γ).conj' ↔ ∀ p_1 ∈ p :: Γ, 𝓢 ⊢! □^[n]p_1
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ 𝓢 ⊢! □^[n](p ⋏ Γ.conj') ↔ 𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a

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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ 𝓢 ⊢! □^[n](p ⋏ Γ.conj') ↔ 𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a
Tactic:
constructor
State after:
case hcons.mp
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ 𝓢 ⊢! □^[n](p ⋏ Γ.conj') → 𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a

case hcons.mpr
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ (𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a) → 𝓢 ⊢! □^[n](p ⋏ Γ.conj')

State before:
case hcons.mp
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ 𝓢 ⊢! □^[n](p ⋏ Γ.conj') → 𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a

case hcons.mpr
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ (𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a) → 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
Tactic:
. intro h;
  have := distribute_multibox_and'! h;
  constructor;
  . exact conj₁'! this;
  . exact ih.mp (conj₂'! this);
State after:
case hcons.mpr
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ (𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a) → 𝓢 ⊢! □^[n](p ⋏ Γ.conj')

State before:
case hcons.mpr
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ (𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a) → 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
Tactic:
. rintro ⟨h₁, h₂⟩;
  exact collect_multibox_and'! $ conj₃'! h₁ (ih.mpr h₂);
State after:
no goals

State before:
case hcons.mp
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ 𝓢 ⊢! □^[n](p ⋏ Γ.conj') → 𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a
Tactic:
intro h
State after:
case hcons.mp
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
⊢ 𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a

State before:
case hcons.mp
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
⊢ 𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a
Tactic:
have := distribute_multibox_and'! h
State after:
case hcons.mp
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ 𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a

State before:
case hcons.mp
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ 𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a
Tactic:
constructor
State after:
case hcons.mp.left
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ 𝓢 ⊢! □^[n]p

case hcons.mp.right
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a

State before:
case hcons.mp.left
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ 𝓢 ⊢! □^[n]p

case hcons.mp.right
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a
Tactic:
. exact conj₁'! this;
State after:
case hcons.mp.right
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a

State before:
case hcons.mp.right
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a
Tactic:
. exact ih.mp (conj₂'! this);
State after:
no goals

State before:
case hcons.mp.left
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ 𝓢 ⊢! □^[n]p
Tactic:
exact conj₁'! this
State after:
no goals

State before:
case hcons.mp.right
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h : 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
this : 𝓢 ⊢! □^[n]p ⋏ □^[n]Γ.conj'
⊢ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a
Tactic:
exact ih.mp (conj₂'! this)
State after:
no goals

State before:
case hcons.mpr
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
⊢ (𝓢 ⊢! □^[n]p ∧ ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a) → 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
Tactic:
rintro ⟨h₁, h₂⟩
State after:
case hcons.mpr.intro
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h₁ : 𝓢 ⊢! □^[n]p
h₂ : ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a
⊢ 𝓢 ⊢! □^[n](p ⋏ Γ.conj')

State before:
case hcons.mpr.intro
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' ↔ ∀ p ∈ Γ, 𝓢 ⊢! □^[n]p
h₁ : 𝓢 ⊢! □^[n]p
h₂ : ∀ a ∈ Γ, 𝓢 ⊢! □^[n]a
⊢ 𝓢 ⊢! □^[n](p ⋏ Γ.conj')
Tactic:
exact collect_multibox_and'! $ conj₃'! h₁ (ih.mpr h₂)
State after:
no goals