Proof of proveit.logic.sets.intersection_subset_eq_union theorem

import proveit
from proveit import defaults
from proveit import m, x, A, B
from proveit.numbers import two
from proveit.logic import Union, Intersect
from proveit.logic.sets.inclusion  import subset_eq_def
from proveit.logic.sets.unification  import union_def
from proveit.logic.sets.intersection  import intersection_def
theory = proveit.Theory() # the theorem's theory

%proving intersection_subset_eq_union

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

subset_eq_def

 ⊢  

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

subset_eq_def_inst:  ⊢  

defaults.assumptions = [subset_eq_def_inst.rhs.condition]

defaults.assumptions:

intersection_def_inst = intersection_def.instantiate({m:two, x:x, A:[A, B]}, auto_simplify=False)

intersection_def_inst:  ⊢  

intersection_def_inst.derive_right_via_equality()

 ⊢  

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

union_def_inst:  ⊢  

union_def_inst.rhs.prove()

 ⊢  

union_def_inst.derive_left_via_equality()

 ⊢  

subset_eq_def_inst.rhs.prove()

 ⊢  

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

subset_eq_def_inst.derive_left_via_equality()

 ⊢  

%qed

proveit.logic.sets.intersection_subset_eq_union 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	⊢
	: , :
8	instantiation	11, 13, 14	⊢
	: , : , :
9	theorem		⊢
	proveit.logic.booleans.disjunction.or_if_both
10	instantiation	12, 13, 14, 15	⊢
	: , : , :
11	axiom		⊢
	proveit.logic.sets.unification.union_def
12	conjecture		⊢
	proveit.logic.sets.intersection.membership_unfolding
13	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
14	instantiation	16	⊢
	: , :
15	assumption		⊢
16	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq