Theorem: LO.System.iff_conj'multidia_multidiaconj'! (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! verum!;
| hsingle p => simp;
| hcons p Γ h ih =>
  simp_all;
  exact imp_trans! distribute_multidia_and! $ by
    apply deduct'!;
    apply iff_provable_list_conj.mpr;
    intro q hq;
    simp at hq;
    cases hq with
    | inl => subst_vars; exact conj₁'! id!;
    | inr hq =>
      obtain ⟨r, hr₁, hr₂⟩ := hq;
      exact (iff_provable_list_conj.mp $ (of'! ih) ⨀ (conj₂'! $ id!)) q (by aesop);
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! verum!
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 : ℕ
p : F
⊢ 𝓢 ⊢! ◇^[n][p].conj' ⟶ (◇'^[n][p]).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! distribute_multidia_and! $ by
  apply deduct'!;
  apply iff_provable_list_conj.mpr;
  intro q hq;
  simp at hq;
  cases hq with
  | inl => subst_vars; exact conj₁'! id!;
  | inr hq =>
    obtain ⟨r, hr₁, hr₂⟩ := hq;
    exact (iff_provable_list_conj.mp $ (of'! ih) ⨀ (conj₂'! $ id!)) q (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 : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
⊢ 𝓢 ⊢! ◇^[n]p ⋏ ◇^[n]Γ.conj' ⟶ (◇'^[n](p :: Γ)).conj'
Tactic:
apply deduct'!
State after:
case h
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]Γ.conj'] ⊢[𝓢]! (◇'^[n](p :: Γ)).conj'

State before:
case h
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]Γ.conj'] ⊢[𝓢]! (◇'^[n](p :: Γ)).conj'
Tactic:
apply iff_provable_list_conj.mpr
State after:
case h
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'
⊢ ∀ p_1 ∈ ◇'^[n](p :: Γ), { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! p_1

State before:
case h
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'
⊢ ∀ p_1 ∈ ◇'^[n](p :: Γ), { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! p_1
Tactic:
intro q hq
State after:
case h
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'
q : F
hq : q ∈ ◇'^[n](p :: Γ)
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q

State before:
case h
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'
q : F
hq : q ∈ ◇'^[n](p :: Γ)
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
simp at hq
State after:
case h
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'
q : F
hq : q = (UnaryModalOperator.mop false)^[n] p ∨ ∃ a ∈ Γ, (UnaryModalOperator.mop false)^[n] a = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q

State before:
case h
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'
q : F
hq : q = (UnaryModalOperator.mop false)^[n] p ∨ ∃ a ∈ Γ, (UnaryModalOperator.mop false)^[n] a = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
cases hq with
| inl => subst_vars; exact conj₁'! id!;
| inr hq =>
  obtain ⟨r, hr₁, hr₂⟩ := hq;
  exact (iff_provable_list_conj.mp $ (of'! ih) ⨀ (conj₂'! $ id!)) q (by aesop);
State after:
no goals

State before:
case h.inl
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'
q : F
h✝ : q = (UnaryModalOperator.mop false)^[n] p
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
subst_vars
State after:
case h.inl
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'
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! (UnaryModalOperator.mop false)^[n] p

State before:
case h.inl
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'
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! (UnaryModalOperator.mop false)^[n] p
Tactic:
exact conj₁'! id!
State after:
no goals

State before:
case h.inr
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'
q : F
hq : ∃ a ∈ Γ, (UnaryModalOperator.mop false)^[n] a = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
obtain ⟨r, hr₁, hr₂⟩ := hq
State after:
case h.inr.intro.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' ⟶ (◇'^[n]Γ).conj'
q r : F
hr₁ : r ∈ Γ
hr₂ : (UnaryModalOperator.mop false)^[n] r = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q

State before:
case h.inr.intro.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' ⟶ (◇'^[n]Γ).conj'
q r : F
hr₁ : r ∈ Γ
hr₂ : (UnaryModalOperator.mop false)^[n] r = q
⊢ { ctx := [◇^[n]p ⋏ ◇^[n]Γ.conj'] } ⊢! q
Tactic:
exact (iff_provable_list_conj.mp $ (of'! ih) ⨀ (conj₂'! $ id!)) q (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 : ℕ
p : F
Γ : List F
h : ¬Γ = []
ih : 𝓢 ⊢! ◇^[n]Γ.conj' ⟶ (◇'^[n]Γ).conj'
q r : F
hr₁ : r ∈ Γ
hr₂ : (UnaryModalOperator.mop false)^[n] r = q
⊢ q ∈ ◇'^[n]Γ
Tactic:
aesop
State after:
no goals