Theorem: LO.System.conj'conj'_subset (Logic/Logic/HilbertStyle/Supplemental.lean)

State before:
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : ∀ p ∈ Γ, p ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ Γ.conj'
Tactic:
induction Γ using List.induction_with_singleton with
| hnil => simpa using dhyp! verum!;
| hsingle => simp_all; exact generalConj'! h;
| hcons p Γ hne ih => simp_all; exact implyRightAnd! (generalConj'! h.1) ih;
State after:
no goals

State before:
case hnil
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
h : ∀ p ∈ [], p ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ [].conj'
Tactic:
simpa using dhyp! verum!
State after:
no goals

State before:
case hsingle
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
a✝ : F
h : ∀ p ∈ [a✝], p ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ [a✝].conj'
Tactic:
simp_all
State after:
case hsingle
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
a✝ : F
h : a✝ ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ a✝

State before:
case hsingle
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p q r : F
Γ Δ : List F
inst✝ : System.NegationEquiv 𝓢
a✝ : F
h : a✝ ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ a✝
Tactic:
exact generalConj'! h
State after:
no goals

State before:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hne : Γ ≠ []
ih : (∀ p ∈ Γ, p ∈ Δ) → 𝓢 ⊢! Δ.conj' ⟶ Γ.conj'
h : ∀ p_1 ∈ p :: Γ, p_1 ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ (p :: Γ).conj'
Tactic:
simp_all
State after:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hne : ¬Γ = []
ih : 𝓢 ⊢! Δ.conj' ⟶ Γ.conj'
h : p ∈ Δ ∧ ∀ a ∈ Γ, a ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ p ⋏ Γ.conj'

State before:
case hcons
F : Type u_1
inst✝⁴ : LogicalConnective F
inst✝³ : DecidableEq F
S : Type u_2
inst✝² : System F S
𝓢 : S
inst✝¹ : Minimal 𝓢
p✝ q r : F
Γ✝ Δ : List F
inst✝ : System.NegationEquiv 𝓢
p : F
Γ : List F
hne : ¬Γ = []
ih : 𝓢 ⊢! Δ.conj' ⟶ Γ.conj'
h : p ∈ Δ ∧ ∀ a ∈ Γ, a ∈ Δ
⊢ 𝓢 ⊢! Δ.conj' ⟶ p ⋏ Γ.conj'
Tactic:
exact implyRightAnd! (generalConj'! h.1) ih
State after:
no goals