failed instance search for Line 211 in analysis/normed_space/operator_norm.lean with `by apply_instance`

instance_search.lean

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : has_bind tactic := filter.ultrafilter.has_bind
[type_context.is_def_eq_detail] [1]: has_bind tactic =?= has_bind filter.ultrafilter
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] [2]: tactic =?= filter.ultrafilter
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= filter.ultrafilter
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= filter.ultrafilter
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= filter.ultrafilter α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= filter.ultrafilter α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= filter.ultrafilter α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= filter.ultrafilter
[type_context.is_def_eq_detail] on failure: has_bind tactic =?= has_bind filter.ultrafilter
[type_context.is_def_eq] has_bind tactic =?= has_bind filter.ultrafilter ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_0 : has_bind tactic := filter.has_bind
[type_context.is_def_eq_detail] [1]: has_bind tactic =?= has_bind filter
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] [2]: tactic =?= filter
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= filter
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= filter
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= filter α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= filter α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= filter α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= filter
[type_context.is_def_eq_detail] on failure: has_bind tactic =?= has_bind filter
[type_context.is_def_eq] has_bind tactic =?= has_bind filter ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_0 : has_bind tactic := @monad.to_has_bind ?x_1 ?x_2
[type_context.is_def_eq_detail] [1]: has_bind tactic =?= has_bind ?x_1
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] process_assignment ?x_1 := tactic
[type_context.is_def_eq_detail] assign: ?x_1 := tactic
[type_context.is_def_eq] has_bind tactic =?= has_bind ?x_1 ... success  (approximate mode)
[class_instances] (1) ?x_2 : monad tactic := free_abelian_group.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad free_abelian_group
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= free_abelian_group
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= free_abelian_group
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= free_abelian_group
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= free_abelian_group α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= free_abelian_group α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= free_abelian_group α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= free_abelian_group
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad free_abelian_group
[type_context.is_def_eq] monad ?x_1 =?= monad free_abelian_group ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := free_group.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad free_group
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= free_group
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= free_group
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= free_group
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= free_group α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= free_group α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= free_group α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= free_group
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad free_group
[type_context.is_def_eq] monad ?x_1 =?= monad free_group ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := filter.ultrafilter.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad filter.ultrafilter
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= filter.ultrafilter
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= filter.ultrafilter
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= filter.ultrafilter
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= filter.ultrafilter α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= filter.ultrafilter α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= filter.ultrafilter α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= filter.ultrafilter
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad filter.ultrafilter
[type_context.is_def_eq] monad ?x_1 =?= monad filter.ultrafilter ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := linarith.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad linarith.linarith_monad
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= linarith.linarith_monad
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= state_t linarith.linarith_structure (except_t linarith.pcomp (@id Type))
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= state_t linarith.linarith_structure (except_t linarith.pcomp (@id Type))
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= state_t linarith.linarith_structure (except_t linarith.pcomp (@id Type)) α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= state_t linarith.linarith_structure (except_t linarith.pcomp (@id Type)) α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= state_t linarith.linarith_structure (except_t linarith.pcomp (@id Type)) α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= state_t linarith.linarith_structure (except_t linarith.pcomp (@id Type))
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad linarith.linarith_monad
[type_context.is_def_eq] monad ?x_1 =?= monad linarith.linarith_monad ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := tactic.ring.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad tactic.ring.ring_m
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= tactic.ring.ring_m
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= tactic.ring.ring_m
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= tactic.ring.ring_m
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= tactic.ring.ring_m α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= tactic.ring.ring_m α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= tactic.ring.ring_m α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= tactic.ring.ring_m
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad tactic.ring.ring_m
[type_context.is_def_eq] monad ?x_1 =?= monad tactic.ring.ring_m ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @pfun.monad ?x_3
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad (pfun ?x_3)
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= pfun ?x_3
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= pfun ?x_3
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= pfun ?x_3
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= ?x_3 →. α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= ?x_3 →. α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= ?x_3 →. α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= pfun ?x_3
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad (pfun ?x_3)
[type_context.is_def_eq] monad ?x_1 =?= monad (pfun ?x_3) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := roption.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad roption
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= roption
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= roption
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= roption
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= roption α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= roption α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= roption α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= roption
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad roption
[type_context.is_def_eq] monad ?x_1 =?= monad roption ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := multiset.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad multiset
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= multiset
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= multiset
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= multiset
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= multiset α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= multiset α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= multiset α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= multiset
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad multiset
[type_context.is_def_eq] monad ?x_1 =?= monad multiset ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := set.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad set
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= set
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= set
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= set
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= set α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= set α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= set α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= set
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad set
[type_context.is_def_eq] monad ?x_1 =?= monad set ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := trunc.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad trunc
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= trunc
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= trunc
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= trunc
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= trunc α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= trunc α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= trunc α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= trunc
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad trunc
[type_context.is_def_eq] monad ?x_1 =?= monad trunc ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := with_zero.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad with_zero
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= with_zero
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= with_zero
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= with_zero
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= with_zero α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= with_zero α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= with_zero α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= with_zero
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad with_zero
[type_context.is_def_eq] monad ?x_1 =?= monad with_zero ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := with_one.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad with_one
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= with_one
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= with_one
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= with_one
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= with_one α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= with_one α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= with_one α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= with_one
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad with_one
[type_context.is_def_eq] monad ?x_1 =?= monad with_one ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := old_conv.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad old_conv
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= old_conv
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= old_conv
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= old_conv
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= old_conv α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= old_conv α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= old_conv α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= old_conv
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad old_conv
[type_context.is_def_eq] monad ?x_1 =?= monad old_conv ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @sum.monad ?x_4
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad (sum ?x_4)
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= sum ?x_4
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= sum ?x_4
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= sum ?x_4
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= ?x_4 ⊕ α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= ?x_4 ⊕ α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= ?x_4 ⊕ α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= sum ?x_4
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad (sum ?x_4)
[type_context.is_def_eq] monad ?x_1 =?= monad (sum ?x_4) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := parser.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad parser
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= parser
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= parser
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= parser
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= parser α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= parser α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= parser α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= parser
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad parser
[type_context.is_def_eq] monad ?x_1 =?= monad parser ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := list.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad list
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= list
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= list
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= list
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= list α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= list α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= list α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= list
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad list
[type_context.is_def_eq] monad ?x_1 =?= monad list ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := smt_tactic.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad smt_tactic
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= smt_tactic
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= smt_tactic
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= smt_tactic
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= smt_tactic α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= smt_tactic α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= smt_tactic α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= smt_tactic
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad smt_tactic
[type_context.is_def_eq] monad ?x_1 =?= monad smt_tactic ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := vm_core.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad vm_core
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= vm_core
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= vm_core
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= vm_core
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= vm_core α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= vm_core α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= vm_core α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= vm_core
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad vm_core
[type_context.is_def_eq] monad ?x_1 =?= monad vm_core ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := conv.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad conv
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= conv
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= conv
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= conv
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= conv α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= conv α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= conv α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= conv
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad conv
[type_context.is_def_eq] monad ?x_1 =?= monad conv ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @option_t.monad ?x_5 ?x_6
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad (option_t ?x_5)
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= option_t ?x_5
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= option_t ?x_5
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= option_t ?x_5
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= option_t ?x_5 α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= option_t ?x_5 α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= option_t ?x_5 α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= option_t ?x_5
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad (option_t ?x_5)
[type_context.is_def_eq] monad ?x_1 =?= monad (option_t ?x_5) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @reader_t.monad ?x_7 ?x_8 ?x_9
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad (reader_t ?x_7 ?x_8)
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= reader_t ?x_7 ?x_8
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= reader_t ?x_7 ?x_8
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= reader_t ?x_7 ?x_8
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= reader_t ?x_7 ?x_8 α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= reader_t ?x_7 ?x_8 α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= reader_t ?x_7 ?x_8 α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= reader_t ?x_7 ?x_8
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad (reader_t ?x_7 ?x_8)
[type_context.is_def_eq] monad ?x_1 =?= monad (reader_t ?x_7 ?x_8) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @state_t.monad ?x_10 ?x_11 ?x_12
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad (state_t ?x_10 ?x_11)
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= state_t ?x_10 ?x_11
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= state_t ?x_10 ?x_11
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= state_t ?x_10 ?x_11
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= state_t ?x_10 ?x_11 α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= state_t ?x_10 ?x_11 α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= state_t ?x_10 ?x_11 α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= state_t ?x_10 ?x_11
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad (state_t ?x_10 ?x_11)
[type_context.is_def_eq] monad ?x_1 =?= monad (state_t ?x_10 ?x_11) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @except_t.monad ?x_13 ?x_14 ?x_15
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad (except_t ?x_13 ?x_14)
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= except_t ?x_13 ?x_14
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= except_t ?x_13 ?x_14
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= except_t ?x_13 ?x_14
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= except_t ?x_13 ?x_14 α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= except_t ?x_13 ?x_14 α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= except_t ?x_13 ?x_14 α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= except_t ?x_13 ?x_14
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad (except_t ?x_13 ?x_14)
[type_context.is_def_eq] monad ?x_1 =?= monad (except_t ?x_13 ?x_14) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @except.monad ?x_16
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad (except ?x_16)
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= except ?x_16
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= except ?x_16
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= except ?x_16
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= except ?x_16 α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= except ?x_16 α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= except ?x_16 α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= except ?x_16
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad (except ?x_16)
[type_context.is_def_eq] monad ?x_1 =?= monad (except ?x_16) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := id.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad (@id (Type ?))
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= @id (Type ?)
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= @id (Type ?)
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= @id (Type ?)
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= @id (Type ?) α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= @id (Type ?) α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= @id (Type ?) α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= @id (Type ?)
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad (@id (Type ?))
[type_context.is_def_eq] monad ?x_1 =?= monad (@id (Type ?)) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := task.monad
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad task
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= task
[type_context.is_def_eq_detail] unfold left: tactic
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= task
[type_context.is_def_eq_detail] unfold left: interaction_monad
[type_context.is_def_eq_detail] [4]: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= task
[type_context.is_def_eq_detail] [5]: id_rhs Type (tactic_state → result tactic_state α) =?= task α
[type_context.is_def_eq_detail] unfold left: id_rhs
[type_context.is_def_eq_detail] [6]: tactic_state → result tactic_state α =?= task α
[type_context.is_def_eq_detail] on failure: tactic_state → result tactic_state α =?= task α
[type_context.is_def_eq_detail] on failure: λ (α : Type), id_rhs Type (tactic_state → result tactic_state α) =?= task
[type_context.is_def_eq_detail] on failure: monad ?x_1 =?= monad task
[type_context.is_def_eq] monad ?x_1 =?= monad task ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_2 : monad tactic := @interaction_monad.monad ?x_17
[type_context.is_def_eq_detail] [1]: monad ?x_1 =?= monad (interaction_monad ?x_17)
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= interaction_monad ?x_17
[type_context.is_def_eq_detail] [3]: interaction_monad tactic_state =?= interaction_monad ?x_17
[type_context.is_def_eq_detail] process_assignment ?x_17 := tactic_state
[type_context.is_def_eq_detail] assign: ?x_17 := tactic_state
[type_context.is_def_eq] monad ?x_1 =?= monad (interaction_monad ?x_17) ... success  (approximate mode)
operator_norm.lean:216:3: information trace output
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : normed_group (E →L[𝕜] F × G) := _inst_3
[type_context.is_def_eq_detail] [1]: normed_group (E →L[𝕜] F × G) =?= normed_group G
[type_context.is_def_eq_detail] [2]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= G
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= G
[type_context.is_def_eq_detail] on failure: normed_group (E →L[𝕜] F × G) =?= normed_group G
[type_context.is_def_eq] normed_group (E →L[𝕜] F × G) =?= normed_group G ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_0 : normed_group (E →L[𝕜] F × G) := _inst_2
[type_context.is_def_eq_detail] [1]: normed_group (E →L[𝕜] F × G) =?= normed_group F
[type_context.is_def_eq_detail] [2]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= F
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= F
[type_context.is_def_eq_detail] on failure: normed_group (E →L[𝕜] F × G) =?= normed_group F
[type_context.is_def_eq] normed_group (E →L[𝕜] F × G) =?= normed_group F ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_0 : normed_group (E →L[𝕜] F × G) := _inst_1
[type_context.is_def_eq_detail] [1]: normed_group (E →L[𝕜] F × G) =?= normed_group E
[type_context.is_def_eq_detail] [2]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= E
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= E
[type_context.is_def_eq_detail] on failure: normed_group (E →L[𝕜] F × G) =?= normed_group E
[type_context.is_def_eq] normed_group (E →L[𝕜] F × G) =?= normed_group E ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_0 : normed_group (E →L[𝕜] F × G) := @continuous_linear_map.to_normed_group ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6 ?x_7 ?x_8
[type_context.is_def_eq_detail] [1]: normed_group (E →L[𝕜] F × G) =?= normed_group (?x_2 →L[?x_1] ?x_3)
[type_context.is_def_eq_detail] [2]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= ?x_2 →L[?x_1] ?x_3
[type_context.is_def_eq_detail] [3]: continuous_linear_map =?= continuous_linear_map
[type_context.is_def_eq_detail] process_assignment ?x_1 := 𝕜
[type_context.is_def_eq_detail] assign: ?x_1 := 𝕜
[type_context.is_def_eq_detail] process_assignment ?x_2 := E
[type_context.is_def_eq_detail] assign: ?x_2 := E
[type_context.is_def_eq_detail] process_assignment ?x_3 := F × G
[type_context.is_def_eq_detail] assign: ?x_3 := F × G
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_9 : nondiscrete_normed_field 𝕜 := _inst_4
[type_context.is_def_eq] nondiscrete_normed_field 𝕜 =?= nondiscrete_normed_field 𝕜 ... success  (approximate mode)
[type_context.is_def_eq_detail] [3]: @normed_ring.to_ring 𝕜 (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @normed_ring.to_ring ?x_1 (@normed_field.to_normed_ring ?x_1 (@nondiscrete_normed_field.to_normed_field ?x_1 _inst_4))
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_10 : normed_group E := _inst_3
[type_context.is_def_eq_detail] [3]: normed_group E =?= normed_group G
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] on failure: normed_group E =?= normed_group G
[type_context.is_def_eq] normed_group E =?= normed_group G ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_10 : normed_group E := _inst_2
[type_context.is_def_eq_detail] [3]: normed_group E =?= normed_group F
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] on failure: normed_group E =?= normed_group F
[type_context.is_def_eq] normed_group E =?= normed_group F ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_10 : normed_group E := _inst_1
[type_context.is_def_eq] normed_group E =?= normed_group E ... success  (approximate mode)
[type_context.is_def_eq_detail] [3]: @uniform_space.to_topological_space E (@metric_space.to_uniform_space' E (@normed_group.to_metric_space E _inst_1)) =?= @uniform_space.to_topological_space ?x_2
  (@metric_space.to_uniform_space' ?x_2 (@normed_group.to_metric_space ?x_2 _inst_1))
[type_context.is_def_eq_detail] [4]: uniform_space.to_topological_space =?= uniform_space.to_topological_space
[type_context.is_def_eq_detail] [4]: @metric_space.to_uniform_space' E (@normed_group.to_metric_space E _inst_1) =?= @metric_space.to_uniform_space' ?x_2 (@normed_group.to_metric_space ?x_2 _inst_1)
[type_context.is_def_eq_detail] [5]: @normed_group.to_metric_space E _inst_1 =?= @normed_group.to_metric_space ?x_2 _inst_1
[type_context.is_def_eq_detail] [6]: normed_group.to_metric_space =?= normed_group.to_metric_space
[type_context.is_def_eq_detail] [3]: @normed_group.to_add_comm_group E _inst_1 =?= @normed_group.to_add_comm_group ?x_2 ?x_4
[type_context.is_def_eq_detail] [4]: normed_group.to_add_comm_group =?= normed_group.to_add_comm_group
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_11 : normed_group (F × G) := _inst_3
[type_context.is_def_eq_detail] [3]: normed_group (F × G) =?= normed_group G
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [4]: F × G =?= G
[type_context.is_def_eq_detail] on failure: F × G =?= G
[type_context.is_def_eq_detail] on failure: normed_group (F × G) =?= normed_group G
[type_context.is_def_eq] normed_group (F × G) =?= normed_group G ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_11 : normed_group (F × G) := _inst_2
[type_context.is_def_eq_detail] [3]: normed_group (F × G) =?= normed_group F
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [4]: F × G =?= F
[type_context.is_def_eq_detail] on failure: F × G =?= F
[type_context.is_def_eq_detail] on failure: normed_group (F × G) =?= normed_group F
[type_context.is_def_eq] normed_group (F × G) =?= normed_group F ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_11 : normed_group (F × G) := _inst_1
[type_context.is_def_eq_detail] [3]: normed_group (F × G) =?= normed_group E
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [4]: F × G =?= E
[type_context.is_def_eq_detail] on failure: F × G =?= E
[type_context.is_def_eq_detail] on failure: normed_group (F × G) =?= normed_group E
[type_context.is_def_eq] normed_group (F × G) =?= normed_group E ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_11 : normed_group (F × G) := @continuous_linear_map.to_normed_group ?x_12 ?x_13 ?x_14 ?x_15 ?x_16 ?x_17 ?x_18 ?x_19
[type_context.is_def_eq_detail] [3]: normed_group (F × G) =?= normed_group (?x_13 →L[?x_12] ?x_14)
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [4]: F × G =?= ?x_13 →L[?x_12] ?x_14
[type_context.is_def_eq_detail] [5]: prod =?= continuous_linear_map
[type_context.is_def_eq_detail] on failure: prod =?= continuous_linear_map
[type_context.is_def_eq_detail] on failure: F × G =?= ?x_13 →L[?x_12] ?x_14
[type_context.is_def_eq_detail] on failure: normed_group (F × G) =?= normed_group (?x_13 →L[?x_12] ?x_14)
[type_context.is_def_eq] normed_group (F × G) =?= normed_group (?x_13 →L[?x_12] ?x_14) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_11 : normed_group (F × G) := @normed_ring.to_normed_group ?x_20 ?x_21
[type_context.is_def_eq_detail] [3]: normed_group (F × G) =?= normed_group ?x_20
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] process_assignment ?x_20 := F × G
[type_context.is_def_eq_detail] assign: ?x_20 := F × G
[type_context.is_def_eq] normed_group (F × G) =?= normed_group ?x_20 ... success  (approximate mode)
[class_instances] (1) ?x_21 : normed_ring (F × G) := @normed_field.to_normed_ring ?x_22 ?x_23
[type_context.is_def_eq_detail] [3]: normed_ring ?x_20 =?= normed_ring ?x_22
[type_context.is_def_eq_detail] [4]: normed_ring =?= normed_ring
[type_context.is_def_eq_detail] process_assignment ?x_22 := F × G
[type_context.is_def_eq_detail] assign: ?x_22 := F × G
[type_context.is_def_eq] normed_ring ?x_20 =?= normed_ring ?x_22 ... success  (approximate mode)
[class_instances] (2) ?x_23 : normed_field (F × G) := complex.normed_field
[type_context.is_def_eq_detail] [3]: normed_field ?x_22 =?= normed_field ℂ
[type_context.is_def_eq_detail] [4]: normed_field =?= normed_field
[type_context.is_def_eq_detail] [4]: F × G =?= ℂ
[type_context.is_def_eq_detail] on failure: F × G =?= ℂ
[type_context.is_def_eq_detail] on failure: normed_field ?x_22 =?= normed_field ℂ
[type_context.is_def_eq] normed_field ?x_22 =?= normed_field ℂ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (2) ?x_23 : normed_field (F × G) := real.normed_field
[type_context.is_def_eq_detail] [3]: normed_field ?x_22 =?= normed_field ℝ
[type_context.is_def_eq_detail] [4]: normed_field =?= normed_field
[type_context.is_def_eq_detail] [4]: F × G =?= ℝ
[type_context.is_def_eq_detail] on failure: F × G =?= ℝ
[type_context.is_def_eq_detail] on failure: normed_field ?x_22 =?= normed_field ℝ
[type_context.is_def_eq] normed_field ?x_22 =?= normed_field ℝ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (2) ?x_23 : normed_field (F × G) := @nondiscrete_normed_field.to_normed_field ?x_24 ?x_25
[type_context.is_def_eq_detail] [3]: normed_field ?x_22 =?= normed_field ?x_24
[type_context.is_def_eq_detail] [4]: normed_field =?= normed_field
[type_context.is_def_eq_detail] process_assignment ?x_24 := F × G
[type_context.is_def_eq_detail] assign: ?x_24 := F × G
[type_context.is_def_eq] normed_field ?x_22 =?= normed_field ?x_24 ... success  (approximate mode)
[class_instances] (3) ?x_25 : nondiscrete_normed_field (F × G) := _inst_4
[type_context.is_def_eq_detail] [3]: nondiscrete_normed_field ?x_24 =?= nondiscrete_normed_field 𝕜
[type_context.is_def_eq_detail] [4]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] [4]: F × G =?= 𝕜
[type_context.is_def_eq_detail] on failure: F × G =?= 𝕜
[type_context.is_def_eq_detail] on failure: nondiscrete_normed_field ?x_24 =?= nondiscrete_normed_field 𝕜
[type_context.is_def_eq] nondiscrete_normed_field ?x_24 =?= nondiscrete_normed_field 𝕜 ... failed  (approximate mode)
failed is_def_eq
[class_instances] (3) ?x_25 : nondiscrete_normed_field (F × G) := complex.nondiscrete_normed_field
[type_context.is_def_eq_detail] [3]: nondiscrete_normed_field ?x_24 =?= nondiscrete_normed_field ℂ
[type_context.is_def_eq_detail] [4]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] [4]: F × G =?= ℂ
[type_context.is_def_eq_detail] on failure: F × G =?= ℂ
[type_context.is_def_eq_detail] on failure: nondiscrete_normed_field ?x_24 =?= nondiscrete_normed_field ℂ
[type_context.is_def_eq] nondiscrete_normed_field ?x_24 =?= nondiscrete_normed_field ℂ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (3) ?x_25 : nondiscrete_normed_field (F × G) := real.nondiscrete_normed_field
[type_context.is_def_eq_detail] [3]: nondiscrete_normed_field ?x_24 =?= nondiscrete_normed_field ℝ
[type_context.is_def_eq_detail] [4]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] [4]: F × G =?= ℝ
[type_context.is_def_eq_detail] on failure: F × G =?= ℝ
[type_context.is_def_eq_detail] on failure: nondiscrete_normed_field ?x_24 =?= nondiscrete_normed_field ℝ
[type_context.is_def_eq] nondiscrete_normed_field ?x_24 =?= nondiscrete_normed_field ℝ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_21 : normed_ring (F × G) := @prod.normed_ring ?x_22 ?x_23 ?x_24 ?x_25
[type_context.is_def_eq_detail] [3]: normed_ring ?x_20 =?= normed_ring (?x_22 × ?x_23)
[type_context.is_def_eq_detail] [4]: normed_ring =?= normed_ring
[type_context.is_def_eq_detail] [4]: F × G =?= ?x_22 × ?x_23
[type_context.is_def_eq_detail] [5]: prod =?= prod
[type_context.is_def_eq_detail] process_assignment ?x_22 := F
[type_context.is_def_eq_detail] assign: ?x_22 := F
[type_context.is_def_eq_detail] process_assignment ?x_23 := G
[type_context.is_def_eq_detail] assign: ?x_23 := G
[type_context.is_def_eq] normed_ring ?x_20 =?= normed_ring (?x_22 × ?x_23) ... success  (approximate mode)
[class_instances] (2) ?x_24 : normed_ring F := @normed_field.to_normed_ring ?x_26 ?x_27
[type_context.is_def_eq_detail] [3]: normed_ring ?x_22 =?= normed_ring ?x_26
[type_context.is_def_eq_detail] [4]: normed_ring =?= normed_ring
[type_context.is_def_eq_detail] process_assignment ?x_26 := F
[type_context.is_def_eq_detail] assign: ?x_26 := F
[type_context.is_def_eq] normed_ring ?x_22 =?= normed_ring ?x_26 ... success  (approximate mode)
[class_instances] (3) ?x_27 : normed_field F := complex.normed_field
[type_context.is_def_eq_detail] [3]: normed_field ?x_26 =?= normed_field ℂ
[type_context.is_def_eq_detail] [4]: normed_field =?= normed_field
[type_context.is_def_eq_detail] on failure: normed_field ?x_26 =?= normed_field ℂ
[type_context.is_def_eq] normed_field ?x_26 =?= normed_field ℂ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (3) ?x_27 : normed_field F := real.normed_field
[type_context.is_def_eq_detail] [3]: normed_field ?x_26 =?= normed_field ℝ
[type_context.is_def_eq_detail] [4]: normed_field =?= normed_field
[type_context.is_def_eq_detail] on failure: normed_field ?x_26 =?= normed_field ℝ
[type_context.is_def_eq] normed_field ?x_26 =?= normed_field ℝ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (3) ?x_27 : normed_field F := @nondiscrete_normed_field.to_normed_field ?x_28 ?x_29
[type_context.is_def_eq_detail] [3]: normed_field ?x_26 =?= normed_field ?x_28
[type_context.is_def_eq_detail] [4]: normed_field =?= normed_field
[type_context.is_def_eq_detail] process_assignment ?x_28 := F
[type_context.is_def_eq_detail] assign: ?x_28 := F
[type_context.is_def_eq] normed_field ?x_26 =?= normed_field ?x_28 ... success  (approximate mode)
[class_instances] (4) ?x_29 : nondiscrete_normed_field F := _inst_4
[type_context.is_def_eq_detail] [3]: nondiscrete_normed_field ?x_28 =?= nondiscrete_normed_field 𝕜
[type_context.is_def_eq_detail] [4]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] on failure: nondiscrete_normed_field ?x_28 =?= nondiscrete_normed_field 𝕜
[type_context.is_def_eq] nondiscrete_normed_field ?x_28 =?= nondiscrete_normed_field 𝕜 ... failed  (approximate mode)
failed is_def_eq
[class_instances] (4) ?x_29 : nondiscrete_normed_field F := complex.nondiscrete_normed_field
[type_context.is_def_eq_detail] [3]: nondiscrete_normed_field ?x_28 =?= nondiscrete_normed_field ℂ
[type_context.is_def_eq_detail] [4]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] on failure: nondiscrete_normed_field ?x_28 =?= nondiscrete_normed_field ℂ
[type_context.is_def_eq] nondiscrete_normed_field ?x_28 =?= nondiscrete_normed_field ℂ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (4) ?x_29 : nondiscrete_normed_field F := real.nondiscrete_normed_field
[type_context.is_def_eq_detail] [3]: nondiscrete_normed_field ?x_28 =?= nondiscrete_normed_field ℝ
[type_context.is_def_eq_detail] [4]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] on failure: nondiscrete_normed_field ?x_28 =?= nondiscrete_normed_field ℝ
[type_context.is_def_eq] nondiscrete_normed_field ?x_28 =?= nondiscrete_normed_field ℝ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (2) ?x_24 : normed_ring F := @prod.normed_ring ?x_26 ?x_27 ?x_28 ?x_29
[type_context.is_def_eq_detail] [3]: normed_ring ?x_22 =?= normed_ring (?x_26 × ?x_27)
[type_context.is_def_eq_detail] [4]: normed_ring =?= normed_ring
[type_context.is_def_eq_detail] [4]: F =?= ?x_26 × ?x_27
[type_context.is_def_eq_detail] on failure: F =?= ?x_26 × ?x_27
[type_context.is_def_eq_detail] on failure: normed_ring ?x_22 =?= normed_ring (?x_26 × ?x_27)
[type_context.is_def_eq] normed_ring ?x_22 =?= normed_ring (?x_26 × ?x_27) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_11 : normed_group (F × G) := @fintype.normed_group ?x_12 ?x_13 ?x_14 ?x_15
[type_context.is_def_eq_detail] [3]: normed_group (F × G) =?= normed_group (Π (b : ?x_12), ?x_13 b)
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [4]: F × G =?= Π (b : ?x_12), ?x_13 b
[type_context.is_def_eq_detail] on failure: F × G =?= Π (b : ?x_12), ?x_13 b
[type_context.is_def_eq_detail] on failure: normed_group (F × G) =?= normed_group (Π (b : ?x_12), ?x_13 b)
[type_context.is_def_eq] normed_group (F × G) =?= normed_group (Π (b : ?x_12), ?x_13 b) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_11 : normed_group (F × G) := @prod.normed_group ?x_16 ?x_17 ?x_18 ?x_19
[type_context.is_def_eq_detail] [3]: normed_group (F × G) =?= normed_group (?x_16 × ?x_17)
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [4]: F × G =?= ?x_16 × ?x_17
[type_context.is_def_eq_detail] [5]: prod =?= prod
[type_context.is_def_eq_detail] process_assignment ?x_16 := F
[type_context.is_def_eq_detail] assign: ?x_16 := F
[type_context.is_def_eq_detail] process_assignment ?x_17 := G
[type_context.is_def_eq_detail] assign: ?x_17 := G
[type_context.is_def_eq] normed_group (F × G) =?= normed_group (?x_16 × ?x_17) ... success  (approximate mode)
[class_instances] (1) ?x_18 : normed_group F := _inst_3
[type_context.is_def_eq_detail] [3]: normed_group ?x_16 =?= normed_group G
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] on failure: normed_group ?x_16 =?= normed_group G
[type_context.is_def_eq] normed_group ?x_16 =?= normed_group G ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_18 : normed_group F := _inst_2
[type_context.is_def_eq_detail] [3]: normed_group ?x_16 =?= normed_group F
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq] normed_group ?x_16 =?= normed_group F ... success  (approximate mode)
[class_instances] (1) ?x_19 : normed_group G := _inst_3
[type_context.is_def_eq_detail] [3]: normed_group ?x_17 =?= normed_group G
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq] normed_group ?x_17 =?= normed_group G ... success  (approximate mode)
[type_context.is_def_eq_detail] [3]: @uniform_space.to_topological_space (F × G)
  (@metric_space.to_uniform_space' (F × G)
     (@normed_group.to_metric_space (F × G) (@prod.normed_group F G _inst_2 _inst_3))) =?= @uniform_space.to_topological_space ?x_3
  (@metric_space.to_uniform_space' ?x_3 (@normed_group.to_metric_space ?x_3 (@prod.normed_group F G _inst_2 _inst_3)))
[type_context.is_def_eq_detail] [3]: @normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_group.to_add_comm_group ?x_3 ?x_5
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_20 : @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 := _inst_7
[type_context.is_def_eq_detail] [3]: @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq_detail] on failure: @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
[type_context.is_def_eq] @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3 ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_20 : @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 := _inst_6
[type_context.is_def_eq_detail] [3]: @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 =?= @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq_detail] on failure: @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 =?= @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
[type_context.is_def_eq] @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 =?= @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2 ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_20 : @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 := _inst_5
[type_context.is_def_eq] @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 =?= @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 ... success  (approximate mode)
[type_context.is_def_eq_detail] [3]: @vector_space.to_module 𝕜 E
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
  (@normed_group.to_add_comm_group E _inst_1)
  (@normed_space.to_vector_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 _inst_5) =?= @vector_space.to_module ?x_1 ?x_2
  (@normed_field.to_discrete_field ?x_1 (@nondiscrete_normed_field.to_normed_field ?x_1 ?x_6))
  (@normed_group.to_add_comm_group ?x_2 ?x_4)
  (@normed_space.to_vector_space ?x_1 ?x_2 (@nondiscrete_normed_field.to_normed_field ?x_1 ?x_6) ?x_4 _inst_5)
