trace.type_context.is_def_eq_detail output

trace.type_context.is_def_eq_detail.txt

[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Sort ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: Type ? =?= subalgebra ?m_1 ?m_2
[type_context.is_def_eq_detail] on failure: Type ? =?= subalgebra ?m_1 ?m_2
[type_context.is_def_eq] Type ? =?= subalgebra ?m_1 ?m_2 ... failed  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: subalgebra R A =?= Type ?
[type_context.is_def_eq_detail] on failure: subalgebra R A =?= Type ?
[type_context.is_def_eq] subalgebra R A =?= Type ? ... failed  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?x_2 := integral_closure R A
[type_context.is_def_eq_detail] process_assignment ?x_0 := subalgebra R A
[type_context.is_def_eq_detail] assign: ?x_0 := subalgebra R A
[type_context.is_def_eq_detail] assign: ?x_2 := integral_closure R A
[type_context.is_def_eq] ?x_2 =?= integral_closure R A ... success  (approximate mode)
[type_context.is_def_eq] ?x_0 =?= subalgebra R A ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?x_1 := coe_sort_trans
[type_context.is_def_eq_detail] [1]: has_coe_to_sort ?x_0 =?= has_coe_to_sort (subalgebra R A)
[type_context.is_def_eq_detail] [2]: has_coe_to_sort =?= has_coe_to_sort
[type_context.is_def_eq_detail] assign: ?x_1 := coe_sort_trans
[type_context.is_def_eq] ?x_1 =?= coe_sort_trans ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: has_coe_to_sort.S (subalgebra R A) =?= Type ?
[type_context.is_def_eq_detail] [2]: has_coe_to_sort.S (submodule R A) =?= Type ?
[type_context.is_def_eq_detail] [3]: has_coe_to_sort.S (set A) =?= Type ?
[type_context.is_def_eq] has_coe_to_sort.S (subalgebra R A) =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?m_1 := ↥(integral_closure R A)
[type_context.is_def_eq_detail] [1]: Type ? =?= has_coe_to_sort.S (subalgebra R A)
[type_context.is_def_eq_detail] [2]: Type ? =?= has_coe_to_sort.S (submodule R A)
[type_context.is_def_eq_detail] [3]: Type ? =?= has_coe_to_sort.S (set A)
[type_context.is_def_eq_detail] assign: ?m_1 := ↥(integral_closure R A)
[type_context.is_def_eq] ?m_1 =?= ↥(integral_closure R A) ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: integral_domain ↥(integral_closure R A) =?= integral_domain ↥?m_2
[type_context.is_def_eq_detail] [2]: integral_domain =?= integral_domain
[type_context.is_def_eq_detail] [2]: ↥(integral_closure R A) =?= ↥?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := integral_closure R A
[type_context.is_def_eq_detail] [3]: set ?m_1 =?= subalgebra R A
[type_context.is_def_eq_detail] unfold left: set
[type_context.is_def_eq_detail] [4]: ?m_1 → Prop =?= subalgebra R A
[type_context.is_def_eq_detail] on failure: ?m_1 → Prop =?= subalgebra R A
[type_context.is_def_eq_detail] Type mismatch when assigning ?m_1 := integral_closure R A
>> set ?m_1 =?= subalgebra R A
[type_context.is_def_eq_detail] unfold left&right: coe_sort
[type_context.is_def_eq_detail] [3]: has_coe_to_sort.coe (integral_closure R A) =?= has_coe_to_sort.coe ?m_2
[type_context.is_def_eq_detail] [4]: has_coe_to_sort.coe =?= has_coe_to_sort.coe
[type_context.is_def_eq_detail] process_assignment ?m_1 := integral_closure R A
[type_context.is_def_eq_detail] [4]: set ?m_1 =?= subalgebra R A
[type_context.is_def_eq_detail] unfold left: set
[type_context.is_def_eq_detail] [5]: ?m_1 → Prop =?= subalgebra R A
[type_context.is_def_eq_detail] on failure: ?m_1 → Prop =?= subalgebra R A
[type_context.is_def_eq_detail] Type mismatch when assigning ?m_1 := integral_closure R A
>> set ?m_1 =?= subalgebra R A
[type_context.is_def_eq_detail] [4]: (λ (x : subalgebra R A), ↥(has_coe_t_aux.coe (submodule R A) x)) (integral_closure R A) =?= (λ (s : set ?m_1), {x // x ∈ s}) ?m_2
[type_context.is_def_eq_detail] after whnf_core: ↥(has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] unfold left: coe_sort
[type_context.is_def_eq_detail] [5]: has_coe_to_sort.coe (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] [6]: (λ (x : submodule R A), ↥(has_coe_t_aux.coe (set A) x)) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] after whnf_core: ↥(has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))) =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] unfold left: coe_sort
[type_context.is_def_eq_detail] [7]: has_coe_to_sort.coe (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))) =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] [8]: (λ (s : set A), {x // x ∈ s}) (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))) =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] after whnf_core: {x // x ∈ has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))} =?= {x // x ∈ ?m_2}
[type_context.is_def_eq_detail] process_assignment ?m_1 := A
[type_context.is_def_eq_detail] assign: ?m_1 := A
[type_context.is_def_eq_detail] [9]: x ∈ has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= x ∈ ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] [10]: set ?m_1 =?= set A
[type_context.is_def_eq_detail] assign: ?m_1 := has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq] integral_domain ↥(integral_closure R A) =?= integral_domain ↥?m_2 ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_2
[type_context.is_def_eq_detail] [1]: integral_domain ?m_1 =?= integral_domain A
[type_context.is_def_eq_detail] [2]: integral_domain =?= integral_domain
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_2
[type_context.is_def_eq] ?m_1 =?= _inst_2 ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: set ?m_1 =?= subalgebra ?m_2 ?m_3
[type_context.is_def_eq_detail] unfold left: set
[type_context.is_def_eq_detail] [2]: ?m_1 → Prop =?= subalgebra ?m_2 ?m_3
[type_context.is_def_eq_detail] on failure: ?m_1 → Prop =?= subalgebra ?m_2 ?m_3
[type_context.is_def_eq] set ?m_1 =?= subalgebra ?m_2 ?m_3 ... failed  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq] Type ? =?= Type ? ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: subalgebra R A =?= set ?m_1
[type_context.is_def_eq_detail] unfold right: set
[type_context.is_def_eq_detail] [2]: subalgebra R A =?= ?m_1 → Prop
[type_context.is_def_eq_detail] on failure: subalgebra R A =?= ?m_1 → Prop
[type_context.is_def_eq] subalgebra R A =?= set ?m_1 ... failed  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?x_2 := integral_closure R A
[type_context.is_def_eq_detail] process_assignment ?x_0 := subalgebra R A
[type_context.is_def_eq_detail] assign: ?x_0 := subalgebra R A
[type_context.is_def_eq_detail] assign: ?x_2 := integral_closure R A
[type_context.is_def_eq] ?x_2 =?= integral_closure R A ... success  (approximate mode)
[type_context.is_def_eq] ?x_0 =?= subalgebra R A ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?x_1 := set A
[type_context.is_def_eq_detail] assign: ?x_1 := set A
[type_context.is_def_eq] ?x_1 =?= set A ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?x_0 := subalgebra R A
[type_context.is_def_eq_detail] assign: ?x_0 := subalgebra R A
[type_context.is_def_eq] ?x_0 =?= subalgebra R A ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: set A =?= set ?m_1
[type_context.is_def_eq] set A =?= set ?m_1 ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= ↑(integral_closure R A)
[type_context.is_def_eq_detail] unfold right: coe
[type_context.is_def_eq_detail] [2]: has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= lift_t (integral_closure R A)
[type_context.is_def_eq_detail] unfold right: lift_t
[type_context.is_def_eq_detail] [3]: has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= has_lift_t.lift (set A) (integral_closure R A)
[type_context.is_def_eq_detail] [4]: coe_b (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= coe_t (integral_closure R A)
[type_context.is_def_eq_detail] [5]: has_coe.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)) =?= has_coe_t.coe (set A) (integral_closure R A)
[type_context.is_def_eq_detail] [6]: (has_coe_t_aux.coe (submodule R A) (integral_closure R A)).carrier =?= coe_b (integral_closure R A)
[type_context.is_def_eq_detail] unfold right: coe_b
[type_context.is_def_eq_detail] [7]: (has_coe_t_aux.coe (submodule R A) (integral_closure R A)).carrier =?= has_coe.coe (set A) (integral_closure R A)
[type_context.is_def_eq_detail] [8]: ↑(integral_closure R A) =?= (λ (S : subalgebra R A), S.carrier) (integral_closure R A)
[type_context.is_def_eq_detail] after whnf_core: ↑(integral_closure R A) =?= (integral_closure R A).carrier
[type_context.is_def_eq_detail] unfold left: coe
[type_context.is_def_eq_detail] [9]: lift_t (integral_closure R A) =?= (integral_closure R A).carrier
[type_context.is_def_eq_detail] unfold left: lift_t
[type_context.is_def_eq_detail] [10]: has_lift_t.lift (set A) (integral_closure R A) =?= (integral_closure R A).carrier
[type_context.is_def_eq_detail] [11]: coe_t (integral_closure R A) =?= {r : A | is_integral R r}
[type_context.is_def_eq_detail] [12]: has_coe_t.coe (set A) (integral_closure R A) =?= λ (r : A), is_integral R r
[type_context.is_def_eq_detail] [13]: coe_b (integral_closure R A) =?= λ (r : A), is_integral R r
[type_context.is_def_eq_detail] unfold left: coe_b
[type_context.is_def_eq_detail] [14]: has_coe.coe (set A) (integral_closure R A) =?= λ (r : A), is_integral R r
[type_context.is_def_eq_detail] [15]: (λ (S : subalgebra R A), S.carrier) (integral_closure R A) =?= λ (r : A), is_integral R r
[type_context.is_def_eq_detail] after whnf_core: (integral_closure R A).carrier =?= λ (r : A), is_integral R r
[type_context.is_def_eq_detail] [16]: {r : A | is_integral R r} =?= λ (r : A), is_integral R r
[type_context.is_def_eq_detail] unfold left: set_of
[type_context.is_def_eq] ?m_1 =?= ↑(integral_closure R A) ... success  (approximate mode)
[type_context.is_def_eq_detail] process_assignment ?m_1 := ⁇
[type_context.is_def_eq_detail] [1]: is_subring ?m_3 =?= is_subring (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)))
[type_context.is_def_eq_detail] [2]: is_subring =?= is_subring
[type_context.is_def_eq_detail] [2]: domain.to_ring ?m_1 =?= domain.to_ring A
[type_context.is_def_eq_detail] [3]: integral_domain.to_domain =?= integral_domain.to_domain
[type_context.is_def_eq_detail] assign: ?m_1 := ⁇
[type_context.is_def_eq] ?m_1 =?= ⁇ ... success  (approximate mode)
[type_context.is_def_eq_detail] [1]: integral_domain ↥↑(integral_closure R A) =?= integral_domain ↥(integral_closure R A)
[type_context.is_def_eq_detail] [2]: integral_domain =?= integral_domain
[type_context.is_def_eq_detail] [2]: ↥↑(integral_closure R A) =?= ↥(integral_closure R A)
[type_context.is_def_eq_detail] [3]: ↑(integral_closure R A) =?= integral_closure R A
[type_context.is_def_eq_detail] unfold (reducible) left: coe
[type_context.is_def_eq_detail] [4]: lift_t (integral_closure R A) =?= integral_closure R A
[type_context.is_def_eq_detail] [5]: lift_t (integral_closure R A) =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] unfold left: lift_t
[type_context.is_def_eq_detail] [6]: has_lift_t.lift (set A) (integral_closure R A) =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] [7]: coe_t (integral_closure R A) =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] unfold left: coe_t
[type_context.is_def_eq_detail] [8]: has_coe_t.coe (set A) (integral_closure R A) =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] [9]: coe_b (integral_closure R A) =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] unfold left: coe_b
[type_context.is_def_eq_detail] [10]: has_coe.coe (set A) (integral_closure R A) =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] [11]: (λ (S : subalgebra R A), S.carrier) (integral_closure R A) =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] after whnf_core: (integral_closure R A).carrier =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] [12]: {r : A | is_integral R r} =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] unfold left: set_of
[type_context.is_def_eq_detail] [13]: λ (r : A), is_integral R r =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] on failure: λ (r : A), is_integral R r =?= {carrier := {r : A | is_integral R r}, subring := _, range_le' := _}
[type_context.is_def_eq_detail] unfold left&right: coe_sort
[type_context.is_def_eq_detail] [3]: has_coe_to_sort.coe ↑(integral_closure R A) =?= has_coe_to_sort.coe (integral_closure R A)
[type_context.is_def_eq_detail] [4]: (λ (s : set A), {x // x ∈ s}) ↑(integral_closure R A) =?= (λ (x : subalgebra R A), ↥(has_coe_t_aux.coe (submodule R A) x)) (integral_closure R A)
[type_context.is_def_eq_detail] after whnf_core: {x // x ∈ ↑(integral_closure R A)} =?= ↥(has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] unfold right: coe_sort
[type_context.is_def_eq_detail] [5]: {x // x ∈ ↑(integral_closure R A)} =?= has_coe_to_sort.coe (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] [6]: {x // x ∈ ↑(integral_closure R A)} =?= (λ (x : submodule R A), ↥(has_coe_t_aux.coe (set A) x)) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] after whnf_core: {x // x ∈ ↑(integral_closure R A)} =?= ↥(has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)))
[type_context.is_def_eq_detail] unfold right: coe_sort
[type_context.is_def_eq_detail] [7]: {x // x ∈ ↑(integral_closure R A)} =?= has_coe_to_sort.coe (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)))
[type_context.is_def_eq_detail] [8]: {x // x ∈ ↑(integral_closure R A)} =?= (λ (s : set A), {x // x ∈ s}) (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)))
[type_context.is_def_eq_detail] after whnf_core: {x // x ∈ ↑(integral_closure R A)} =?= {x // x ∈ has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))}
[type_context.is_def_eq_detail] [9]: x ∈ ↑(integral_closure R A) =?= x ∈ has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] [10]: set.mem x ↑(integral_closure R A) =?= set.mem x (has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A)))
[type_context.is_def_eq_detail] [11]: ↑(integral_closure R A) =?= has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] unfold left: coe
[type_context.is_def_eq_detail] [12]: lift_t (integral_closure R A) =?= has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] unfold left: lift_t
[type_context.is_def_eq_detail] [13]: has_lift_t.lift (set A) (integral_closure R A) =?= has_coe_t_aux.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] [14]: coe_t (integral_closure R A) =?= coe_b (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] [15]: has_coe_t.coe (set A) (integral_closure R A) =?= has_coe.coe (set A) (has_coe_t_aux.coe (submodule R A) (integral_closure R A))
[type_context.is_def_eq_detail] [16]: coe_b (integral_closure R A) =?= (has_coe_t_aux.coe (submodule R A) (integral_closure R A)).carrier
[type_context.is_def_eq_detail] unfold left: coe_b
[type_context.is_def_eq_detail] [17]: has_coe.coe (set A) (integral_closure R A) =?= (has_coe_t_aux.coe (submodule R A) (integral_closure R A)).carrier
[type_context.is_def_eq_detail] [18]: (λ (S : subalgebra R A), S.carrier) (integral_closure R A) =?= ↑(integral_closure R A)
[type_context.is_def_eq_detail] after whnf_core: (integral_closure R A).carrier =?= ↑(integral_closure R A)
[type_context.is_def_eq_detail] unfold right: coe
[type_context.is_def_eq_detail] [19]: (integral_closure R A).carrier =?= lift_t (integral_closure R A)
[type_context.is_def_eq_detail] unfold right: lift_t
[type_context.is_def_eq_detail] [20]: (integral_closure R A).carrier =?= has_lift_t.lift (set A) (integral_closure R A)
[type_context.is_def_eq_detail] [21]: {r : A | is_integral R r} =?= coe_t (integral_closure R A)
[type_context.is_def_eq_detail] [22]: λ (r : A), is_integral R r =?= has_coe_t.coe (set A) (integral_closure R A)
[type_context.is_def_eq_detail] [23]: λ (r : A), is_integral R r =?= coe_b (integral_closure R A)
[type_context.is_def_eq_detail] unfold right: coe_b
[type_context.is_def_eq_detail] [24]: λ (r : A), is_integral R r =?= has_coe.coe (set A) (integral_closure R A)
[type_context.is_def_eq_detail] [25]: λ (r : A), is_integral R r =?= (λ (S : subalgebra R A), S.carrier) (integral_closure R A)
[type_context.is_def_eq_detail] after whnf_core: λ (r : A), is_integral R r =?= (integral_closure R A).carrier
[type_context.is_def_eq_detail] [26]: λ (r : A), is_integral R r =?= {r : A | is_integral R r}
[type_context.is_def_eq_detail] unfold right: set_of
[type_context.is_def_eq] integral_domain ↥↑(integral_closure R A) =?= integral_domain ↥(integral_closure R A) ... success  (approximate mode)