Proof of proveit.logic.sets.set_subset_eq_of_union_with_set theorem

import proveit
from proveit import defaults
from proveit import m, x, y, A, B, S
from proveit.numbers import one, two
from proveit.logic import InSet, Union
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 set_subset_eq_of_union_with_set

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

defaults.assumptions = [set_subset_eq_of_union_with_set.condition]

defaults.assumptions:

set_subset_eq_of_union_with_set.condition.instantiate()

 ⊢  

subset_eq_def

 ⊢  

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

subset_eq_def_inst:  ⊢  

union_def_inst = union_def.instantiate({m:two, x:x, A:[A, B]})

union_def_inst:  ⊢  

defaults.assumptions = [*defaults.assumptions, InSet(x, A)]

defaults.assumptions:

union_def_inst.rhs.prove()

,  ⊢  

union_def_inst.derive_left_via_equality()

,  ⊢  

subset_eq_def_inst.derive_left_via_equality(assumptions=[set_subset_eq_of_union_with_set.condition])

 ⊢  

set_subset_eq_of_union_with_set may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.logic.sets.set_subset_eq_of_union_with_set has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	6, 2, 3	⊢
	: , :
2	generalization	4	⊢
3	instantiation	5	⊢
	: , :
4	instantiation	6, 7, 8	,  ⊢
	: , :
5	axiom		⊢
	proveit.logic.sets.inclusion.subset_eq_def
6	theorem		⊢
	proveit.logic.equality.lhs_via_equality
7	instantiation	9, 10, 11, 16	,  ⊢
	: , :
8	instantiation	12, 13, 14	⊢
	: , : , :
9	conjecture		⊢
	proveit.logic.booleans.disjunction.or_if_left
10	instantiation	15, 16	⊢
	:
11	instantiation	17	⊢
	:
12	axiom		⊢
	proveit.logic.sets.unification.union_def
13	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
14	instantiation	18	⊢
	: , :
15	conjecture		⊢
	proveit.logic.booleans.in_bool_if_true
16	assumption		⊢
17	assumption		⊢
18	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq