Proof of proveit.core_expr_types.tuples.singular_range_reduction theorem¶
In [1]:
import proveit
from proveit import defaults
theory = proveit.Theory() # the theorem's theory
In [2]:
%proving singular_range_reduction
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
singular_range_reduction:
(see dependencies)
singular_range_reduction:
(see dependencies)
In [3]:
defaults.assumptions = singular_range_reduction.conditions
defaults.assumptions: 
In [4]:
i_eq_j = defaults.assumptions[0]
i_eq_j: 
In [5]:
i_eq_j.derive_reversed().substitution(singular_range_reduction.instance_expr.lhs)