[type_context.is_def_eq_detail] [4]: vector_space.to_module =?= vector_space.to_module
[type_context.is_def_eq_detail] [4]: @normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @normed_field.to_discrete_field ?x_1 (@nondiscrete_normed_field.to_normed_field ?x_1 ?x_6)
[type_context.is_def_eq_detail] [5]: normed_field.to_discrete_field =?= normed_field.to_discrete_field
[type_context.is_def_eq_detail] [5]: @nondiscrete_normed_field.to_normed_field 𝕜 _inst_4 =?= @nondiscrete_normed_field.to_normed_field ?x_1 ?x_6
[type_context.is_def_eq_detail] [6]: nondiscrete_normed_field.to_normed_field =?= nondiscrete_normed_field.to_normed_field
[type_context.is_def_eq_detail] [4]: @normed_group.to_add_comm_group E _inst_1 =?= @normed_group.to_add_comm_group ?x_2 ?x_4
[type_context.is_def_eq_detail] [5]: normed_group.to_add_comm_group =?= normed_group.to_add_comm_group
[type_context.is_def_eq_detail] [4]: @normed_space.to_vector_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 _inst_5 =?= @normed_space.to_vector_space ?x_1 ?x_2 (@nondiscrete_normed_field.to_normed_field ?x_1 ?x_6) ?x_4 _inst_5
[type_context.is_def_eq_detail] [5]: normed_space.to_vector_space =?= normed_space.to_vector_space
[type_context.is_def_eq_detail] [5]: @nondiscrete_normed_field.to_normed_field 𝕜 _inst_4 =?= @nondiscrete_normed_field.to_normed_field ?x_1 ?x_6
[type_context.is_def_eq_detail] [6]: nondiscrete_normed_field.to_normed_field =?= nondiscrete_normed_field.to_normed_field
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_21 : @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) := _inst_7
[type_context.is_def_eq_detail] [3]: @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq_detail] [4]: F × G =?= G
[type_context.is_def_eq_detail] on failure: F × G =?= G
[type_context.is_def_eq_detail] on failure: @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
[type_context.is_def_eq] @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3 ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_21 : @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) := _inst_6
[type_context.is_def_eq_detail] [3]: @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq_detail] [4]: F × G =?= F
[type_context.is_def_eq_detail] on failure: F × G =?= F
[type_context.is_def_eq_detail] on failure: @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
[type_context.is_def_eq] @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2 ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_21 : @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) := _inst_5
[type_context.is_def_eq_detail] [3]: @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq_detail] [4]: F × G =?= E
[type_context.is_def_eq_detail] on failure: F × G =?= E
[type_context.is_def_eq_detail] on failure: @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1
[type_context.is_def_eq] @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space 𝕜 E (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_1 ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_21 : @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) := @fintype.normed_space ?x_22 ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28
[type_context.is_def_eq_detail] [3]: @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space ?x_22 (Π (i : ?x_23), ?x_25 i) ?x_24
  (@fintype.normed_group ?x_23 (λ (i : ?x_23), ?x_25 i) ?x_26 (λ (i : ?x_23), ?x_27 i))
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq_detail] process_assignment ?x_22 := 𝕜
[type_context.is_def_eq_detail] assign: ?x_22 := 𝕜
[type_context.is_def_eq_detail] [4]: F × G =?= Π (i : ?x_23), ?x_25 i
[type_context.is_def_eq_detail] on failure: F × G =?= Π (i : ?x_23), ?x_25 i
[type_context.is_def_eq_detail] on failure: @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space ?x_22 (Π (i : ?x_23), ?x_25 i) ?x_24
  (@fintype.normed_group ?x_23 (λ (i : ?x_23), ?x_25 i) ?x_26 (λ (i : ?x_23), ?x_27 i))
