Proof of proveit.logic.sets.union_with_superset_is_superset theorem

import proveit
from proveit import defaults
from proveit import m, x, y, A, B, S
from proveit.numbers import two
from proveit.logic import SetEquiv, Union
from proveit.logic.sets.equivalence  import set_equiv_def
from proveit.logic.sets.inclusion  import subset_eq_def
from proveit.logic.sets.unification  import union_def

theory = proveit.Theory() # the theorem's theory

%proving union_with_superset_is_superset

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
union_with_superset_is_superset:
(see dependencies)

defaults.assumptions = union_with_superset_is_superset.all_conditions()

defaults.assumptions:

set_equiv_def

 ⊢  

set_equiv_def_spec = set_equiv_def.instantiate({A:Union(A, S), B:S})

set_equiv_def_spec:  ⊢  

set_equiv_def_spec_r_h_s = set_equiv_def_spec.rhs

set_equiv_def_spec_r_h_s:

First, let's focus on the easiest: $S \subseteq (A\cup S)$

subset_eq_def

 ⊢  

subset_eq_def_inst_S_subset_eq_AUS = subset_eq_def.instantiate({A:S, B:Union(A, S)})

subset_eq_def_inst_S_subset_eq_AUS:  ⊢  

subset_eq_def_inst_S_subset_eq_AUS.rhs

union_def

 ⊢  

union_def_inst_AUS = union_def.instantiate({m:two, x:y, A:[A,S]})

union_def_inst_AUS:  ⊢  

union_def_inst_AUS.sub_right_side_into(subset_eq_def_inst_S_subset_eq_AUS)

 ⊢  

subset_eq_def

 ⊢  

subset_eq_def_inst_01 = subset_eq_def.instantiate({A:A, B:S})

subset_eq_def_inst_01:  ⊢  

subset_eq_def_inst_01_kt = subset_eq_def_inst_01.rhs.prove()

subset_eq_def_inst_01_kt:  ⊢  

subset_eq_def_inst_02 = subset_eq_def.instantiate({A:Union(A, S), B:S})

subset_eq_def_inst_02:  ⊢  

subset_eq_def_inst_03 = subset_eq_def.instantiate({A:S, B:Union(A, S)})

subset_eq_def_inst_03:  ⊢  

union_def

 ⊢  

# union_def_spec = union_def.instantiate({m:two, x:x, AA:[A, S]})
union_def_spec = union_def.instantiate({m:two, x:x, A:[A, S]})

union_def_spec:  ⊢  

# %qed