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

State before:
α : Type u_1
Ax : AxiomSet α
l₁ l₂ : List Axioms.Geach.Taple
h : l₁ ⊆ l₂
⊢ 𝗚𝗲(l₁) ⊆ 𝗚𝗲(l₂)
Tactic:
induction l₁ generalizing l₂ <;> induction l₂
State after:
case nil.nil
α : Type u_1
Ax : AxiomSet α
h : [] ⊆ []
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲([])

case nil.cons
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : [] ⊆ tail✝ → 𝗚𝗲([]) ⊆ 𝗚𝗲(tail✝)
h : [] ⊆ head✝ :: tail✝
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲(head✝ :: tail✝)

case cons.nil
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝ ⊆ l₂ → 𝗚𝗲(tail✝) ⊆ 𝗚𝗲(l₂)
h : head✝ :: tail✝ ⊆ []
⊢ 𝗚𝗲(head✝ :: tail✝) ⊆ 𝗚𝗲([])

case cons.cons
α : Type u_1
Ax : AxiomSet α
head✝¹ : Axioms.Geach.Taple
tail✝¹ : List Axioms.Geach.Taple
tail_ih✝¹ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝¹ ⊆ l₂ → 𝗚𝗲(tail✝¹) ⊆ 𝗚𝗲(l₂)
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : head✝¹ :: tail✝¹ ⊆ tail✝ → 𝗚𝗲(head✝¹ :: tail✝¹) ⊆ 𝗚𝗲(tail✝)
h : head✝¹ :: tail✝¹ ⊆ head✝ :: tail✝
⊢ 𝗚𝗲(head✝¹ :: tail✝¹) ⊆ 𝗚𝗲(head✝ :: tail✝)

State before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝ ⊆ l₂ → 𝗚𝗲(tail✝) ⊆ 𝗚𝗲(l₂)
h : head✝ :: tail✝ ⊆ []
⊢ 𝗚𝗲(head✝ :: tail✝) ⊆ 𝗚𝗲([])
Tactic:
case nil.nil | cons.nil => simp_all;
State after:
no goals

State before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : [] ⊆ tail✝ → 𝗚𝗲([]) ⊆ 𝗚𝗲(tail✝)
h : [] ⊆ head✝ :: tail✝
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲(head✝ :: tail✝)
Tactic:
case nil.cons => simp_all; apply Set.subset_union_of_subset_right (by simp);
State after:
no goals

State before:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a :: as ⊆ bs → 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(bs)
h : a :: as ⊆ b :: bs
⊢ 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(b :: bs)
Tactic:
case cons.cons a as iha b bs ihb =>
  simp_all;
  constructor;
  . cases h.1;
    . subst_vars; tauto;
    . apply Set.subset_union_of_subset_right $ mem (by assumption);
  . simpa using (iha h.2);
State after:
no goals

State before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : ∀ {l₂ : List Axioms.Geach.Taple}, tail✝ ⊆ l₂ → 𝗚𝗲(tail✝) ⊆ 𝗚𝗲(l₂)
h : head✝ :: tail✝ ⊆ []
⊢ 𝗚𝗲(head✝ :: tail✝) ⊆ 𝗚𝗲([])
Tactic:
simp_all
State after:
no goals

State before:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
tail_ih✝ : [] ⊆ tail✝ → 𝗚𝗲([]) ⊆ 𝗚𝗲(tail✝)
h : [] ⊆ head✝ :: tail✝
⊢ 𝗚𝗲([]) ⊆ 𝗚𝗲(head✝ :: tail✝)
Tactic:
simp_all
State after:
α : Type u_1
Ax : AxiomSet α
head✝ : Axioms.Geach.Taple
tail✝ : List Axioms.Geach.Taple
⊢ 𝗞 ⊆ 𝗴𝗲(head✝) ∪ 𝗚𝗲(tail✝)

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

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

State before:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a :: as ⊆ bs → 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(bs)
h : a :: as ⊆ b :: bs
⊢ 𝗚𝗲(a :: as) ⊆ 𝗚𝗲(b :: bs)
Tactic:
simp_all
State after:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs) ∧ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

State before:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs) ∧ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
constructor
State after:
case left
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

State before:
case left
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
. cases h.1;
  . subst_vars; tauto;
  . apply Set.subset_union_of_subset_right $ mem (by assumption);
State after:
case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

State before:
case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
. simpa using (iha h.2);
State after:
no goals

State before:
case left
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
cases h.1
State after:
case left.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a = b
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

State before:
case left.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a = b
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
. subst_vars; tauto;
State after:
case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

State before:
case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
. apply Set.subset_union_of_subset_right $ mem (by assumption);
State after:
no goals

State before:
case left.inl
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a = b
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
subst_vars
State after:
case left.inl
α : Type u_1
Ax : AxiomSet α
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : b ∈ bs → as ⊆ bs → 𝗴𝗲(b) ⊆ 𝗚𝗲(bs)
h : (b = b ∨ b ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(b) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)

State before:
case left.inl
α : Type u_1
Ax : AxiomSet α
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : b ∈ bs → as ⊆ bs → 𝗴𝗲(b) ⊆ 𝗚𝗲(bs)
h : (b = b ∨ b ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗴𝗲(b) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
tauto
State after:
no goals

State before:
case left.inr
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ 𝗴𝗲(a) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
apply Set.subset_union_of_subset_right $ mem (by assumption)
State after:
no goals

State before:
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
h✝ : a ∈ bs
⊢ a ∈ bs
Tactic:
assumption
State after:
no goals

State before:
case right
α : Type u_1
Ax : AxiomSet α
a : Axioms.Geach.Taple
as : List Axioms.Geach.Taple
iha : ∀ {l₂ : List Axioms.Geach.Taple}, as ⊆ l₂ → 𝗚𝗲(as) ⊆ 𝗚𝗲(l₂)
b : Axioms.Geach.Taple
bs : List Axioms.Geach.Taple
ihb : a ∈ bs → as ⊆ bs → 𝗴𝗲(a) ⊆ 𝗚𝗲(bs)
h : (a = b ∨ a ∈ bs) ∧ as ⊆ b :: bs
⊢ 𝗚𝗲(as) ⊆ 𝗴𝗲(b) ∪ 𝗚𝗲(bs)
Tactic:
simpa using (iha h.2)
State after:
no goals