Theorem: LO.Modal.Standard.AxiomSet.MultiGeach.subsetK (Logic/Modal/Standard/Geach.lean)

State before:
α : Type u_1
Ax : AxiomSet α
l : List Axioms.Geach.Taple
⊢ 𝗞 ⊆ 𝗚𝗲(l)
Tactic:
induction l with
| nil => simp;
| cons => simp; apply Set.subset_union_of_subset_right (by assumption);
State after:
no goals

State before:
case nil
α : Type u_1
Ax : AxiomSet α
⊢ 𝗞 ⊆ 𝗚𝗲([])
Tactic:
simp
State after:
no goals

State before:
case cons
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : 𝗞 ⊆ 𝗚𝗲(tail✝)
⊢ 𝗞 ⊆ 𝗚𝗲(head✝ :: tail✝)
Tactic:
simp
State after:
case cons
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : 𝗞 ⊆ 𝗚𝗲(tail✝)
⊢ 𝗞 ⊆ 𝗴𝗲(head✝) ∪ 𝗚𝗲(tail✝)

State before:
case cons
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : 𝗞 ⊆ 𝗚𝗲(tail✝)
⊢ 𝗞 ⊆ 𝗴𝗲(head✝) ∪ 𝗚𝗲(tail✝)
Tactic:
apply Set.subset_union_of_subset_right (by assumption)
State after:
no goals

State before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : 𝗞 ⊆ 𝗚𝗲(tail✝)
⊢ 𝗞 ⊆ 𝗚𝗲(tail✝)
Tactic:
assumption
State after:
no goals