Proof of proveit.logic.sets.intersection_is_subset_eq 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, Intersect
from proveit.logic.sets.inclusion  import subset_eq_def
from proveit.logic.sets.intersection  import intersection_def

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

%proving intersection_is_subset_eq

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

defaults.assumptions = [intersection_is_subset_eq.condition]

defaults.assumptions:

intersection_is_subset_eq.condition.instantiate()

 ⊢  

subset_eq_def

 ⊢  

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

subset_eq_def_inst:  ⊢  

defaults.assumptions = [*defaults.assumptions, subset_eq_def_inst.rhs.condition]

defaults.assumptions:

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

intersection_def_inst:  ⊢  

intersection_def_inst.derive_right_via_equality()

 ⊢  

subset_eq_def_inst.rhs.prove()

 ⊢  

intersection_is_subset_eq 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_is_subset_eq has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3, 4	⊢
	: , :
2	theorem		⊢
	proveit.logic.equality.lhs_via_equality
3	generalization	5	⊢
4	instantiation	6	⊢
	: , :
5	instantiation	7, 8	⊢
	: , :
6	axiom		⊢
	proveit.logic.sets.inclusion.subset_eq_def
7	theorem		⊢
	proveit.logic.booleans.conjunction.left_from_and
8	instantiation	9, 10, 11, 12	⊢
	: , : , :
9	conjecture		⊢
	proveit.logic.sets.intersection.membership_unfolding
10	conjecture		⊢
	proveit.numbers.numerals.decimals.posnat2
11	instantiation	13	⊢
	: , :
12	assumption		⊢
13	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq