internlm/Lean-Github huggingface dataset:
Theorem: LO.System.Necessitation.multinec!
Proof state before:
case 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 𝓢
n : ℕ
hp : 𝓢 ⊢ p
⊢ 𝓢 ⊢! □^[n]p
Tactic:
exact ⟨multinec hp⟩
Proof state after:
no goals
Theorem: LO.System.multiboxDuality'!
Proof 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]p ↔ 𝓢 ⊢! ~(◇^[n](~p))
Tactic:
constructor
Proof state after:
case 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 : ℕ
⊢ 𝓢 ⊢! □^[n]p → 𝓢 ⊢! ~(◇^[n](~p))

case 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 : ℕ
⊢ 𝓢 ⊢! ~(◇^[n](~p)) → 𝓢 ⊢! □^[n]p
Theorem: LO.System.multiboxDuality'!
Proof state before:
case 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 : ℕ
⊢ 𝓢 ⊢! □^[n]p → 𝓢 ⊢! ~(◇^[n](~p))

case 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 : ℕ
⊢ 𝓢 ⊢! ~(◇^[n](~p)) → 𝓢 ⊢! □^[n]p
Tactic:
. intro h; exact (conj₁'! multiboxDuality!) ⨀ h;
Proof state after:
case 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 : ℕ
⊢ 𝓢 ⊢! ~(◇^[n](~p)) → 𝓢 ⊢! □^[n]p
Theorem: LO.System.multiboxDuality'!
Proof state before:
case 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 : ℕ
⊢ 𝓢 ⊢! ~(◇^[n](~p)) → 𝓢 ⊢! □^[n]p
Tactic:
. intro h; exact (conj₂'! multiboxDuality!) ⨀ h;
Proof state after:
no goals
Theorem: LO.System.multiboxDuality'!
Proof state before:
case 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 : ℕ
⊢ 𝓢 ⊢! □^[n]p → 𝓢 ⊢! ~(◇^[n](~p))
Tactic:
intro h
Proof state after:
case 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 : ℕ
h : 𝓢 ⊢! □^[n]p
⊢ 𝓢 ⊢! ~(◇^[n](~p))
Theorem: LO.System.multiboxDuality'!
Proof state before:
case 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 : ℕ
h : 𝓢 ⊢! □^[n]p
⊢ 𝓢 ⊢! ~(◇^[n](~p))
Tactic:
exact (conj₁'! multiboxDuality!) ⨀ h
Proof state after:
no goals
Theorem: LO.System.multiboxDuality'!
Proof state before:
case 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 : ℕ
⊢ 𝓢 ⊢! ~(◇^[n](~p)) → 𝓢 ⊢! □^[n]p
Tactic:
intro h
Proof state after:
case 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 : ℕ
h : 𝓢 ⊢! ~(◇^[n](~p))
⊢ 𝓢 ⊢! □^[n]p
Theorem: LO.System.multiboxDuality'!
Proof state before:
case 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 : ℕ
h : 𝓢 ⊢! ~(◇^[n](~p))
⊢ 𝓢 ⊢! □^[n]p
Tactic:
exact (conj₂'! multiboxDuality!) ⨀ h
Proof state after:
no goals
Theorem: LO.System.multidiaDuality'!
Proof 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]p ↔ 𝓢 ⊢! ~(□^[n](~p))
Tactic:
constructor
Proof state after:
case 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 : ℕ
⊢ 𝓢 ⊢! ◇^[n]p → 𝓢 ⊢! ~(□^[n](~p))

case 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 : ℕ
⊢ 𝓢 ⊢! ~(□^[n](~p)) → 𝓢 ⊢! ◇^[n]p
Theorem: LO.System.multidiaDuality'!
Proof state before:
case 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 : ℕ
⊢ 𝓢 ⊢! ◇^[n]p → 𝓢 ⊢! ~(□^[n](~p))

case 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 : ℕ
⊢ 𝓢 ⊢! ~(□^[n](~p)) → 𝓢 ⊢! ◇^[n]p
Tactic:
. intro h; exact (conj₁'! multidiaDuality!) ⨀ h;
Proof state after:
case 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 : ℕ
⊢ 𝓢 ⊢! ~(□^[n](~p)) → 𝓢 ⊢! ◇^[n]p
Theorem: LO.System.multidiaDuality'!
Proof state before:
case 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 : ℕ
⊢ 𝓢 ⊢! ~(□^[n](~p)) → 𝓢 ⊢! ◇^[n]p
Tactic:
. intro h; exact (conj₂'! multidiaDuality!) ⨀ h;
Proof state after:
no goals
Theorem: LO.System.multidiaDuality'!
Proof state before:
case 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 : ℕ
⊢ 𝓢 ⊢! ◇^[n]p → 𝓢 ⊢! ~(□^[n](~p))
Tactic:
intro h
Proof state after:
case 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 : ℕ
h : 𝓢 ⊢! ◇^[n]p
⊢ 𝓢 ⊢! ~(□^[n](~p))
Theorem: LO.System.multidiaDuality'!
Proof state before:
case 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 : ℕ
h : 𝓢 ⊢! ◇^[n]p
⊢ 𝓢 ⊢! ~(□^[n](~p))
Tactic:
exact (conj₁'! multidiaDuality!) ⨀ h
Proof state after:
no goals
Theorem: LO.System.multidiaDuality'!
Proof state before:
case 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 : ℕ
⊢ 𝓢 ⊢! ~(□^[n](~p)) → 𝓢 ⊢! ◇^[n]p
Tactic:
intro h
Proof state after:
case 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 : ℕ
h : 𝓢 ⊢! ~(□^[n](~p))
⊢ 𝓢 ⊢! ◇^[n]p
Theorem: LO.System.multidiaDuality'!
Proof state before:
case 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 : ℕ
h : 𝓢 ⊢! ~(□^[n](~p))
⊢ 𝓢 ⊢! ◇^[n]p
Tactic:
exact (conj₂'! multidiaDuality!) ⨀ h
Proof state after:
no goals
Theorem: LO.System.multiboxConj'_iff!
Proof 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₂);
Proof state after:
no goals
Theorem: LO.System.multiboxConj'_iff!
Proof 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
Proof state after:
no goals
Theorem: LO.System.multiboxConj'_iff!
Proof 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
Proof state after:
no goals
Theorem: LO.System.multiboxConj'_iff!
Proof 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
Proof 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
Theorem: LO.System.multiboxConj'_iff!
Proof 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
Proof 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')
Theorem: LO.System.multiboxConj'_iff!
Proof 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);
Proof 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')
Theorem: LO.System.multiboxConj'_iff!
Proof 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₂);
Proof state after:
no goals
Theorem: LO.System.multiboxConj'_iff!
Proof 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
Proof 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
Theorem: LO.System.multiboxConj'_iff!
Proof 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
Proof 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
Theorem: LO.System.multiboxConj'_iff!
Proof 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
Proof 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
Theorem: LO.System.multiboxConj'_iff!
Proof 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;
Proof 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
Theorem: LO.System.multiboxConj'_iff!
Proof 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);
Proof state after:
no goals
Theorem: LO.System.multiboxConj'_iff!
Proof 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
Proof state after:
no goals
Theorem: LO.System.multiboxConj'_iff!
Proof 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)
Proof state after:
no goals
Theorem: LO.System.multiboxConj'_iff!
Proof 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₂⟩
Proof 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')
Theorem: LO.System.multiboxConj'_iff!
Proof 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₂)
Proof state after:
no goals
Theorem: LO.System.multiboxconj'_of_conj'multibox!
Proof 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
Proof 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