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

State before:
α : Type u_1
Ax : AxiomSet α
x : Axioms.Geach.Taple
l : List Axioms.Geach.Taple
h : x ∈ l
⊢ 𝗴𝗲(x) ⊆ 𝗚𝗲(l)
Tactic:
induction l with
| nil => contradiction;
| cons a as ih =>
  simp_all;
  cases h;
  . subst_vars; tauto;
  . apply Set.subset_union_of_subset_right $ ih (by assumption);
State after:
no goals

State before:
case nil
α : Type u_1
Ax : AxiomSet α
x : Axioms.Geach.Taple
h : x ∈ []
⊢ 𝗴𝗲(x) ⊆ 𝗚𝗲([])
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h : x ∈ a :: as
⊢ 𝗴𝗲(x) ⊆ 𝗚𝗲(a :: as)
Tactic:
simp_all
State after:
case cons
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h : x = a ∨ x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)

State before:
case cons
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h : x = a ∨ x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
cases h
State after:
case cons.inl
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x = a
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)

case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)

State before:
case cons.inl
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x = a
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)

case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
. subst_vars; tauto;
State after:
case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)

State before:
case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
. apply Set.subset_union_of_subset_right $ ih (by assumption);
State after:
no goals

State before:
case cons.inl
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x = a
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
subst_vars
State after:
case cons.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : a ∈ as → 𝗴𝗲(a) ⊆ 𝗚𝗲(as)
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)

State before:
case cons.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : a ∈ as → 𝗴𝗲(a) ⊆ 𝗚𝗲(as)
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
tauto
State after:
no goals

State before:
case cons.inr
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ 𝗴𝗲(x) ⊆ 𝗴𝗲(a) ∪ 𝗚𝗲(as)
Tactic:
apply Set.subset_union_of_subset_right $ ih (by assumption)
State after:
no goals

State before:
α : Type u_1
Ax : AxiomSet α
x a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
ih : x ∈ as → 𝗴𝗲(x) ⊆ 𝗚𝗲(as)
h✝ : x ∈ as
⊢ x ∈ as
Tactic:
assumption
State after:
no goals