[type_context.is_def_eq] @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space ?x_22 (Π (i : ?x_23), ?x_25 i) ?x_24
  (@fintype.normed_group ?x_23 (λ (i : ?x_23), ?x_25 i) ?x_26 (λ (i : ?x_23), ?x_27 i)) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_21 : @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) := @prod.normed_space ?x_29 ?x_30 ?x_31 ?x_32 ?x_33 ?x_34 ?x_35 ?x_36
[type_context.is_def_eq_detail] [3]: @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space ?x_29 (?x_31 × ?x_32) ?x_30 (@prod.normed_group ?x_31 ?x_32 ?x_33 ?x_35)
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq_detail] process_assignment ?x_29 := 𝕜
[type_context.is_def_eq_detail] assign: ?x_29 := 𝕜
[type_context.is_def_eq_detail] [4]: F × G =?= ?x_31 × ?x_32
[type_context.is_def_eq_detail] [5]: prod =?= prod
[type_context.is_def_eq_detail] process_assignment ?x_31 := F
[type_context.is_def_eq_detail] assign: ?x_31 := F
[type_context.is_def_eq_detail] process_assignment ?x_32 := G
[type_context.is_def_eq_detail] assign: ?x_32 := G
[type_context.is_def_eq_detail] process_assignment ?x_30 := @nondiscrete_normed_field.to_normed_field 𝕜 _inst_4
[type_context.is_def_eq_detail] [4]: normed_field ?x_29 =?= normed_field 𝕜
[type_context.is_def_eq_detail] [5]: normed_field =?= normed_field
[type_context.is_def_eq_detail] assign: ?x_30 := @nondiscrete_normed_field.to_normed_field 𝕜 _inst_4
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_37 : normed_group F := _inst_3
[type_context.is_def_eq_detail] [4]: normed_group F =?= normed_group G
[type_context.is_def_eq_detail] [5]: normed_group =?= normed_group
[type_context.is_def_eq_detail] on failure: normed_group F =?= normed_group G
[type_context.is_def_eq] normed_group F =?= normed_group G ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_37 : normed_group F := _inst_2
[type_context.is_def_eq] normed_group F =?= normed_group F ... success  (approximate mode)
[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_38 : normed_group G := _inst_3
[type_context.is_def_eq] normed_group G =?= normed_group G ... success  (approximate mode)
[type_context.is_def_eq_detail] [4]: @prod.normed_group F G _inst_2 _inst_3 =?= @prod.normed_group ?x_31 ?x_32 _inst_2 _inst_3
[type_context.is_def_eq] @normed_space 𝕜 (F × G) (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
  (@prod.normed_group F G _inst_2 _inst_3) =?= @normed_space ?x_29 (?x_31 × ?x_32) ?x_30 (@prod.normed_group ?x_31 ?x_32 ?x_33 ?x_35) ... success  (approximate mode)
[class_instances] (1) ?x_30 : normed_field 𝕜 := complex.normed_field
[type_context.is_def_eq_detail] [3]: normed_field ?x_29 =?= normed_field ℂ
[type_context.is_def_eq_detail] [4]: normed_field =?= normed_field
[type_context.is_def_eq_detail] on failure: normed_field ?x_29 =?= normed_field ℂ
[type_context.is_def_eq] normed_field ?x_29 =?= normed_field ℂ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_30 : normed_field 𝕜 := real.normed_field
[type_context.is_def_eq_detail] [3]: normed_field ?x_29 =?= normed_field ℝ
[type_context.is_def_eq_detail] [4]: normed_field =?= normed_field
[type_context.is_def_eq_detail] on failure: normed_field ?x_29 =?= normed_field ℝ
[type_context.is_def_eq] normed_field ?x_29 =?= normed_field ℝ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_30 : normed_field 𝕜 := @nondiscrete_normed_field.to_normed_field ?x_39 ?x_40
[type_context.is_def_eq_detail] [3]: normed_field ?x_29 =?= normed_field ?x_39
[type_context.is_def_eq_detail] [4]: normed_field =?= normed_field
[type_context.is_def_eq_detail] process_assignment ?x_39 := 𝕜
[type_context.is_def_eq_detail] assign: ?x_39 := 𝕜
[type_context.is_def_eq] normed_field ?x_29 =?= normed_field ?x_39 ... success  (approximate mode)
[class_instances] (2) ?x_40 : nondiscrete_normed_field 𝕜 := _inst_4
[type_context.is_def_eq_detail] [3]: nondiscrete_normed_field ?x_39 =?= nondiscrete_normed_field 𝕜
[type_context.is_def_eq_detail] [4]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq] nondiscrete_normed_field ?x_39 =?= nondiscrete_normed_field 𝕜 ... success  (approximate mode)
[class_instances] (1) ?x_33 : normed_group F := _inst_3
[type_context.is_def_eq_detail] [3]: normed_group ?x_31 =?= normed_group G
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq_detail] on failure: normed_group ?x_31 =?= normed_group G
[type_context.is_def_eq] normed_group ?x_31 =?= normed_group G ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_33 : normed_group F := _inst_2
[type_context.is_def_eq_detail] [3]: normed_group ?x_31 =?= normed_group F
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq] normed_group ?x_31 =?= normed_group F ... success  (approximate mode)
[class_instances] (1) ?x_34 : @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2 := _inst_7
[type_context.is_def_eq_detail] [3]: @normed_space ?x_29 ?x_31 ?x_30 ?x_33 =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq_detail] on failure: @normed_space ?x_29 ?x_31 ?x_30 ?x_33 =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
[type_context.is_def_eq] @normed_space ?x_29 ?x_31 ?x_30 ?x_33 =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3 ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_34 : @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2 := _inst_6
[type_context.is_def_eq_detail] [3]: @normed_space ?x_29 ?x_31 ?x_30 ?x_33 =?= @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq] @normed_space ?x_29 ?x_31 ?x_30 ?x_33 =?= @normed_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2 ... success  (approximate mode)
[class_instances] (1) ?x_35 : normed_group G := _inst_3
[type_context.is_def_eq_detail] [3]: normed_group ?x_32 =?= normed_group G
[type_context.is_def_eq_detail] [4]: normed_group =?= normed_group
[type_context.is_def_eq] normed_group ?x_32 =?= normed_group G ... success  (approximate mode)
[class_instances] (1) ?x_36 : @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3 := _inst_7
[type_context.is_def_eq_detail] [3]: @normed_space ?x_29 ?x_32 ?x_30 ?x_35 =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
[type_context.is_def_eq_detail] [4]: normed_space =?= normed_space
[type_context.is_def_eq] @normed_space ?x_29 ?x_32 ?x_30 ?x_35 =?= @normed_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3 ... success  (approximate mode)
[type_context.is_def_eq_detail] [3]: @prod.module 𝕜 F G
  (@normed_ring.to_ring 𝕜
     (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
  (@normed_group.to_add_comm_group F _inst_2)
  (@normed_group.to_add_comm_group G _inst_3)
  (@vector_space.to_module 𝕜 F
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
     (@normed_group.to_add_comm_group F _inst_2)
     (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2 _inst_6))
  (@vector_space.to_module 𝕜 G
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
     (@normed_group.to_add_comm_group G _inst_3)
     (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3 _inst_7)) =?= @vector_space.to_module ?x_1 ?x_3
  (@normed_field.to_discrete_field ?x_1 (@nondiscrete_normed_field.to_normed_field ?x_1 ?x_6))
  (@normed_group.to_add_comm_group ?x_3 ?x_5)
  (@normed_space.to_vector_space ?x_1 ?x_3 (@nondiscrete_normed_field.to_normed_field ?x_1 ?x_6) ?x_5
     (@prod.normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) F G _inst_2 _inst_6 _inst_3
        _inst_7))
[type_context.is_def_eq_detail] unfold left: prod.module
[type_context.is_def_eq_detail] [4]: @module.mk 𝕜 (F × G)
  (@normed_ring.to_ring 𝕜
     (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
  (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2) (@normed_group.to_add_comm_group G _inst_3))
  (@prod.semimodule 𝕜 F G
     (@ring.to_semiring 𝕜
        (@normed_ring.to_ring 𝕜
           (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
     (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
     (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
     (@module.to_semimodule 𝕜 F
        (@normed_ring.to_ring 𝕜
           (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
        (@normed_group.to_add_comm_group F _inst_2)
        (@vector_space.to_module 𝕜 F
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
           (@normed_group.to_add_comm_group F _inst_2)
           (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
              _inst_6)))
     (@module.to_semimodule 𝕜 G
        (@normed_ring.to_ring 𝕜
           (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
        (@normed_group.to_add_comm_group G _inst_3)
        (@vector_space.to_module 𝕜 G
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
           (@normed_group.to_add_comm_group G _inst_3)
           (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
              _inst_7)))) =?= @vector_space.to_module ?x_1 ?x_3
  (@normed_field.to_discrete_field ?x_1 (@nondiscrete_normed_field.to_normed_field ?x_1 ?x_6))
  (@normed_group.to_add_comm_group ?x_3 ?x_5)
  (@normed_space.to_vector_space ?x_1 ?x_3 (@nondiscrete_normed_field.to_normed_field ?x_1 ?x_6) ?x_5
     (@prod.normed_space 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) F G _inst_2 _inst_6 _inst_3
        _inst_7))
[type_context.is_def_eq_detail] [5]: @module.mk 𝕜 (F × G)
  (@normed_ring.to_ring 𝕜
     (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
  (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2) (@normed_group.to_add_comm_group G _inst_3))
  (@prod.semimodule 𝕜 F G
     (@ring.to_semiring 𝕜
        (@normed_ring.to_ring 𝕜
           (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
     (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
     (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
     (@module.to_semimodule 𝕜 F
        (@normed_ring.to_ring 𝕜
           (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
        (@normed_group.to_add_comm_group F _inst_2)
        (@vector_space.to_module 𝕜 F
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
           (@normed_group.to_add_comm_group F _inst_2)
           (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
              _inst_6)))
     (@module.to_semimodule 𝕜 G
        (@normed_ring.to_ring 𝕜
           (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
        (@normed_group.to_add_comm_group G _inst_3)
        (@vector_space.to_module 𝕜 G
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
           (@normed_group.to_add_comm_group G _inst_3)
           (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
              _inst_7)))) =?= @module.mk 𝕜 (F × G)
  (@domain.to_ring 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
  (@semimodule.mk 𝕜 (F × G)
     (@ring.to_semiring 𝕜
        (@domain.to_ring 𝕜
           (@division_ring.to_domain 𝕜
              (@field.to_division_ring 𝕜
                 (@discrete_field.to_field 𝕜
                    (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))))
     (@add_comm_group.to_add_comm_monoid (F × G)
        (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)))
     (@distrib_mul_action.mk 𝕜 (F × G)
        (@semiring.to_monoid 𝕜
           (@ring.to_semiring 𝕜
              (@domain.to_ring 𝕜
                 (@division_ring.to_domain 𝕜
                    (@field.to_division_ring 𝕜
                       (@discrete_field.to_field 𝕜
                          (@normed_field.to_discrete_field 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))))
        (@add_comm_monoid.to_add_monoid (F × G)
           (@add_comm_group.to_add_comm_monoid (F × G)
              (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))))
        (@distrib_mul_action.to_mul_action 𝕜 (F × G)
           (@semiring.to_monoid 𝕜
              (@ring.to_semiring 𝕜
                 (@domain.to_ring 𝕜
                    (@division_ring.to_domain 𝕜
                       (@field.to_division_ring 𝕜
                          (@discrete_field.to_field 𝕜
                             (@normed_field.to_discrete_field 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))))
           (@add_comm_monoid.to_add_monoid (F × G)
              (@add_comm_group.to_add_comm_monoid (F × G)
                 (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                    (@normed_group.to_add_comm_group G _inst_3))))
           (@semimodule.to_distrib_mul_action 𝕜 (F × G)
              (@ring.to_semiring 𝕜
                 (@domain.to_ring 𝕜
                    (@division_ring.to_domain 𝕜
                       (@field.to_division_ring 𝕜
                          (@discrete_field.to_field 𝕜
                             (@normed_field.to_discrete_field 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))))
              (@add_comm_group.to_add_comm_monoid (F × G)
                 (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                    (@normed_group.to_add_comm_group G _inst_3)))
              (@module.to_semimodule 𝕜 (F × G)
                 (@domain.to_ring 𝕜
                    (@division_ring.to_domain 𝕜
                       (@field.to_division_ring 𝕜
                          (@discrete_field.to_field 𝕜
                             (@normed_field.to_discrete_field 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
                 (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                    (@normed_group.to_add_comm_group G _inst_3))
                 (@vector_space.to_module 𝕜 (F × G)
                    (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                    (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                       (@normed_group.to_add_comm_group G _inst_3))
                    (@prod.vector_space 𝕜 F G
                       (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                       (@normed_group.to_add_comm_group F _inst_2)
                       (@normed_group.to_add_comm_group G _inst_3)
                       (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                          _inst_2
                          _inst_6)
                       (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                          _inst_3
                          _inst_7))))))
        _
        _)
     _
     _)
[type_context.is_def_eq_detail] [6]: @normed_ring.to_ring 𝕜 (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @domain.to_ring 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] unfold right: domain.to_ring
[type_context.is_def_eq_detail] [7]: @normed_ring.to_ring 𝕜 (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @ring.mk 𝕜
  (@domain.add 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  (@domain.zero 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  _
  (@domain.neg 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  _
  (@domain.mul 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  (@domain.one 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  _
  _
  _
[type_context.is_def_eq_detail] [8]: @ring.mk 𝕜
  (@discrete_field.add 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
  _
  (@discrete_field.zero 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
  _
  _
  (@discrete_field.neg 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
  _
  _
  (@discrete_field.mul 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
  _
  (@discrete_field.one 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
  _
  _
  _
  _ =?= @ring.mk 𝕜
  (@domain.add 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  (@domain.zero 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  _
  (@domain.neg 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  _
  (@domain.mul 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  (@domain.one 𝕜
     (@division_ring.to_domain 𝕜
        (@field.to_division_ring 𝕜
           (@discrete_field.to_field 𝕜
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
  _
  _
  _
  _
[type_context.is_def_eq_detail] [9]: @discrete_field.add 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @domain.add 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @discrete_field.add 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @division_ring.add 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @discrete_field.add 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @field.add 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_1 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.add_assoc 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_1 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.add_assoc 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_1 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.add_assoc 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_1 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.add_assoc 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_1 =?= discrete_field.add_assoc
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_1 =?= discrete_field.add_assoc
[type_context.is_def_eq_detail] [9]: @discrete_field.zero 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @domain.zero 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @discrete_field.zero 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @division_ring.zero 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @discrete_field.zero 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @field.zero 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_2 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.zero_add 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_2 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.zero_add 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_2 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.zero_add 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_2 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.zero_add 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_2 =?= discrete_field.zero_add
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_2 =?= discrete_field.zero_add
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_3 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.add_zero 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_3 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.add_zero 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_3 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.add_zero 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_3 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.add_zero 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_3 =?= discrete_field.add_zero
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_3 =?= discrete_field.add_zero
[type_context.is_def_eq_detail] [9]: @discrete_field.neg 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @domain.neg 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @discrete_field.neg 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @division_ring.neg 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @discrete_field.neg 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @field.neg 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_4 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.add_left_neg 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_4 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.add_left_neg 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_4 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.add_left_neg 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_4 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.add_left_neg 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_4 =?= discrete_field.add_left_neg
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_4 =?= discrete_field.add_left_neg
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_5 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.add_comm 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_5 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.add_comm 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_5 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.add_comm 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_5 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.add_comm 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_5 =?= discrete_field.add_comm
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_5 =?= discrete_field.add_comm
[type_context.is_def_eq_detail] [9]: @discrete_field.mul 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @domain.mul 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @discrete_field.mul 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @division_ring.mul 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @discrete_field.mul 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @field.mul 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_6 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.mul_assoc 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_6 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.mul_assoc 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_6 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.mul_assoc 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_6 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.mul_assoc 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_6 =?= discrete_field.mul_assoc
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_6 =?= discrete_field.mul_assoc
[type_context.is_def_eq_detail] [9]: @discrete_field.one 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @domain.one 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @discrete_field.one 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @division_ring.one 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @discrete_field.one 𝕜 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)) =?= @field.one 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_7 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.one_mul 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_7 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.one_mul 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_7 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.one_mul 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_7 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.one_mul 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_7 =?= discrete_field.one_mul
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_7 =?= discrete_field.one_mul
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_8 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.mul_one 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_8 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.mul_one 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_8 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.mul_one 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_8 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.mul_one 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_8 =?= discrete_field.mul_one
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_8 =?= discrete_field.mul_one
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_9 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.left_distrib 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_9 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.left_distrib 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_9 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.left_distrib 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_9 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.left_distrib 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_9 =?= discrete_field.left_distrib
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_9 =?= discrete_field.left_distrib
[type_context.is_def_eq_detail] [9]: @normed_field.to_normed_ring._proof_10 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @domain.right_distrib 𝕜
  (@division_ring.to_domain 𝕜
     (@field.to_division_ring 𝕜
        (@discrete_field.to_field 𝕜
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
[type_context.is_def_eq_detail] [10]: @normed_field.to_normed_ring._proof_10 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @division_ring.right_distrib 𝕜
  (@field.to_division_ring 𝕜
     (@discrete_field.to_field 𝕜
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
[type_context.is_def_eq_detail] [11]: @normed_field.to_normed_ring._proof_10 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @field.right_distrib 𝕜
  (@discrete_field.to_field 𝕜
     (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
[type_context.is_def_eq_detail] [12]: @normed_field.to_normed_ring._proof_10 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) =?= @discrete_field.right_distrib 𝕜
  (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
[type_context.is_def_eq_detail] [13]: normed_field.to_normed_ring._proof_10 =?= discrete_field.right_distrib
[type_context.is_def_eq_detail] [14]: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] [15]: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field =?= discrete_field
[type_context.is_def_eq_detail] on failure: normed_field α =?= discrete_field α
[type_context.is_def_eq_detail] on failure: normed_field.to_normed_ring._proof_10 =?= discrete_field.right_distrib
[type_context.is_def_eq_detail] [6]: @prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2) (@normed_group.to_add_comm_group G _inst_3) =?= @normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)
[type_context.is_def_eq_detail] unfold left: prod.add_comm_group
[type_context.is_def_eq_detail] [7]: @add_comm_group.mk (F × G)
  (@add_comm_semigroup.add (F × G)
     (@prod.add_comm_semigroup F G
        (@add_comm_monoid.to_add_comm_semigroup F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
        (@add_comm_monoid.to_add_comm_semigroup G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  _
  (@add_group.zero (F × G)
     (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
        (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
  _
  _
  (@add_group.neg (F × G)
     (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
        (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
  _
  _ =?= @normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)
[type_context.is_def_eq_detail] [8]: @add_comm_group.mk (F × G)
  (@add_comm_semigroup.add (F × G)
     (@prod.add_comm_semigroup F G
        (@add_comm_monoid.to_add_comm_semigroup F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
        (@add_comm_monoid.to_add_comm_semigroup G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  _
  (@add_group.zero (F × G)
     (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
        (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
  _
  _
  (@add_group.neg (F × G)
     (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
        (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
  _
  _ =?= @prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2) (@normed_group.to_add_comm_group G _inst_3)
[type_context.is_def_eq_detail] unfold right: prod.add_comm_group
[type_context.is_def_eq_detail] [6]: @prod.semimodule 𝕜 F G
  (@ring.to_semiring 𝕜
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
  (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@module.to_semimodule 𝕜 F
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group F _inst_2)
     (@vector_space.to_module 𝕜 F
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group F _inst_2)
        (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
           _inst_6)))
  (@module.to_semimodule 𝕜 G
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group G _inst_3)
     (@vector_space.to_module 𝕜 G
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group G _inst_3)
        (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
           _inst_7))) =?= @semimodule.mk 𝕜 (F × G)
  (@ring.to_semiring 𝕜
     (@domain.to_ring 𝕜
        (@division_ring.to_domain 𝕜
           (@field.to_division_ring 𝕜
              (@discrete_field.to_field 𝕜
                 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))))
  (@add_comm_group.to_add_comm_monoid (F × G)
     (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)))
  (@distrib_mul_action.mk 𝕜 (F × G)
     (@semiring.to_monoid 𝕜
        (@ring.to_semiring 𝕜
           (@domain.to_ring 𝕜
              (@division_ring.to_domain 𝕜
                 (@field.to_division_ring 𝕜
                    (@discrete_field.to_field 𝕜
                       (@normed_field.to_discrete_field 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))))
     (@add_comm_monoid.to_add_monoid (F × G)
        (@add_comm_group.to_add_comm_monoid (F × G)
           (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))))
     (@distrib_mul_action.to_mul_action 𝕜 (F × G)
        (@semiring.to_monoid 𝕜
           (@ring.to_semiring 𝕜
              (@domain.to_ring 𝕜
                 (@division_ring.to_domain 𝕜
                    (@field.to_division_ring 𝕜
                       (@discrete_field.to_field 𝕜
                          (@normed_field.to_discrete_field 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))))
        (@add_comm_monoid.to_add_monoid (F × G)
           (@add_comm_group.to_add_comm_monoid (F × G)
              (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                 (@normed_group.to_add_comm_group G _inst_3))))
        (@semimodule.to_distrib_mul_action 𝕜 (F × G)
           (@ring.to_semiring 𝕜
              (@domain.to_ring 𝕜
                 (@division_ring.to_domain 𝕜
                    (@field.to_division_ring 𝕜
                       (@discrete_field.to_field 𝕜
                          (@normed_field.to_discrete_field 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))))
           (@add_comm_group.to_add_comm_monoid (F × G)
              (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                 (@normed_group.to_add_comm_group G _inst_3)))
           (@module.to_semimodule 𝕜 (F × G)
              (@domain.to_ring 𝕜
                 (@division_ring.to_domain 𝕜
                    (@field.to_division_ring 𝕜
                       (@discrete_field.to_field 𝕜
                          (@normed_field.to_discrete_field 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
              (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                 (@normed_group.to_add_comm_group G _inst_3))
              (@vector_space.to_module 𝕜 (F × G)
                 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                 (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                    (@normed_group.to_add_comm_group G _inst_3))
                 (@prod.vector_space 𝕜 F G
                    (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                    (@normed_group.to_add_comm_group F _inst_2)
                    (@normed_group.to_add_comm_group G _inst_3)
                    (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                       _inst_2
                       _inst_6)
                    (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                       _inst_3
                       _inst_7))))))
     _
     _)
  _
  _
[type_context.is_def_eq_detail] unfold left: prod.semimodule
[type_context.is_def_eq_detail] [7]: @semimodule.mk 𝕜 (F × G)
  (@ring.to_semiring 𝕜
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
  (@prod.add_comm_monoid F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
     (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
  (@distrib_mul_action.mk 𝕜 (F × G)
     (@semiring.to_monoid 𝕜
        (@ring.to_semiring 𝕜
           (@normed_ring.to_ring 𝕜
              (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
     (@add_comm_monoid.to_add_monoid (F × G)
        (@prod.add_comm_monoid F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
     (@mul_action.mk 𝕜 (F × G)
        (@semiring.to_monoid 𝕜
           (@ring.to_semiring 𝕜
              (@normed_ring.to_ring 𝕜
                 (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
        (@has_scalar.mk 𝕜 (F × G)
           (@has_scalar.smul 𝕜 (F × G)
              (@prod.has_scalar 𝕜 F G
                 (@mul_action.to_has_scalar 𝕜 F
                    (@semiring.to_monoid 𝕜
                       (@ring.to_semiring 𝕜
                          (@normed_ring.to_ring 𝕜
                             (@normed_field.to_normed_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                    (@distrib_mul_action.to_mul_action 𝕜 F
                       (@semiring.to_monoid 𝕜
                          (@ring.to_semiring 𝕜
                             (@normed_ring.to_ring 𝕜
                                (@normed_field.to_normed_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                       (@add_comm_monoid.to_add_monoid F
                          (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
                       (@semimodule.to_distrib_mul_action 𝕜 F
                          (@ring.to_semiring 𝕜
                             (@normed_ring.to_ring 𝕜
                                (@normed_field.to_normed_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
                          (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
                          (@module.to_semimodule 𝕜 F
                             (@normed_ring.to_ring 𝕜
                                (@normed_field.to_normed_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
                             (@normed_group.to_add_comm_group F _inst_2)
                             (@vector_space.to_module 𝕜 F
                                (@normed_field.to_discrete_field 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                                (@normed_group.to_add_comm_group F _inst_2)
                                (@normed_space.to_vector_space 𝕜 F
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                                   _inst_2
                                   _inst_6))))))
                 (@mul_action.to_has_scalar 𝕜 G
                    (@semiring.to_monoid 𝕜
                       (@ring.to_semiring 𝕜
                          (@normed_ring.to_ring 𝕜
                             (@normed_field.to_normed_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                    (@distrib_mul_action.to_mul_action 𝕜 G
                       (@semiring.to_monoid 𝕜
                          (@ring.to_semiring 𝕜
                             (@normed_ring.to_ring 𝕜
                                (@normed_field.to_normed_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                       (@add_comm_monoid.to_add_monoid G
                          (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
                       (@semimodule.to_distrib_mul_action 𝕜 G
                          (@ring.to_semiring 𝕜
                             (@normed_ring.to_ring 𝕜
                                (@normed_field.to_normed_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
                          (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
                          (@module.to_semimodule 𝕜 G
                             (@normed_ring.to_ring 𝕜
                                (@normed_field.to_normed_ring 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
                             (@normed_group.to_add_comm_group G _inst_3)
                             (@vector_space.to_module 𝕜 G
                                (@normed_field.to_discrete_field 𝕜
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                                (@normed_group.to_add_comm_group G _inst_3)
                                (@normed_space.to_vector_space 𝕜 G
                                   (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                                   _inst_3
                                   _inst_7)))))))))
        _
        _)
     _
     _)
  _
  _ =?= @semimodule.mk 𝕜 (F × G)
  (@ring.to_semiring 𝕜
     (@domain.to_ring 𝕜
        (@division_ring.to_domain 𝕜
           (@field.to_division_ring 𝕜
              (@discrete_field.to_field 𝕜
                 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))))
  (@add_comm_group.to_add_comm_monoid (F × G)
     (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)))
  (@distrib_mul_action.mk 𝕜 (F × G)
     (@semiring.to_monoid 𝕜
        (@ring.to_semiring 𝕜
           (@domain.to_ring 𝕜
              (@division_ring.to_domain 𝕜
                 (@field.to_division_ring 𝕜
                    (@discrete_field.to_field 𝕜
                       (@normed_field.to_discrete_field 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))))
     (@add_comm_monoid.to_add_monoid (F × G)
        (@add_comm_group.to_add_comm_monoid (F × G)
           (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))))
     (@distrib_mul_action.to_mul_action 𝕜 (F × G)
        (@semiring.to_monoid 𝕜
           (@ring.to_semiring 𝕜
              (@domain.to_ring 𝕜
                 (@division_ring.to_domain 𝕜
                    (@field.to_division_ring 𝕜
                       (@discrete_field.to_field 𝕜
                          (@normed_field.to_discrete_field 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))))
        (@add_comm_monoid.to_add_monoid (F × G)
           (@add_comm_group.to_add_comm_monoid (F × G)
              (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                 (@normed_group.to_add_comm_group G _inst_3))))
        (@semimodule.to_distrib_mul_action 𝕜 (F × G)
           (@ring.to_semiring 𝕜
              (@domain.to_ring 𝕜
                 (@division_ring.to_domain 𝕜
                    (@field.to_division_ring 𝕜
                       (@discrete_field.to_field 𝕜
                          (@normed_field.to_discrete_field 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))))
           (@add_comm_group.to_add_comm_monoid (F × G)
              (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                 (@normed_group.to_add_comm_group G _inst_3)))
           (@module.to_semimodule 𝕜 (F × G)
              (@domain.to_ring 𝕜
                 (@division_ring.to_domain 𝕜
                    (@field.to_division_ring 𝕜
                       (@discrete_field.to_field 𝕜
                          (@normed_field.to_discrete_field 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
              (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                 (@normed_group.to_add_comm_group G _inst_3))
              (@vector_space.to_module 𝕜 (F × G)
                 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                 (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                    (@normed_group.to_add_comm_group G _inst_3))
                 (@prod.vector_space 𝕜 F G
                    (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                    (@normed_group.to_add_comm_group F _inst_2)
                    (@normed_group.to_add_comm_group G _inst_3)
                    (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                       _inst_2
                       _inst_6)
                    (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                       _inst_3
                       _inst_7))))))
     _
     _)
  _
  _
[type_context.is_def_eq_detail] [8]: @prod.semimodule._proof_5 𝕜 F G
  (@ring.to_semiring 𝕜
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
  (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@module.to_semimodule 𝕜 F
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group F _inst_2)
     (@vector_space.to_module 𝕜 F
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group F _inst_2)
        (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
           _inst_6)))
  (@module.to_semimodule 𝕜 G
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group G _inst_3)
     (@vector_space.to_module 𝕜 G
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group G _inst_3)
        (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
           _inst_7))) =?= @prod.normed_space._proof_3 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) F G _inst_2 _inst_6 _inst_3
  _inst_7
[type_context.is_def_eq_detail] [9]: prod.semimodule._proof_5 =?= prod.normed_space._proof_3
[type_context.is_def_eq_detail] [10]: Type u_3 =?= normed_field α
[type_context.is_def_eq_detail] on failure: Type u_3 =?= normed_field α
[type_context.is_def_eq_detail] on failure: prod.semimodule._proof_5 =?= prod.normed_space._proof_3
[type_context.is_def_eq_detail] [9]: ((a + p₁) • @prod.fst F G p₂, (a + p₁) • @prod.snd F G p₂) =
  (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂),
   @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= (a + p₁) • p₂ = a • p₂ + p₁ • p₂
[type_context.is_def_eq_detail] [10]: ((a + p₁) • @prod.fst F G p₂, (a + p₁) • @prod.snd F G p₂) =?= (a + p₁) • p₂
[type_context.is_def_eq_detail] [11]: ((a + p₁) • @prod.fst F G p₂, (a + p₁) • @prod.snd F G p₂) =?= (a + p₁) • p₂
[type_context.is_def_eq_detail] [12]: ((a + p₁) • @prod.fst F G p₂, (a + p₁) • @prod.snd F G p₂) =?= (λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) (a + p₁) p₂
[type_context.is_def_eq_detail] after whnf_core: ((a + p₁) • @prod.fst F G p₂, (a + p₁) • @prod.snd F G p₂) =?= ((a + p₁) • @prod.fst F G p₂, (a + p₁) • @prod.snd F G p₂)
[type_context.is_def_eq_detail] [10]: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= a • p₂ + p₁ • p₂
[type_context.is_def_eq_detail] [11]: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= @add_semigroup.add (F × G)
  (@add_monoid.to_add_semigroup (F × G)
     (@add_comm_monoid.to_add_monoid (F × G)
        (@add_comm_group.to_add_comm_monoid (F × G)
           (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)))))
  (a • p₂)
  (p₁ • p₂)
[type_context.is_def_eq_detail] [12]: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= @add_monoid.add (F × G)
  (@add_comm_monoid.to_add_monoid (F × G)
     (@add_comm_group.to_add_comm_monoid (F × G)
        (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))))
  (a • p₂)
  (p₁ • p₂)
[type_context.is_def_eq_detail] [13]: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= @add_comm_monoid.add (F × G)
  (@add_comm_group.to_add_comm_monoid (F × G)
     (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)))
  (a • p₂)
  (p₁ • p₂)
[type_context.is_def_eq_detail] [14]: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= @add_comm_group.add (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
  (a • p₂)
  (p₁ • p₂)
[type_context.is_def_eq_detail] [15]: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= @add_comm_semigroup.add (F × G)
  (@prod.add_comm_semigroup F G
     (@add_comm_monoid.to_add_comm_semigroup F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_comm_monoid.to_add_comm_semigroup G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  (a • p₂)
  (p₁ • p₂)
[type_context.is_def_eq_detail] [16]: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= @add_semigroup.add (F × G)
  (@prod.add_semigroup F G
     (@add_comm_semigroup.to_add_semigroup F
        (@add_comm_monoid.to_add_comm_semigroup F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
     (@add_comm_semigroup.to_add_semigroup G
        (@add_comm_monoid.to_add_comm_semigroup G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  (a • p₂)
  (p₁ • p₂)
[type_context.is_def_eq_detail] [17]: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= a • p₂ + p₁ • p₂
[type_context.is_def_eq_detail] [18]: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= (λ (p q : F × G), (@prod.fst F G p + @prod.fst F G q, @prod.snd F G p + @prod.snd F G q)) (a • p₂) (p₁ • p₂)
[type_context.is_def_eq_detail] after whnf_core: (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)) =?= (@prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂), @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂))
[type_context.is_def_eq_detail] [19]: @prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂) =?= @prod.fst F G (a • p₂) + @prod.fst F G (p₁ • p₂)
[type_context.is_def_eq_detail] [20]: @add_semigroup.add F
  (@add_comm_semigroup.to_add_semigroup F
     (@add_comm_monoid.to_add_comm_semigroup F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
  (@prod.fst F G (a • p₂))
  (@prod.fst F G (p₁ • p₂)) =?= @add_semigroup.add F
  (@add_comm_semigroup.to_add_semigroup F
     (@add_comm_monoid.to_add_comm_semigroup F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
  (@prod.fst F G (a • p₂))
  (@prod.fst F G (p₁ • p₂))
[type_context.is_def_eq_detail] [21]: @add_comm_semigroup.add F
  (@add_comm_monoid.to_add_comm_semigroup F
     (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
  (@prod.fst F G (a • p₂))
  (@prod.fst F G (p₁ • p₂)) =?= @add_comm_semigroup.add F
  (@add_comm_monoid.to_add_comm_semigroup F
     (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
  (@prod.fst F G (a • p₂))
  (@prod.fst F G (p₁ • p₂))
[type_context.is_def_eq_detail] [22]: @add_comm_monoid.add F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@prod.fst F G (a • p₂))
  (@prod.fst F G (p₁ • p₂)) =?= @add_comm_monoid.add F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@prod.fst F G (a • p₂))
  (@prod.fst F G (p₁ • p₂))
[type_context.is_def_eq_detail] [23]: @add_comm_group.add F (@normed_group.to_add_comm_group F _inst_2) (@prod.fst F G (a • p₂))
  (@prod.fst F G (p₁ • p₂)) =?= @add_comm_group.add F (@normed_group.to_add_comm_group F _inst_2) (@prod.fst F G (a • p₂))
  (@prod.fst F G (p₁ • p₂))
[type_context.is_def_eq_detail] [24]: @prod.fst F G (a • p₂) =?= @prod.fst F G (a • p₂)
[type_context.is_def_eq_detail] [24]: @prod.fst F G (p₁ • p₂) =?= @prod.fst F G (p₁ • p₂)
[type_context.is_def_eq_detail] [19]: @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂) =?= @prod.snd F G (a • p₂) + @prod.snd F G (p₁ • p₂)
[type_context.is_def_eq_detail] [20]: @add_semigroup.add G
  (@add_comm_semigroup.to_add_semigroup G
     (@add_comm_monoid.to_add_comm_semigroup G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  (@prod.snd F G (a • p₂))
  (@prod.snd F G (p₁ • p₂)) =?= @add_semigroup.add G
  (@add_comm_semigroup.to_add_semigroup G
     (@add_comm_monoid.to_add_comm_semigroup G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  (@prod.snd F G (a • p₂))
  (@prod.snd F G (p₁ • p₂))
[type_context.is_def_eq_detail] [21]: @add_comm_semigroup.add G
  (@add_comm_monoid.to_add_comm_semigroup G
     (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
  (@prod.snd F G (a • p₂))
  (@prod.snd F G (p₁ • p₂)) =?= @add_comm_semigroup.add G
  (@add_comm_monoid.to_add_comm_semigroup G
     (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
  (@prod.snd F G (a • p₂))
  (@prod.snd F G (p₁ • p₂))
[type_context.is_def_eq_detail] [22]: @add_comm_monoid.add G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@prod.snd F G (a • p₂))
  (@prod.snd F G (p₁ • p₂)) =?= @add_comm_monoid.add G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@prod.snd F G (a • p₂))
  (@prod.snd F G (p₁ • p₂))
[type_context.is_def_eq_detail] [23]: @add_comm_group.add G (@normed_group.to_add_comm_group G _inst_3) (@prod.snd F G (a • p₂))
  (@prod.snd F G (p₁ • p₂)) =?= @add_comm_group.add G (@normed_group.to_add_comm_group G _inst_3) (@prod.snd F G (a • p₂))
  (@prod.snd F G (p₁ • p₂))
[type_context.is_def_eq_detail] [24]: @prod.snd F G (a • p₂) =?= @prod.snd F G (a • p₂)
[type_context.is_def_eq_detail] [24]: @prod.snd F G (p₁ • p₂) =?= @prod.snd F G (p₁ • p₂)
[type_context.is_def_eq_detail] [8]: @prod.semimodule._proof_6 𝕜 F G
  (@ring.to_semiring 𝕜
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
  (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@module.to_semimodule 𝕜 F
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group F _inst_2)
     (@vector_space.to_module 𝕜 F
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group F _inst_2)
        (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
           _inst_6)))
  (@module.to_semimodule 𝕜 G
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group G _inst_3)
     (@vector_space.to_module 𝕜 G
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group G _inst_3)
        (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
           _inst_7))) =?= @prod.normed_space._proof_4 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) F G _inst_2 _inst_6 _inst_3
  _inst_7
[type_context.is_def_eq_detail] [9]: prod.semimodule._proof_6 =?= prod.normed_space._proof_4
[type_context.is_def_eq_detail] [10]: Type u_3 =?= normed_field α
[type_context.is_def_eq_detail] on failure: Type u_3 =?= normed_field α
[type_context.is_def_eq_detail] on failure: prod.semimodule._proof_6 =?= prod.normed_space._proof_4
[type_context.is_def_eq_detail] [9]: 0 • _x = 0 =?= 0 • _x = 0
[type_context.is_def_eq_detail] [10]: 0 • _x =?= 0 • _x
[type_context.is_def_eq_detail] [10]: 0 =?= 0
[type_context.is_def_eq_detail] [11]: @add_monoid.zero (F × G)
  (@add_comm_monoid.to_add_monoid (F × G)
     (@prod.add_comm_monoid F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))) =?= @add_monoid.zero (F × G)
  (@add_comm_monoid.to_add_monoid (F × G)
     (@add_comm_group.to_add_comm_monoid (F × G)
        (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
           (@normed_group.to_add_comm_group G _inst_3))))
[type_context.is_def_eq_detail] [12]: @add_comm_monoid.zero (F × G)
  (@prod.add_comm_monoid F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
     (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))) =?= @add_comm_monoid.zero (F × G)
  (@add_comm_group.to_add_comm_monoid (F × G)
     (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2) (@normed_group.to_add_comm_group G _inst_3)))
[type_context.is_def_eq_detail] [13]: @add_monoid.zero (F × G)
  (@prod.add_monoid F G
     (@add_comm_monoid.to_add_monoid F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_comm_monoid.to_add_monoid G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))) =?= @add_comm_group.zero (F × G)
  (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2) (@normed_group.to_add_comm_group G _inst_3))
[type_context.is_def_eq_detail] [14]: 0 =?= @add_group.zero (F × G)
  (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
     (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))
[type_context.is_def_eq_detail] [15]: (0, 0) =?= @add_monoid.zero (F × G)
  (@prod.add_monoid F G
     (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
[type_context.is_def_eq_detail] [16]: (0, 0) =?= 0
[type_context.is_def_eq_detail] [17]: (0, 0) =?= (0, 0)
[type_context.is_def_eq_detail] [18]: 0 =?= 0
[type_context.is_def_eq_detail] [19]: @add_monoid.zero F
  (@add_comm_monoid.to_add_monoid F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))) =?= @add_monoid.zero F
  (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)))
[type_context.is_def_eq_detail] [20]: @add_comm_monoid.zero F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)) =?= @add_group.zero F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
[type_context.is_def_eq_detail] [18]: 0 =?= 0
[type_context.is_def_eq_detail] [19]: @add_monoid.zero G
  (@add_comm_monoid.to_add_monoid G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))) =?= @add_monoid.zero G
  (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))
[type_context.is_def_eq_detail] [20]: @add_comm_monoid.zero G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @add_group.zero G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))
[type_context.is_def_eq_detail] [8]: @prod.add_comm_monoid F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @add_comm_group.to_add_comm_monoid (F × G)
  (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
[type_context.is_def_eq_detail] [9]: @add_comm_monoid.mk (F × G)
  (@add_comm_semigroup.add (F × G)
     (@prod.add_comm_semigroup F G
        (@add_comm_monoid.to_add_comm_semigroup F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
        (@add_comm_monoid.to_add_comm_semigroup G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  _
  (@add_monoid.zero (F × G)
     (@prod.add_monoid F G
        (@add_comm_monoid.to_add_monoid F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
        (@add_comm_monoid.to_add_monoid G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  _
  _
  _ =?= @add_comm_group.to_add_comm_monoid (F × G)
  (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
[type_context.is_def_eq_detail] unfold right: add_comm_group.to_add_comm_monoid
[type_context.is_def_eq_detail] [10]: @add_comm_monoid.mk (F × G)
  (@add_comm_semigroup.add (F × G)
     (@prod.add_comm_semigroup F G
        (@add_comm_monoid.to_add_comm_semigroup F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
        (@add_comm_monoid.to_add_comm_semigroup G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  _
  (@add_monoid.zero (F × G)
     (@prod.add_monoid F G
        (@add_comm_monoid.to_add_monoid F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
        (@add_comm_monoid.to_add_monoid G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  _
  _
  _ =?= @add_comm_monoid.mk (F × G)
  (@add_comm_group.add (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)))
  _
  (@add_comm_group.zero (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)))
  _
  _
  _
[type_context.is_def_eq_detail] [11]: @add_comm_semigroup.add (F × G)
  (@prod.add_comm_semigroup F G
     (@add_comm_monoid.to_add_comm_semigroup F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_comm_monoid.to_add_comm_semigroup G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))) =?= @add_comm_group.add (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
[type_context.is_def_eq_detail] [12]: @add_semigroup.add (F × G)
  (@prod.add_semigroup F G
     (@add_comm_semigroup.to_add_semigroup F
        (@add_comm_monoid.to_add_comm_semigroup F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
     (@add_comm_semigroup.to_add_semigroup G
        (@add_comm_monoid.to_add_comm_semigroup G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))) =?= @add_comm_semigroup.add (F × G)
  (@prod.add_comm_semigroup F G
     (@add_comm_monoid.to_add_comm_semigroup F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_comm_monoid.to_add_comm_semigroup G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
[type_context.is_def_eq_detail] [13]: @has_add.add (F × G)
  (@prod.has_add F G
     (@add_semigroup.to_has_add F
        (@add_comm_semigroup.to_add_semigroup F
           (@add_comm_monoid.to_add_comm_semigroup F
              (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))))
     (@add_semigroup.to_has_add G
        (@add_comm_semigroup.to_add_semigroup G
           (@add_comm_monoid.to_add_comm_semigroup G
              (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))) =?= @add_semigroup.add (F × G)
  (@prod.add_semigroup F G
     (@add_comm_semigroup.to_add_semigroup F
        (@add_comm_monoid.to_add_comm_semigroup F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
     (@add_comm_semigroup.to_add_semigroup G
        (@add_comm_monoid.to_add_comm_semigroup G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
[type_context.is_def_eq_detail] [14]: λ (p q : F × G), (@prod.fst F G p + @prod.fst F G q, @prod.snd F G p + @prod.snd F G q) =?= @has_add.add (F × G)
  (@prod.has_add F G
     (@add_semigroup.to_has_add F
        (@add_comm_semigroup.to_add_semigroup F
           (@add_comm_monoid.to_add_comm_semigroup F
              (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))))
     (@add_semigroup.to_has_add G
        (@add_comm_semigroup.to_add_semigroup G
           (@add_comm_monoid.to_add_comm_semigroup G
              (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))))
[type_context.is_def_eq_detail] [11]: @prod.add_comm_monoid._proof_1 F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @add_comm_group.add_assoc (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
[type_context.is_def_eq_detail] [12]: @prod.add_comm_monoid._proof_1 F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @prod.add_comm_group._proof_1 F G (@normed_group.to_add_comm_group F _inst_2)
  (@normed_group.to_add_comm_group G _inst_3)
[type_context.is_def_eq_detail] [13]: prod.add_comm_monoid._proof_1 =?= prod.add_comm_group._proof_1
[type_context.is_def_eq_detail] [14]: add_comm_monoid α =?= add_comm_group α
[type_context.is_def_eq_detail] [15]: add_comm_monoid =?= add_comm_group
[type_context.is_def_eq_detail] on failure: add_comm_monoid =?= add_comm_group
[type_context.is_def_eq_detail] on failure: add_comm_monoid α =?= add_comm_group α
[type_context.is_def_eq_detail] on failure: prod.add_comm_monoid._proof_1 =?= prod.add_comm_group._proof_1
[type_context.is_def_eq_detail] [11]: @add_monoid.zero (F × G)
  (@prod.add_monoid F G
     (@add_comm_monoid.to_add_monoid F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_comm_monoid.to_add_monoid G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))) =?= @add_comm_group.zero (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
[type_context.is_def_eq_detail] [12]: 0 =?= @add_group.zero (F × G)
  (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
     (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))
[type_context.is_def_eq_detail] [13]: (0, 0) =?= @add_monoid.zero (F × G)
  (@prod.add_monoid F G
     (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
[type_context.is_def_eq_detail] [14]: (0, 0) =?= 0
[type_context.is_def_eq_detail] [11]: @prod.add_comm_monoid._proof_2 F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @add_comm_group.zero_add (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
[type_context.is_def_eq_detail] [12]: @prod.add_comm_monoid._proof_2 F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @prod.add_comm_group._proof_2 F G (@normed_group.to_add_comm_group F _inst_2)
  (@normed_group.to_add_comm_group G _inst_3)
[type_context.is_def_eq_detail] [13]: prod.add_comm_monoid._proof_2 =?= prod.add_comm_group._proof_2
[type_context.is_def_eq_detail] [14]: add_comm_monoid α =?= add_comm_group α
[type_context.is_def_eq_detail] [15]: add_comm_monoid =?= add_comm_group
[type_context.is_def_eq_detail] on failure: add_comm_monoid =?= add_comm_group
[type_context.is_def_eq_detail] on failure: add_comm_monoid α =?= add_comm_group α
[type_context.is_def_eq_detail] on failure: prod.add_comm_monoid._proof_2 =?= prod.add_comm_group._proof_2
[type_context.is_def_eq_detail] [13]: 0 + a = a =?= 0 + a = a
[type_context.is_def_eq_detail] [14]: 0 + a =?= 0 + a
[type_context.is_def_eq_detail] [15]: @add_semigroup.add (F × G)
  (@add_semigroup.mk (F × G)
     (@add_monoid.add (F × G)
        (@prod.add_monoid F G
           (@add_comm_monoid.to_add_monoid F
              (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
           (@add_comm_monoid.to_add_monoid G
              (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
     _)
  0
  a =?= @add_semigroup.add (F × G)
  (@add_semigroup.mk (F × G)
     (@add_group.add (F × G)
        (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
           (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
     _)
  0
  a
[type_context.is_def_eq_detail] [16]: @add_monoid.add (F × G)
  (@prod.add_monoid F G
     (@add_comm_monoid.to_add_monoid F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_comm_monoid.to_add_monoid G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  0
  a =?= @add_group.add (F × G)
  (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
     (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))
  0
  a
[type_context.is_def_eq_detail] [17]: @add_semigroup.add (F × G)
  (@prod.add_semigroup F G
     (@add_monoid.to_add_semigroup F
        (@add_comm_monoid.to_add_monoid F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
     (@add_monoid.to_add_semigroup G
        (@add_comm_monoid.to_add_monoid G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  0
  a =?= @add_monoid.add (F × G)
  (@prod.add_monoid F G
     (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
  0
  a
[type_context.is_def_eq_detail] [18]: 0 + a =?= @add_semigroup.add (F × G)
  (@prod.add_semigroup F G
     (@add_monoid.to_add_semigroup F
        (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))))
     (@add_monoid.to_add_semigroup G
        (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))))
  0
  a
[type_context.is_def_eq_detail] [19]: (λ (p q : F × G), (@prod.fst F G p + @prod.fst F G q, @prod.snd F G p + @prod.snd F G q)) 0 a =?= 0 + a
[type_context.is_def_eq_detail] after whnf_core: (@prod.fst F G 0 + @prod.fst F G a, @prod.snd F G 0 + @prod.snd F G a) =?= 0 + a
[type_context.is_def_eq_detail] [20]: (@prod.fst F G 0 + @prod.fst F G a, @prod.snd F G 0 + @prod.snd F G a) =?= (λ (p q : F × G), (@prod.fst F G p + @prod.fst F G q, @prod.snd F G p + @prod.snd F G q)) 0 a
[type_context.is_def_eq_detail] after whnf_core: (@prod.fst F G 0 + @prod.fst F G a, @prod.snd F G 0 + @prod.snd F G a) =?= (@prod.fst F G 0 + @prod.fst F G a, @prod.snd F G 0 + @prod.snd F G a)
[type_context.is_def_eq_detail] [21]: @prod.fst F G 0 + @prod.fst F G a =?= @prod.fst F G 0 + @prod.fst F G a
[type_context.is_def_eq_detail] [22]: @add_semigroup.add F
  (@add_monoid.to_add_semigroup F
     (@add_comm_monoid.to_add_monoid F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
  (@prod.fst F G 0)
  (@prod.fst F G a) =?= @add_semigroup.add F
  (@add_monoid.to_add_semigroup F
     (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))))
  (@prod.fst F G 0)
  (@prod.fst F G a)
[type_context.is_def_eq_detail] [23]: @add_monoid.add F
  (@add_comm_monoid.to_add_monoid F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
  (@prod.fst F G 0)
  (@prod.fst F G a) =?= @add_monoid.add F
  (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)))
  (@prod.fst F G 0)
  (@prod.fst F G a)
[type_context.is_def_eq_detail] [24]: @add_comm_monoid.add F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@prod.fst F G 0)
  (@prod.fst F G a) =?= @add_group.add F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)) (@prod.fst F G 0)
  (@prod.fst F G a)
[type_context.is_def_eq_detail] [25]: @add_comm_group.add F (@normed_group.to_add_comm_group F _inst_2) (@prod.fst F G 0) (@prod.fst F G a) =?= @add_comm_group.add F (@normed_group.to_add_comm_group F _inst_2) (@prod.fst F G 0) (@prod.fst F G a)
[type_context.is_def_eq_detail] [26]: @prod.fst F G 0 =?= @prod.fst F G 0
[type_context.is_def_eq_detail] [21]: @prod.snd F G 0 + @prod.snd F G a =?= @prod.snd F G 0 + @prod.snd F G a
[type_context.is_def_eq_detail] [22]: @add_semigroup.add G
  (@add_monoid.to_add_semigroup G
     (@add_comm_monoid.to_add_monoid G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  (@prod.snd F G 0)
  (@prod.snd F G a) =?= @add_semigroup.add G
  (@add_monoid.to_add_semigroup G
     (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
  (@prod.snd F G 0)
  (@prod.snd F G a)
[type_context.is_def_eq_detail] [23]: @add_monoid.add G
  (@add_comm_monoid.to_add_monoid G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
  (@prod.snd F G 0)
  (@prod.snd F G a) =?= @add_monoid.add G
  (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))
  (@prod.snd F G 0)
  (@prod.snd F G a)
[type_context.is_def_eq_detail] [24]: @add_comm_monoid.add G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@prod.snd F G 0)
  (@prod.snd F G a) =?= @add_group.add G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)) (@prod.snd F G 0)
  (@prod.snd F G a)
[type_context.is_def_eq_detail] [25]: @add_comm_group.add G (@normed_group.to_add_comm_group G _inst_3) (@prod.snd F G 0) (@prod.snd F G a) =?= @add_comm_group.add G (@normed_group.to_add_comm_group G _inst_3) (@prod.snd F G 0) (@prod.snd F G a)
[type_context.is_def_eq_detail] [26]: @prod.snd F G 0 =?= @prod.snd F G 0
[type_context.is_def_eq_detail] [11]: @prod.add_comm_monoid._proof_3 F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @add_comm_group.add_zero (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
[type_context.is_def_eq_detail] [12]: @prod.add_comm_monoid._proof_3 F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @prod.add_comm_group._proof_3 F G (@normed_group.to_add_comm_group F _inst_2)
  (@normed_group.to_add_comm_group G _inst_3)
[type_context.is_def_eq_detail] [13]: prod.add_comm_monoid._proof_3 =?= prod.add_comm_group._proof_3
[type_context.is_def_eq_detail] [14]: add_comm_monoid α =?= add_comm_group α
[type_context.is_def_eq_detail] [15]: add_comm_monoid =?= add_comm_group
[type_context.is_def_eq_detail] on failure: add_comm_monoid =?= add_comm_group
[type_context.is_def_eq_detail] on failure: add_comm_monoid α =?= add_comm_group α
[type_context.is_def_eq_detail] on failure: prod.add_comm_monoid._proof_3 =?= prod.add_comm_group._proof_3
[type_context.is_def_eq_detail] [13]: a + 0 = a =?= a + 0 = a
[type_context.is_def_eq_detail] [14]: a + 0 =?= a + 0
[type_context.is_def_eq_detail] [15]: @add_semigroup.add (F × G)
  (@add_semigroup.mk (F × G)
     (@add_monoid.add (F × G)
        (@prod.add_monoid F G
           (@add_comm_monoid.to_add_monoid F
              (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
           (@add_comm_monoid.to_add_monoid G
              (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
     _)
  a
  0 =?= @add_semigroup.add (F × G)
  (@add_semigroup.mk (F × G)
     (@add_group.add (F × G)
        (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
           (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
     _)
  a
  0
[type_context.is_def_eq_detail] [16]: @add_monoid.add (F × G)
  (@prod.add_monoid F G
     (@add_comm_monoid.to_add_monoid F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_comm_monoid.to_add_monoid G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  a
  0 =?= @add_group.add (F × G)
  (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
     (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))
  a
  0
[type_context.is_def_eq_detail] [17]: @add_semigroup.add (F × G)
  (@prod.add_semigroup F G
     (@add_monoid.to_add_semigroup F
        (@add_comm_monoid.to_add_monoid F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
     (@add_monoid.to_add_semigroup G
        (@add_comm_monoid.to_add_monoid G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  a
  0 =?= @add_monoid.add (F × G)
  (@prod.add_monoid F G
     (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
  a
  0
[type_context.is_def_eq_detail] [18]: a + 0 =?= @add_semigroup.add (F × G)
  (@prod.add_semigroup F G
     (@add_monoid.to_add_semigroup F
        (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))))
     (@add_monoid.to_add_semigroup G
        (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))))
  a
  0
[type_context.is_def_eq_detail] [19]: (λ (p q : F × G), (@prod.fst F G p + @prod.fst F G q, @prod.snd F G p + @prod.snd F G q)) a 0 =?= a + 0
[type_context.is_def_eq_detail] after whnf_core: (@prod.fst F G a + @prod.fst F G 0, @prod.snd F G a + @prod.snd F G 0) =?= a + 0
[type_context.is_def_eq_detail] [20]: (@prod.fst F G a + @prod.fst F G 0, @prod.snd F G a + @prod.snd F G 0) =?= (λ (p q : F × G), (@prod.fst F G p + @prod.fst F G q, @prod.snd F G p + @prod.snd F G q)) a 0
[type_context.is_def_eq_detail] after whnf_core: (@prod.fst F G a + @prod.fst F G 0, @prod.snd F G a + @prod.snd F G 0) =?= (@prod.fst F G a + @prod.fst F G 0, @prod.snd F G a + @prod.snd F G 0)
[type_context.is_def_eq_detail] [21]: @prod.fst F G a + @prod.fst F G 0 =?= @prod.fst F G a + @prod.fst F G 0
[type_context.is_def_eq_detail] [22]: @add_semigroup.add F
  (@add_monoid.to_add_semigroup F
     (@add_comm_monoid.to_add_monoid F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
  (@prod.fst F G a)
  (@prod.fst F G 0) =?= @add_semigroup.add F
  (@add_monoid.to_add_semigroup F
     (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))))
  (@prod.fst F G a)
  (@prod.fst F G 0)
[type_context.is_def_eq_detail] [23]: @add_monoid.add F
  (@add_comm_monoid.to_add_monoid F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
  (@prod.fst F G a)
  (@prod.fst F G 0) =?= @add_monoid.add F
  (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)))
  (@prod.fst F G a)
  (@prod.fst F G 0)
[type_context.is_def_eq_detail] [24]: @add_comm_monoid.add F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@prod.fst F G a)
  (@prod.fst F G 0) =?= @add_group.add F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)) (@prod.fst F G a)
  (@prod.fst F G 0)
[type_context.is_def_eq_detail] [21]: @prod.snd F G a + @prod.snd F G 0 =?= @prod.snd F G a + @prod.snd F G 0
[type_context.is_def_eq_detail] [22]: @add_semigroup.add G
  (@add_monoid.to_add_semigroup G
     (@add_comm_monoid.to_add_monoid G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  (@prod.snd F G a)
  (@prod.snd F G 0) =?= @add_semigroup.add G
  (@add_monoid.to_add_semigroup G
     (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
  (@prod.snd F G a)
  (@prod.snd F G 0)
[type_context.is_def_eq_detail] [23]: @add_monoid.add G
  (@add_comm_monoid.to_add_monoid G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
  (@prod.snd F G a)
  (@prod.snd F G 0) =?= @add_monoid.add G
  (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))
  (@prod.snd F G a)
  (@prod.snd F G 0)
[type_context.is_def_eq_detail] [24]: @add_comm_monoid.add G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@prod.snd F G a)
  (@prod.snd F G 0) =?= @add_group.add G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)) (@prod.snd F G a)
  (@prod.snd F G 0)
[type_context.is_def_eq_detail] [11]: @prod.add_comm_monoid._proof_4 F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @add_comm_group.add_comm (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
[type_context.is_def_eq_detail] [12]: @prod.add_comm_monoid._proof_4 F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)) =?= @prod.add_comm_group._proof_5 F G (@normed_group.to_add_comm_group F _inst_2)
  (@normed_group.to_add_comm_group G _inst_3)
[type_context.is_def_eq_detail] [13]: prod.add_comm_monoid._proof_4 =?= prod.add_comm_group._proof_5
[type_context.is_def_eq_detail] [14]: add_comm_monoid α =?= add_comm_group α
[type_context.is_def_eq_detail] [15]: add_comm_monoid =?= add_comm_group
[type_context.is_def_eq_detail] on failure: add_comm_monoid =?= add_comm_group
[type_context.is_def_eq_detail] on failure: add_comm_monoid α =?= add_comm_group α
[type_context.is_def_eq_detail] on failure: prod.add_comm_monoid._proof_4 =?= prod.add_comm_group._proof_5
[type_context.is_def_eq_detail] [8]: @distrib_mul_action.mk 𝕜 (F × G)
  (@semiring.to_monoid 𝕜
     (@ring.to_semiring 𝕜
        (@normed_ring.to_ring 𝕜
           (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
  (@add_comm_monoid.to_add_monoid (F × G)
     (@prod.add_comm_monoid F G (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  (@mul_action.mk 𝕜 (F × G)
     (@semiring.to_monoid 𝕜
        (@ring.to_semiring 𝕜
           (@normed_ring.to_ring 𝕜
              (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
     (@has_scalar.mk 𝕜 (F × G)
        (@has_scalar.smul 𝕜 (F × G)
           (@prod.has_scalar 𝕜 F G
              (@mul_action.to_has_scalar 𝕜 F
                 (@semiring.to_monoid 𝕜
                    (@ring.to_semiring 𝕜
                       (@normed_ring.to_ring 𝕜
                          (@normed_field.to_normed_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                 (@distrib_mul_action.to_mul_action 𝕜 F
                    (@semiring.to_monoid 𝕜
                       (@ring.to_semiring 𝕜
                          (@normed_ring.to_ring 𝕜
                             (@normed_field.to_normed_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                    (@add_comm_monoid.to_add_monoid F
                       (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
                    (@semimodule.to_distrib_mul_action 𝕜 F
                       (@ring.to_semiring 𝕜
                          (@normed_ring.to_ring 𝕜
                             (@normed_field.to_normed_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
                       (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
                       (@module.to_semimodule 𝕜 F
                          (@normed_ring.to_ring 𝕜
                             (@normed_field.to_normed_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
                          (@normed_group.to_add_comm_group F _inst_2)
                          (@vector_space.to_module 𝕜 F
                             (@normed_field.to_discrete_field 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                             (@normed_group.to_add_comm_group F _inst_2)
                             (@normed_space.to_vector_space 𝕜 F
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                                _inst_2
                                _inst_6))))))
              (@mul_action.to_has_scalar 𝕜 G
                 (@semiring.to_monoid 𝕜
                    (@ring.to_semiring 𝕜
                       (@normed_ring.to_ring 𝕜
                          (@normed_field.to_normed_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                 (@distrib_mul_action.to_mul_action 𝕜 G
                    (@semiring.to_monoid 𝕜
                       (@ring.to_semiring 𝕜
                          (@normed_ring.to_ring 𝕜
                             (@normed_field.to_normed_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                    (@add_comm_monoid.to_add_monoid G
                       (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
                    (@semimodule.to_distrib_mul_action 𝕜 G
                       (@ring.to_semiring 𝕜
                          (@normed_ring.to_ring 𝕜
                             (@normed_field.to_normed_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
                       (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
                       (@module.to_semimodule 𝕜 G
                          (@normed_ring.to_ring 𝕜
                             (@normed_field.to_normed_ring 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
                          (@normed_group.to_add_comm_group G _inst_3)
                          (@vector_space.to_module 𝕜 G
                             (@normed_field.to_discrete_field 𝕜
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                             (@normed_group.to_add_comm_group G _inst_3)
                             (@normed_space.to_vector_space 𝕜 G
                                (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                                _inst_3
                                _inst_7)))))))))
     _
     _)
  _
  _ =?= @distrib_mul_action.mk 𝕜 (F × G)
  (@semiring.to_monoid 𝕜
     (@ring.to_semiring 𝕜
        (@domain.to_ring 𝕜
           (@division_ring.to_domain 𝕜
              (@field.to_division_ring 𝕜
                 (@discrete_field.to_field 𝕜
                    (@normed_field.to_discrete_field 𝕜
                       (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))))
  (@add_comm_monoid.to_add_monoid (F × G)
     (@add_comm_group.to_add_comm_monoid (F × G)
        (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))))
  (@distrib_mul_action.to_mul_action 𝕜 (F × G)
     (@semiring.to_monoid 𝕜
        (@ring.to_semiring 𝕜
           (@domain.to_ring 𝕜
              (@division_ring.to_domain 𝕜
                 (@field.to_division_ring 𝕜
                    (@discrete_field.to_field 𝕜
                       (@normed_field.to_discrete_field 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))))
     (@add_comm_monoid.to_add_monoid (F × G)
        (@add_comm_group.to_add_comm_monoid (F × G)
           (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
              (@normed_group.to_add_comm_group G _inst_3))))
     (@semimodule.to_distrib_mul_action 𝕜 (F × G)
        (@ring.to_semiring 𝕜
           (@domain.to_ring 𝕜
              (@division_ring.to_domain 𝕜
                 (@field.to_division_ring 𝕜
                    (@discrete_field.to_field 𝕜
                       (@normed_field.to_discrete_field 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))))
        (@add_comm_group.to_add_comm_monoid (F × G)
           (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
              (@normed_group.to_add_comm_group G _inst_3)))
        (@module.to_semimodule 𝕜 (F × G)
           (@domain.to_ring 𝕜
              (@division_ring.to_domain 𝕜
                 (@field.to_division_ring 𝕜
                    (@discrete_field.to_field 𝕜
                       (@normed_field.to_discrete_field 𝕜
                          (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
           (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
              (@normed_group.to_add_comm_group G _inst_3))
           (@vector_space.to_module 𝕜 (F × G)
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
              (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
                 (@normed_group.to_add_comm_group G _inst_3))
              (@prod.vector_space 𝕜 F G
                 (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                 (@normed_group.to_add_comm_group F _inst_2)
                 (@normed_group.to_add_comm_group G _inst_3)
                 (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
                    _inst_6)
                 (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
                    _inst_7))))))
  _
  _
[type_context.is_def_eq_detail] [9]: @prod.semimodule._proof_3 𝕜 F G
  (@ring.to_semiring 𝕜
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
  (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@module.to_semimodule 𝕜 F
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group F _inst_2)
     (@vector_space.to_module 𝕜 F
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group F _inst_2)
        (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
           _inst_6)))
  (@module.to_semimodule 𝕜 G
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group G _inst_3)
     (@vector_space.to_module 𝕜 G
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group G _inst_3)
        (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
           _inst_7))) =?= @prod.normed_space._proof_1 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) F G _inst_2 _inst_6 _inst_3
  _inst_7
[type_context.is_def_eq_detail] [10]: prod.semimodule._proof_3 =?= prod.normed_space._proof_1
[type_context.is_def_eq_detail] [11]: Type u_3 =?= normed_field α
[type_context.is_def_eq_detail] on failure: Type u_3 =?= normed_field α
[type_context.is_def_eq_detail] on failure: prod.semimodule._proof_3 =?= prod.normed_space._proof_1
[type_context.is_def_eq_detail] [10]: (a • @prod.fst F G (p₁ + p₂), a • @prod.snd F G (p₁ + p₂)) =
  (@prod.fst F G (a • p₁) + @prod.fst F G (a • p₂), @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂)) =?= (λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a (p₁ + p₂) =
  @add_monoid.add (F × G)
    (@add_comm_monoid.to_add_monoid (F × G)
       (@add_comm_group.to_add_comm_monoid (F × G)
          (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))))
    ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁)
    ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [11]: (a • @prod.fst F G (p₁ + p₂), a • @prod.snd F G (p₁ + p₂)) =?= (λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a (p₁ + p₂)
[type_context.is_def_eq_detail] after whnf_core: (a • @prod.fst F G (p₁ + p₂), a • @prod.snd F G (p₁ + p₂)) =?= (a • @prod.fst F G (p₁ + p₂), a • @prod.snd F G (p₁ + p₂))
[type_context.is_def_eq_detail] [11]: (@prod.fst F G (a • p₁) + @prod.fst F G (a • p₂), @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂)) =?= @add_monoid.add (F × G)
  (@add_comm_monoid.to_add_monoid (F × G)
     (@add_comm_group.to_add_comm_monoid (F × G)
        (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))))
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁)
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [12]: (@prod.fst F G (a • p₁) + @prod.fst F G (a • p₂), @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂)) =?= @add_comm_monoid.add (F × G)
  (@add_comm_group.to_add_comm_monoid (F × G)
     (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3)))
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁)
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [13]: (@prod.fst F G (a • p₁) + @prod.fst F G (a • p₂), @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂)) =?= @add_comm_group.add (F × G) (@normed_group.to_add_comm_group (F × G) (@prod.normed_group F G _inst_2 _inst_3))
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁)
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [14]: (@prod.fst F G (a • p₁) + @prod.fst F G (a • p₂), @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂)) =?= @add_comm_semigroup.add (F × G)
  (@prod.add_comm_semigroup F G
     (@add_comm_monoid.to_add_comm_semigroup F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_comm_monoid.to_add_comm_semigroup G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁)
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [15]: (@prod.fst F G (a • p₁) + @prod.fst F G (a • p₂), @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂)) =?= @add_semigroup.add (F × G)
  (@prod.add_semigroup F G
     (@add_comm_semigroup.to_add_semigroup F
        (@add_comm_monoid.to_add_comm_semigroup F
           (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
     (@add_comm_semigroup.to_add_semigroup G
        (@add_comm_monoid.to_add_comm_semigroup G
           (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))))
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁)
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [16]: (@prod.fst F G (a • p₁) + @prod.fst F G (a • p₂), @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂)) =?= (λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁ +
  (λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂
[type_context.is_def_eq_detail] [17]: (@prod.fst F G (a • p₁) + @prod.fst F G (a • p₂), @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂)) =?= (λ (p q : F × G), (@prod.fst F G p + @prod.fst F G q, @prod.snd F G p + @prod.snd F G q))
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁)
  ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] after whnf_core: (@prod.fst F G (a • p₁) + @prod.fst F G (a • p₂), @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂)) =?= (@prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁) +
   @prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂),
 @prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁) +
   @prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂))
[type_context.is_def_eq_detail] [18]: @prod.fst F G (a • p₁) + @prod.fst F G (a • p₂) =?= @prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁) +
  @prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [19]: @add_semigroup.add F
  (@add_comm_semigroup.to_add_semigroup F
     (@add_comm_monoid.to_add_comm_semigroup F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
  (@prod.fst F G (a • p₁))
  (@prod.fst F G (a • p₂)) =?= @add_semigroup.add F
  (@add_comm_semigroup.to_add_semigroup F
     (@add_comm_monoid.to_add_comm_semigroup F
        (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))))
  (@prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁))
  (@prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂))
[type_context.is_def_eq_detail] [20]: @add_comm_semigroup.add F
  (@add_comm_monoid.to_add_comm_semigroup F
     (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
  (@prod.fst F G (a • p₁))
  (@prod.fst F G (a • p₂)) =?= @add_comm_semigroup.add F
  (@add_comm_monoid.to_add_comm_semigroup F
     (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
  (@prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁))
  (@prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂))
[type_context.is_def_eq_detail] [21]: @add_comm_monoid.add F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@prod.fst F G (a • p₁))
  (@prod.fst F G (a • p₂)) =?= @add_comm_monoid.add F (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁))
  (@prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂))
[type_context.is_def_eq_detail] [22]: @add_comm_group.add F (@normed_group.to_add_comm_group F _inst_2) (@prod.fst F G (a • p₁))
  (@prod.fst F G (a • p₂)) =?= @add_comm_group.add F (@normed_group.to_add_comm_group F _inst_2)
  (@prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁))
  (@prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂))
[type_context.is_def_eq_detail] [23]: @prod.fst F G (a • p₁) =?= @prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁)
[type_context.is_def_eq_detail] [23]: @prod.fst F G (a • p₂) =?= @prod.fst F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [18]: @prod.snd F G (a • p₁) + @prod.snd F G (a • p₂) =?= @prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁) +
  @prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [19]: @add_semigroup.add G
  (@add_comm_semigroup.to_add_semigroup G
     (@add_comm_monoid.to_add_comm_semigroup G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  (@prod.snd F G (a • p₁))
  (@prod.snd F G (a • p₂)) =?= @add_semigroup.add G
  (@add_comm_semigroup.to_add_semigroup G
     (@add_comm_monoid.to_add_comm_semigroup G
        (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))))
  (@prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁))
  (@prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂))
[type_context.is_def_eq_detail] [20]: @add_comm_semigroup.add G
  (@add_comm_monoid.to_add_comm_semigroup G
     (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
  (@prod.snd F G (a • p₁))
  (@prod.snd F G (a • p₂)) =?= @add_comm_semigroup.add G
  (@add_comm_monoid.to_add_comm_semigroup G
     (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
  (@prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁))
  (@prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂))
[type_context.is_def_eq_detail] [21]: @add_comm_monoid.add G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@prod.snd F G (a • p₁))
  (@prod.snd F G (a • p₂)) =?= @add_comm_monoid.add G (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁))
  (@prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂))
[type_context.is_def_eq_detail] [22]: @add_comm_group.add G (@normed_group.to_add_comm_group G _inst_3) (@prod.snd F G (a • p₁))
  (@prod.snd F G (a • p₂)) =?= @add_comm_group.add G (@normed_group.to_add_comm_group G _inst_3)
  (@prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁))
  (@prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂))
[type_context.is_def_eq_detail] [23]: @prod.snd F G (a • p₁) =?= @prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₁)
[type_context.is_def_eq_detail] [23]: @prod.snd F G (a • p₂) =?= @prod.snd F G ((λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a p₂)
[type_context.is_def_eq_detail] [9]: @prod.semimodule._proof_4 𝕜 F G
  (@ring.to_semiring 𝕜
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
  (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
  (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
  (@module.to_semimodule 𝕜 F
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group F _inst_2)
     (@vector_space.to_module 𝕜 F
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group F _inst_2)
        (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
           _inst_6)))
  (@module.to_semimodule 𝕜 G
     (@normed_ring.to_ring 𝕜
        (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
     (@normed_group.to_add_comm_group G _inst_3)
     (@vector_space.to_module 𝕜 G
        (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
        (@normed_group.to_add_comm_group G _inst_3)
        (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
           _inst_7))) =?= @prod.normed_space._proof_2 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) F G _inst_2 _inst_6 _inst_3
  _inst_7
[type_context.is_def_eq_detail] [10]: prod.semimodule._proof_4 =?= prod.normed_space._proof_2
[type_context.is_def_eq_detail] [11]: Type u_3 =?= normed_field α
[type_context.is_def_eq_detail] on failure: Type u_3 =?= normed_field α
[type_context.is_def_eq_detail] on failure: prod.semimodule._proof_4 =?= prod.normed_space._proof_2
[type_context.is_def_eq_detail] [10]: (a • @prod.fst F G 0, a • @prod.snd F G 0) = (0, 0) =?= a • 0 = 0
[type_context.is_def_eq_detail] [11]: eq =?= eq
[type_context.is_def_eq_detail] [11]: (a • @prod.fst F G 0, a • @prod.snd F G 0) =?= a • 0
[type_context.is_def_eq_detail] [12]: (a • @prod.fst F G 0, a • @prod.snd F G 0) =?= a • 0
[type_context.is_def_eq_detail] [13]: (a • @prod.fst F G 0, a • @prod.snd F G 0) =?= (λ (a : 𝕜) (p : F × G), (a • @prod.fst F G p, a • @prod.snd F G p)) a 0
[type_context.is_def_eq_detail] after whnf_core: (a • @prod.fst F G 0, a • @prod.snd F G 0) =?= (a • @prod.fst F G 0, a • @prod.snd F G 0)
[type_context.is_def_eq_detail] [11]: (0, 0) =?= 0
[type_context.is_def_eq_detail] [12]: (0, 0) =?= @add_monoid.zero (F × G)
  (@add_comm_monoid.to_add_monoid (F × G)
     (@add_comm_group.to_add_comm_monoid (F × G)
        (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
           (@normed_group.to_add_comm_group G _inst_3))))
[type_context.is_def_eq_detail] [13]: (0, 0) =?= @add_comm_monoid.zero (F × G)
  (@add_comm_group.to_add_comm_monoid (F × G)
     (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2) (@normed_group.to_add_comm_group G _inst_3)))
[type_context.is_def_eq_detail] [14]: (0, 0) =?= @add_comm_group.zero (F × G)
  (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2) (@normed_group.to_add_comm_group G _inst_3))
[type_context.is_def_eq_detail] [15]: (0, 0) =?= @add_group.zero (F × G)
  (@prod.add_group F G (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2))
     (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3)))
[type_context.is_def_eq_detail] [16]: (0, 0) =?= @add_monoid.zero (F × G)
  (@prod.add_monoid F G
     (@add_group.to_add_monoid F (@add_comm_group.to_add_group F (@normed_group.to_add_comm_group F _inst_2)))
     (@add_group.to_add_monoid G (@add_comm_group.to_add_group G (@normed_group.to_add_comm_group G _inst_3))))
[type_context.is_def_eq_detail] [17]: (0, 0) =?= 0
[type_context.is_def_eq_detail] [9]: @mul_action.mk 𝕜 (F × G)
  (@semiring.to_monoid 𝕜
     (@ring.to_semiring 𝕜
        (@normed_ring.to_ring 𝕜
           (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
  (@has_scalar.mk 𝕜 (F × G)
     (@has_scalar.smul 𝕜 (F × G)
        (@prod.has_scalar 𝕜 F G
           (@mul_action.to_has_scalar 𝕜 F
              (@semiring.to_monoid 𝕜
                 (@ring.to_semiring 𝕜
                    (@normed_ring.to_ring 𝕜
                       (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
              (@distrib_mul_action.to_mul_action 𝕜 F
                 (@semiring.to_monoid 𝕜
                    (@ring.to_semiring 𝕜
                       (@normed_ring.to_ring 𝕜
                          (@normed_field.to_normed_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                 (@add_comm_monoid.to_add_monoid F
                    (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2)))
                 (@semimodule.to_distrib_mul_action 𝕜 F
                    (@ring.to_semiring 𝕜
                       (@normed_ring.to_ring 𝕜
                          (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
                    (@add_comm_group.to_add_comm_monoid F (@normed_group.to_add_comm_group F _inst_2))
                    (@module.to_semimodule 𝕜 F
                       (@normed_ring.to_ring 𝕜
                          (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
                       (@normed_group.to_add_comm_group F _inst_2)
                       (@vector_space.to_module 𝕜 F
                          (@normed_field.to_discrete_field 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                          (@normed_group.to_add_comm_group F _inst_2)
                          (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                             _inst_2
                             _inst_6))))))
           (@mul_action.to_has_scalar 𝕜 G
              (@semiring.to_monoid 𝕜
                 (@ring.to_semiring 𝕜
                    (@normed_ring.to_ring 𝕜
                       (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
              (@distrib_mul_action.to_mul_action 𝕜 G
                 (@semiring.to_monoid 𝕜
                    (@ring.to_semiring 𝕜
                       (@normed_ring.to_ring 𝕜
                          (@normed_field.to_normed_ring 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))
                 (@add_comm_monoid.to_add_monoid G
                    (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3)))
                 (@semimodule.to_distrib_mul_action 𝕜 G
                    (@ring.to_semiring 𝕜
                       (@normed_ring.to_ring 𝕜
                          (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))
                    (@add_comm_group.to_add_comm_monoid G (@normed_group.to_add_comm_group G _inst_3))
                    (@module.to_semimodule 𝕜 G
                       (@normed_ring.to_ring 𝕜
                          (@normed_field.to_normed_ring 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))
                       (@normed_group.to_add_comm_group G _inst_3)
                       (@vector_space.to_module 𝕜 G
                          (@normed_field.to_discrete_field 𝕜
                             (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
                          (@normed_group.to_add_comm_group G _inst_3)
                          (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)
                             _inst_3
                             _inst_7)))))))))
  _
  _ =?= @distrib_mul_action.to_mul_action 𝕜 (F × G)
  (@semiring.to_monoid 𝕜
     (@ring.to_semiring 𝕜
        (@domain.to_ring 𝕜
           (@division_ring.to_domain 𝕜
              (@field.to_division_ring 𝕜
                 (@discrete_field.to_field 𝕜
                    (@normed_field.to_discrete_field 𝕜
                       (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))))
  (@add_comm_monoid.to_add_monoid (F × G)
     (@add_comm_group.to_add_comm_monoid (F × G)
        (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
           (@normed_group.to_add_comm_group G _inst_3))))
  (@semimodule.to_distrib_mul_action 𝕜 (F × G)
     (@ring.to_semiring 𝕜
        (@domain.to_ring 𝕜
           (@division_ring.to_domain 𝕜
              (@field.to_division_ring 𝕜
                 (@discrete_field.to_field 𝕜
                    (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4)))))))
     (@add_comm_group.to_add_comm_monoid (F × G)
        (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
           (@normed_group.to_add_comm_group G _inst_3)))
     (@module.to_semimodule 𝕜 (F × G)
        (@domain.to_ring 𝕜
           (@division_ring.to_domain 𝕜
              (@field.to_division_ring 𝕜
                 (@discrete_field.to_field 𝕜
                    (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))))))
        (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
           (@normed_group.to_add_comm_group G _inst_3))
        (@vector_space.to_module 𝕜 (F × G)
           (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
           (@prod.add_comm_group F G (@normed_group.to_add_comm_group F _inst_2)
              (@normed_group.to_add_comm_group G _inst_3))
           (@prod.vector_space 𝕜 F G
              (@normed_field.to_discrete_field 𝕜 (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4))
              (@normed_group.to_add_comm_group F _inst_2)
              (@normed_group.to_add_comm_group G _inst_3)
              (@normed_space.to_vector_space 𝕜 F (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_2
                 _inst_6)
              (@normed_space.to_vector_space 𝕜 G (@nondiscrete_normed_field.to_normed_field 𝕜 _inst_4) _inst_3
                 _inst_7)))))
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= ?x_2 →L[?x_1] ?x_3
[type_context.is_def_eq_detail] on failure: normed_group (E →L[𝕜] F × G) =?= normed_group (?x_2 →L[?x_1] ?x_3)
[type_context.is_def_eq] normed_group (E →L[𝕜] F × G) =?= normed_group (?x_2 →L[?x_1] ?x_3) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_0 : normed_group (E →L[𝕜] F × G) := @normed_ring.to_normed_group ?x_9 ?x_10
[type_context.is_def_eq_detail] [1]: normed_group (E →L[𝕜] F × G) =?= normed_group ?x_9
[type_context.is_def_eq_detail] [2]: normed_group =?= normed_group
[type_context.is_def_eq_detail] process_assignment ?x_9 := E →L[𝕜] F × G
[type_context.is_def_eq_detail] assign: ?x_9 := E →L[𝕜] F × G
[type_context.is_def_eq] normed_group (E →L[𝕜] F × G) =?= normed_group ?x_9 ... success  (approximate mode)
[class_instances] (1) ?x_10 : normed_ring (E →L[𝕜] F × G) := @normed_field.to_normed_ring ?x_11 ?x_12
[type_context.is_def_eq_detail] [1]: normed_ring ?x_9 =?= normed_ring ?x_11
[type_context.is_def_eq_detail] [2]: normed_ring =?= normed_ring
[type_context.is_def_eq_detail] process_assignment ?x_11 := E →L[𝕜] F × G
[type_context.is_def_eq_detail] assign: ?x_11 := E →L[𝕜] F × G
[type_context.is_def_eq] normed_ring ?x_9 =?= normed_ring ?x_11 ... success  (approximate mode)
[class_instances] (2) ?x_12 : normed_field (E →L[𝕜] F × G) := complex.normed_field
[type_context.is_def_eq_detail] [1]: normed_field ?x_11 =?= normed_field ℂ
[type_context.is_def_eq_detail] [2]: normed_field =?= normed_field
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= ℂ
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= ℂ
[type_context.is_def_eq_detail] on failure: normed_field ?x_11 =?= normed_field ℂ
[type_context.is_def_eq] normed_field ?x_11 =?= normed_field ℂ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (2) ?x_12 : normed_field (E →L[𝕜] F × G) := real.normed_field
[type_context.is_def_eq_detail] [1]: normed_field ?x_11 =?= normed_field ℝ
[type_context.is_def_eq_detail] [2]: normed_field =?= normed_field
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= ℝ
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= ℝ
[type_context.is_def_eq_detail] on failure: normed_field ?x_11 =?= normed_field ℝ
[type_context.is_def_eq] normed_field ?x_11 =?= normed_field ℝ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (2) ?x_12 : normed_field (E →L[𝕜] F × G) := @nondiscrete_normed_field.to_normed_field ?x_13 ?x_14
[type_context.is_def_eq_detail] [1]: normed_field ?x_11 =?= normed_field ?x_13
[type_context.is_def_eq_detail] [2]: normed_field =?= normed_field
[type_context.is_def_eq_detail] process_assignment ?x_13 := E →L[𝕜] F × G
[type_context.is_def_eq_detail] assign: ?x_13 := E →L[𝕜] F × G
[type_context.is_def_eq] normed_field ?x_11 =?= normed_field ?x_13 ... success  (approximate mode)
[class_instances] (3) ?x_14 : nondiscrete_normed_field (E →L[𝕜] F × G) := _inst_4
[type_context.is_def_eq_detail] [1]: nondiscrete_normed_field ?x_13 =?= nondiscrete_normed_field 𝕜
[type_context.is_def_eq_detail] [2]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= 𝕜
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= 𝕜
[type_context.is_def_eq_detail] on failure: nondiscrete_normed_field ?x_13 =?= nondiscrete_normed_field 𝕜
[type_context.is_def_eq] nondiscrete_normed_field ?x_13 =?= nondiscrete_normed_field 𝕜 ... failed  (approximate mode)
failed is_def_eq
[class_instances] (3) ?x_14 : nondiscrete_normed_field (E →L[𝕜] F × G) := complex.nondiscrete_normed_field
[type_context.is_def_eq_detail] [1]: nondiscrete_normed_field ?x_13 =?= nondiscrete_normed_field ℂ
[type_context.is_def_eq_detail] [2]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= ℂ
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= ℂ
[type_context.is_def_eq_detail] on failure: nondiscrete_normed_field ?x_13 =?= nondiscrete_normed_field ℂ
[type_context.is_def_eq] nondiscrete_normed_field ?x_13 =?= nondiscrete_normed_field ℂ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (3) ?x_14 : nondiscrete_normed_field (E →L[𝕜] F × G) := real.nondiscrete_normed_field
[type_context.is_def_eq_detail] [1]: nondiscrete_normed_field ?x_13 =?= nondiscrete_normed_field ℝ
[type_context.is_def_eq_detail] [2]: nondiscrete_normed_field =?= nondiscrete_normed_field
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= ℝ
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= ℝ
[type_context.is_def_eq_detail] on failure: nondiscrete_normed_field ?x_13 =?= nondiscrete_normed_field ℝ
[type_context.is_def_eq] nondiscrete_normed_field ?x_13 =?= nondiscrete_normed_field ℝ ... failed  (approximate mode)
failed is_def_eq
[class_instances] (1) ?x_10 : normed_ring (E →L[𝕜] F × G) := @prod.normed_ring ?x_11 ?x_12 ?x_13 ?x_14
[type_context.is_def_eq_detail] [1]: normed_ring ?x_9 =?= normed_ring (?x_11 × ?x_12)
[type_context.is_def_eq_detail] [2]: normed_ring =?= normed_ring
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= ?x_11 × ?x_12
[type_context.is_def_eq_detail] [3]: continuous_linear_map =?= prod
[type_context.is_def_eq_detail] on failure: continuous_linear_map =?= prod
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= ?x_11 × ?x_12
[type_context.is_def_eq_detail] on failure: normed_ring ?x_9 =?= normed_ring (?x_11 × ?x_12)
[type_context.is_def_eq] normed_ring ?x_9 =?= normed_ring (?x_11 × ?x_12) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_0 : normed_group (E →L[𝕜] F × G) := @fintype.normed_group ?x_1 ?x_2 ?x_3 ?x_4
[type_context.is_def_eq_detail] [1]: normed_group (E →L[𝕜] F × G) =?= normed_group (Π (b : ?x_1), ?x_2 b)
[type_context.is_def_eq_detail] [2]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= Π (b : ?x_1), ?x_2 b
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= Π (b : ?x_1), ?x_2 b
[type_context.is_def_eq_detail] on failure: normed_group (E →L[𝕜] F × G) =?= normed_group (Π (b : ?x_1), ?x_2 b)
[type_context.is_def_eq] normed_group (E →L[𝕜] F × G) =?= normed_group (Π (b : ?x_1), ?x_2 b) ... failed  (approximate mode)
failed is_def_eq
[class_instances] (0) ?x_0 : normed_group (E →L[𝕜] F × G) := @prod.normed_group ?x_5 ?x_6 ?x_7 ?x_8
[type_context.is_def_eq_detail] [1]: normed_group (E →L[𝕜] F × G) =?= normed_group (?x_5 × ?x_6)
[type_context.is_def_eq_detail] [2]: normed_group =?= normed_group
[type_context.is_def_eq_detail] [2]: E →L[𝕜] F × G =?= ?x_5 × ?x_6
[type_context.is_def_eq_detail] [3]: continuous_linear_map =?= prod
[type_context.is_def_eq_detail] on failure: continuous_linear_map =?= prod
[type_context.is_def_eq_detail] on failure: E →L[𝕜] F × G =?= ?x_5 × ?x_6
[type_context.is_def_eq_detail] on failure: normed_group (E →L[𝕜] F × G) =?= normed_group (?x_5 × ?x_6)
[type_context.is_def_eq] normed_group (E →L[𝕜] F × G) =?= normed_group (?x_5 × ?x_6) ... failed  (approximate mode)
failed is_def_eq