Skip to content

Instantly share code, notes, and snippets.

@b-mehta

b-mehta/is_def_eq_detail trace

Created May 2, 2020 13:36
Show Gist options
  • Save b-mehta/88525a9eb2c41c23e414d9bb30c650fb to your computer and use it in GitHub Desktop.
Save b-mehta/88525a9eb2c41c23e414d9bb30c650fb to your computer and use it in GitHub Desktop.
Download ZIP
Raw
is_def_eq_detail trace
[type_context.is_def_eq_detail] [1]: Ω C ⟶ Ω C =?= Ω C ⟶ Ω C
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω C
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_ C) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_ C =?= ⊤_ C
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal C =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits C =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω C
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_ C) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_ C =?= ⊤_ C
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal C =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits C =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [2]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [1]: Ω C ⟶ Ω C =?= Ω C ⟶ Ω C
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω C
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_ C) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_ C =?= ⊤_ C
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal C =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits C =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω C
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_ C) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_ C =?= ⊤_ C
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal C =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits C =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [2]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] process_assignment ?m_1 := C
[type_context.is_def_eq_detail] assign: ?m_1 := C
[type_context.is_def_eq_detail] process_assignment ?m_1 := 𝒞
[type_context.is_def_eq_detail] [1]: category ?m_1 =?= category C
[type_context.is_def_eq_detail] [2]: category =?= category
[type_context.is_def_eq_detail] assign: ?m_1 := 𝒞
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_1
[type_context.is_def_eq_detail] [1]: has_finite_limits ?m_1 =?= has_finite_limits C
[type_context.is_def_eq_detail] [2]: has_finite_limits =?= has_finite_limits
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_2
[type_context.is_def_eq_detail] [1]: has_power_objects ?m_1 =?= has_power_objects C
[type_context.is_def_eq_detail] [2]: has_power_objects =?= has_power_objects
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_2
[type_context.is_def_eq_detail] [1]: Ω C ⟶ Ω C =?= Ω ?m_1 ⟶ Ω ?m_1
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω ?m_1
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_ C) =?= has_power_objects.has_power_object (⊤_?m_1)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_ C =?= ⊤_?m_1
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal C =?= category_theory.limits.has_terminal ?m_1
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits C =?= limits.has_finite_products_of_has_finite_limits ?m_1
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω ?m_1
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_ C) =?= has_power_objects.has_power_object (⊤_?m_1)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_ C =?= ⊤_?m_1
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal C =?= category_theory.limits.has_terminal ?m_1
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits C =?= limits.has_finite_products_of_has_finite_limits ?m_1
[type_context.is_def_eq_detail] [2]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [1]: Ω C ⟶ Ω C =?= Ω ?m_1 ⟶ Ω ?m_1
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω ?m_1
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_ C) =?= has_power_objects.has_power_object (⊤_?m_1)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_ C =?= ⊤_?m_1
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal C =?= category_theory.limits.has_terminal ?m_1
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits C =?= limits.has_finite_products_of_has_finite_limits ?m_1
[type_context.is_def_eq_detail] [2]: Ω C =?= Ω ?m_1
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_ C) =?= has_power_objects.has_power_object (⊤_?m_1)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_ C =?= ⊤_?m_1
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal C =?= category_theory.limits.has_terminal ?m_1
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits C =?= limits.has_finite_products_of_has_finite_limits ?m_1
[type_context.is_def_eq_detail] [2]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] process_assignment ?m_1 := j
[type_context.is_def_eq_detail] [1]: Ω ?m_1 ⟶ Ω ?m_1 =?= Ω C ⟶ Ω C
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: Ω ?m_1 =?= Ω C
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_?m_1) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_?m_1 =?= ⊤_ C
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal ?m_1 =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits ?m_1 =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [2]: Ω ?m_1 =?= Ω C
[type_context.is_def_eq_detail] [3]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [4]: has_power_objects.has_power_object (⊤_?m_1) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [5]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [5]: ⊤_?m_1 =?= ⊤_ C
[type_context.is_def_eq_detail] [6]: category_theory.limits.has_terminal ?m_1 =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [7]: limits.has_finite_products_of_has_finite_limits ?m_1 =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [2]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] assign: ?m_1 := j
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_3
[type_context.is_def_eq_detail] [1]: topology ?m_1 ?m_5 =?= topology C j
[type_context.is_def_eq_detail] [2]: topology =?= topology
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_3
[type_context.is_def_eq_detail] [1]: sheaf C j =?= sheaf' ?m_1 ?m_5
[type_context.is_def_eq_detail] unfold left: sheaf
[type_context.is_def_eq_detail] [2]: induced_category C (forget_sheaf C j) =?= sheaf' ?m_1 ?m_5
[type_context.is_def_eq_detail] unfold left: category_theory.induced_category
[type_context.is_def_eq_detail] [3]: sheaf' C j =?= sheaf' ?m_1 ?m_5
[type_context.is_def_eq_detail] [4]: sheaf' =?= sheaf'
[type_context.is_def_eq_detail] process_assignment ?m_1 := C
[type_context.is_def_eq_detail] assign: ?m_1 := C
[type_context.is_def_eq_detail] process_assignment ?m_1 := 𝒞
[type_context.is_def_eq_detail] [4]: category ?m_1 =?= category C
[type_context.is_def_eq_detail] [5]: category =?= category
[type_context.is_def_eq_detail] assign: ?m_1 := 𝒞
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_1
[type_context.is_def_eq_detail] [4]: has_finite_limits ?m_1 =?= has_finite_limits C
[type_context.is_def_eq_detail] [5]: has_finite_limits =?= has_finite_limits
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_2
[type_context.is_def_eq_detail] [4]: has_power_objects ?m_1 =?= has_power_objects C
[type_context.is_def_eq_detail] [5]: has_power_objects =?= has_power_objects
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := j
[type_context.is_def_eq_detail] [4]: Ω ?m_1 ⟶ Ω ?m_1 =?= Ω C ⟶ Ω C
[type_context.is_def_eq_detail] [5]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [5]: Ω ?m_1 =?= Ω C
[type_context.is_def_eq_detail] [6]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [7]: has_power_objects.has_power_object (⊤_?m_1) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [8]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [8]: ⊤_?m_1 =?= ⊤_ C
[type_context.is_def_eq_detail] [9]: category_theory.limits.has_terminal ?m_1 =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [10]: limits.has_finite_products_of_has_finite_limits ?m_1 =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [5]: Ω ?m_1 =?= Ω C
[type_context.is_def_eq_detail] [6]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [7]: has_power_objects.has_power_object (⊤_?m_1) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [8]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [8]: ⊤_?m_1 =?= ⊤_ C
[type_context.is_def_eq_detail] [9]: category_theory.limits.has_terminal ?m_1 =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [10]: limits.has_finite_products_of_has_finite_limits ?m_1 =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [5]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [6]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [7]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] assign: ?m_1 := j
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_3
[type_context.is_def_eq_detail] [4]: topology ?m_1 ?m_5 =?= topology C j
[type_context.is_def_eq_detail] [5]: topology =?= topology
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := C
[type_context.is_def_eq_detail] assign: ?m_1 := C
[type_context.is_def_eq_detail] process_assignment ?m_1 := 𝒞
[type_context.is_def_eq_detail] [1]: category ?m_1 =?= category C
[type_context.is_def_eq_detail] [2]: category =?= category
[type_context.is_def_eq_detail] assign: ?m_1 := 𝒞
[type_context.is_def_eq_detail] process_assignment ?m_1 := limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [1]: has_finite_products ?m_1 =?= has_finite_products C
[type_context.is_def_eq_detail] [2]: has_finite_products =?= has_finite_products
[type_context.is_def_eq_detail] assign: ?m_1 := limits.has_finite_products_of_has_finite_limits C
[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] [1]: sheaf C j =?= sheaf' ?m_1 ?m_5
[type_context.is_def_eq_detail] unfold left: sheaf
[type_context.is_def_eq_detail] [2]: induced_category C (forget_sheaf C j) =?= sheaf' ?m_1 ?m_5
[type_context.is_def_eq_detail] unfold left: category_theory.induced_category
[type_context.is_def_eq_detail] [3]: sheaf' C j =?= sheaf' ?m_1 ?m_5
[type_context.is_def_eq_detail] [4]: sheaf' =?= sheaf'
[type_context.is_def_eq_detail] process_assignment ?m_1 := C
[type_context.is_def_eq_detail] assign: ?m_1 := C
[type_context.is_def_eq_detail] process_assignment ?m_1 := 𝒞
[type_context.is_def_eq_detail] [4]: category ?m_1 =?= category C
[type_context.is_def_eq_detail] [5]: category =?= category
[type_context.is_def_eq_detail] assign: ?m_1 := 𝒞
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_1
[type_context.is_def_eq_detail] [4]: has_finite_limits ?m_1 =?= has_finite_limits C
[type_context.is_def_eq_detail] [5]: has_finite_limits =?= has_finite_limits
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_2
[type_context.is_def_eq_detail] [4]: has_power_objects ?m_1 =?= has_power_objects C
[type_context.is_def_eq_detail] [5]: has_power_objects =?= has_power_objects
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := j
[type_context.is_def_eq_detail] [4]: Ω ?m_1 ⟶ Ω ?m_1 =?= Ω C ⟶ Ω C
[type_context.is_def_eq_detail] [5]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [5]: Ω ?m_1 =?= Ω C
[type_context.is_def_eq_detail] [6]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [7]: has_power_objects.has_power_object (⊤_?m_1) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [8]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [8]: ⊤_?m_1 =?= ⊤_ C
[type_context.is_def_eq_detail] [9]: category_theory.limits.has_terminal ?m_1 =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [10]: limits.has_finite_products_of_has_finite_limits ?m_1 =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [5]: Ω ?m_1 =?= Ω C
[type_context.is_def_eq_detail] [6]: weak_topos_has_subobj =?= weak_topos_has_subobj
[type_context.is_def_eq_detail] [7]: has_power_objects.has_power_object (⊤_?m_1) =?= has_power_objects.has_power_object (⊤_ C)
[type_context.is_def_eq_detail] [8]: has_power_objects.has_power_object =?= has_power_objects.has_power_object
[type_context.is_def_eq_detail] [8]: ⊤_?m_1 =?= ⊤_ C
[type_context.is_def_eq_detail] [9]: category_theory.limits.has_terminal ?m_1 =?= category_theory.limits.has_terminal C
[type_context.is_def_eq_detail] [10]: limits.has_finite_products_of_has_finite_limits ?m_1 =?= limits.has_finite_products_of_has_finite_limits C
[type_context.is_def_eq_detail] [5]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [6]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [7]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] assign: ?m_1 := j
[type_context.is_def_eq_detail] process_assignment ?m_1 := _inst_3
[type_context.is_def_eq_detail] [4]: topology ?m_1 ?m_5 =?= topology C j
[type_context.is_def_eq_detail] [5]: topology =?= topology
[type_context.is_def_eq_detail] assign: ?m_1 := _inst_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := s.A
[type_context.is_def_eq_detail] assign: ?m_1 := s.A
[type_context.is_def_eq_detail] process_assignment ?m_1 := is_cartesian_closed.cart_closed A
[type_context.is_def_eq_detail] [1]: exponentiable ?m_4 =?= exponentiable A
[type_context.is_def_eq_detail] [2]: exponentiable =?= exponentiable
[type_context.is_def_eq_detail] assign: ?m_1 := is_cartesian_closed.cart_closed A
[type_context.is_def_eq_detail] process_assignment ?A := A⟹s.A
[type_context.is_def_eq_detail] assign: ?A := A⟹s.A
[type_context.is_def_eq_detail] process_assignment ?m_1 := C
[type_context.is_def_eq_detail] process_assignment ?m_1 := Type u
[type_context.is_def_eq_detail] assign: ?m_1 := Type u
[type_context.is_def_eq_detail] assign: ?m_1 := C
[type_context.is_def_eq_detail] process_assignment ?m_1 := C
[type_context.is_def_eq_detail] process_assignment ?m_1 := Type u
[type_context.is_def_eq_detail] assign: ?m_1 := Type u
[type_context.is_def_eq_detail] assign: ?m_1 := C
[type_context.is_def_eq_detail] process_assignment ?m_1 := B' ⟶ B
[type_context.is_def_eq_detail] process_assignment ?m_1 := Type v
[type_context.is_def_eq_detail] assign: ?m_1 := Type v
[type_context.is_def_eq_detail] assign: ?m_1 := B' ⟶ B
[type_context.is_def_eq_detail] process_assignment ?m_1 := B' ⟶ A⟹s.A
[type_context.is_def_eq_detail] process_assignment ?m_1 := Type v
[type_context.is_def_eq_detail] assign: ?m_1 := Type v
[type_context.is_def_eq_detail] assign: ?m_1 := B' ⟶ A⟹s.A
[type_context.is_def_eq_detail] process_assignment ?m_1 := closure.dense j m
[type_context.is_def_eq_detail] process_assignment ?m_1 := Type v
[type_context.is_def_eq_detail] assign: ?m_1 := Type v
[type_context.is_def_eq_detail] assign: ?m_1 := closure.dense j m
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 537
[type_context.is_def_eq_detail] assign: ?m_1 := 537
[type_context.is_def_eq_detail] process_assignment ?m_1 := 2
[type_context.is_def_eq_detail] assign: ?m_1 := 2
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 537, column := 2}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 537, column := 2}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 537, column := 2}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 537, column := 2}
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 538
[type_context.is_def_eq_detail] assign: ?m_1 := 538
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 538, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 538, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 538, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 538, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 538
[type_context.is_def_eq_detail] assign: ?m_1 := 538
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 538
[type_context.is_def_eq_detail] assign: ?m_1 := 538
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: option name =?= interactive.parse (optional lean.parser.ident)
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [1]: option pexpr =?= interactive.parse (optional (lean.parser.tk ":" *> interactive.types.texpr))
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [1]: expr ff =?= interactive.parse (lean.parser.tk ":=" *> interactive.types.texpr)
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [2]: expr ff =?= pexpr
[type_context.is_def_eq_detail] unfold right: pexpr
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.haveI none none ``(d)
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.haveI none none ``(d)
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d)))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d)))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 539
[type_context.is_def_eq_detail] assign: ?m_1 := 539
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 539, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 539, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 539, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 539, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5})
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 537, column := 2})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5}))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 537, column := 2})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5}))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 539
[type_context.is_def_eq_detail] assign: ?m_1 := 539
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 539, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 539, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 539, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 539, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 539
[type_context.is_def_eq_detail] assign: ?m_1 := 539
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 539
[type_context.is_def_eq_detail] assign: ?m_1 := 539
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.haveI none none ``(dense_prod_map_id j A m)
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.haveI none none ``(dense_prod_map_id j A m)
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m)))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m)))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 540
[type_context.is_def_eq_detail] assign: ?m_1 := 540
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 540, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 540, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 540, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 540, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 540
[type_context.is_def_eq_detail] assign: ?m_1 := 540
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 540, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 540, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 540, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 540, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 540
[type_context.is_def_eq_detail] assign: ?m_1 := 540
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 540
[type_context.is_def_eq_detail] assign: ?m_1 := 540
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: expr ff =?= interactive.parse interactive.types.texpr
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [2]: expr ff =?= pexpr
[type_context.is_def_eq_detail] unfold right: pexpr
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation [field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation [field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation [field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation [field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation [field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation [field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation [field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation [field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_))))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))))
(has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))))
(has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)))))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 537, column := 2})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5})))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))))
(has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_))))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 537, column := 2})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5})))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))))
(has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_))))))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 541
[type_context.is_def_eq_detail] assign: ?m_1 := 541
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 541, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 541, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 541, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 541, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 541
[type_context.is_def_eq_detail] assign: ?m_1 := 541
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 541, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 541, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 541, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 541, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 541
[type_context.is_def_eq_detail] assign: ?m_1 := 541
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 543
[type_context.is_def_eq_detail] assign: ?m_1 := 543
[type_context.is_def_eq_detail] process_assignment ?m_1 := 60
[type_context.is_def_eq_detail] assign: ?m_1 := 60
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := interaction_monad.monad
[type_context.is_def_eq_detail] [1]: monad ?m_1 =?= monad (interaction_monad tactic_state)
[type_context.is_def_eq_detail] [2]: monad =?= monad
[type_context.is_def_eq_detail] [2]: tactic =?= interaction_monad tactic_state
[type_context.is_def_eq_detail] assign: ?m_1 := interaction_monad.monad
[type_context.is_def_eq_detail] process_assignment ?m_1 := interactive.interactive.executor
[type_context.is_def_eq_detail] [1]: interactive.executor ?m_1 =?= interactive.executor tactic
[type_context.is_def_eq_detail] [2]: interactive.executor =?= interactive.executor
[type_context.is_def_eq_detail] assign: ?m_1 := interactive.interactive.executor
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 541
[type_context.is_def_eq_detail] assign: ?m_1 := 541
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 541, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 541, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 541, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 541, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 541
[type_context.is_def_eq_detail] assign: ?m_1 := 541
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 541, column := 6}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 541, column := 6}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 541, column := 6}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 541, column := 6}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 541
[type_context.is_def_eq_detail] assign: ?m_1 := 541
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] process_assignment ?m_1 := 541
[type_context.is_def_eq_detail] assign: ?m_1 := 541
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] [1]: tactic.interactive.rw_rules_t =?= interactive.parse tactic.interactive.rw_rules
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [1]: interactive.loc =?= interactive.parse interactive.types.location
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := (tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := (tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none])))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none])))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 542
[type_context.is_def_eq_detail] assign: ?m_1 := 542
[type_context.is_def_eq_detail] process_assignment ?m_1 := 7
[type_context.is_def_eq_detail] assign: ?m_1 := 7
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 542, column := 7}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 542, column := 7}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 542, column := 7}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 542, column := 7}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7}))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7}))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 542
[type_context.is_def_eq_detail] assign: ?m_1 := 542
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 542, column := 6}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 542, column := 6}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 542, column := 6}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 542, column := 6}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 542
[type_context.is_def_eq_detail] assign: ?m_1 := 542
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] process_assignment ?m_1 := 542
[type_context.is_def_eq_detail] assign: ?m_1 := 542
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := (tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := (tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none])))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none])))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 543
[type_context.is_def_eq_detail] assign: ?m_1 := 543
[type_context.is_def_eq_detail] process_assignment ?m_1 := 7
[type_context.is_def_eq_detail] assign: ?m_1 := 7
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 543, column := 7}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 543, column := 7}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 543, column := 7}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 543, column := 7}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7})
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 543
[type_context.is_def_eq_detail] assign: ?m_1 := 543
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 543, column := 6}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 543, column := 6}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 543, column := 6}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 543, column := 6}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 543
[type_context.is_def_eq_detail] assign: ?m_1 := 543
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] process_assignment ?m_1 := 543
[type_context.is_def_eq_detail] assign: ?m_1 := 543
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f')
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f')
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 543 6 543 6 (tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 543 6 543 6 (tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f')))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f')))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 543
[type_context.is_def_eq_detail] assign: ?m_1 := 543
[type_context.is_def_eq_detail] process_assignment ?m_1 := 61
[type_context.is_def_eq_detail] assign: ?m_1 := 61
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 543, column := 61}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 543, column := 61}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 543, column := 61}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 543, column := 61}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61})
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61})))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61})))
[type_context.is_def_eq_detail] process_assignment ?m_1 := 543
[type_context.is_def_eq_detail] assign: ?m_1 := 543
[type_context.is_def_eq_detail] process_assignment ?m_1 := 60
[type_context.is_def_eq_detail] assign: ?m_1 := 60
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 543, column := 60}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 543, column := 60}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 543, column := 60}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 543, column := 60}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9}, symm := tt, rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60})
[type_context.is_def_eq_detail] process_assignment ?m_1 := interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))
[type_context.is_def_eq_detail] assign: ?m_1 := interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60})))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60})))
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact ``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60})))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60})))))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 544
[type_context.is_def_eq_detail] assign: ?m_1 := 544
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 544, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 544, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 544, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 544, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5})
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 541, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5}))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 541, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5}))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 544
[type_context.is_def_eq_detail] assign: ?m_1 := 544
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 544, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 544, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 544, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 544, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 544
[type_context.is_def_eq_detail] assign: ?m_1 := 544
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 544
[type_context.is_def_eq_detail] assign: ?m_1 := 544
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: tactic.list_Pi tactic.rcases_patt ⊕ ℕ =?= interactive.parse tactic.rintro_parse
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]])
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]])
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]])))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]])))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 545
[type_context.is_def_eq_detail] assign: ?m_1 := 545
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 545, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 545, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 545, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 545, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5})
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 545
[type_context.is_def_eq_detail] assign: ?m_1 := 545
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 545, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 545, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 545, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 545, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 545
[type_context.is_def_eq_detail] assign: ?m_1 := 545
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 545
[type_context.is_def_eq_detail] assign: ?m_1 := 545
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: option name =?= interactive.parse (optional lean.parser.ident)
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [1]: option pexpr =?= interactive.parse (optional (lean.parser.tk ":" *> interactive.types.texpr))
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [1]: option pexpr =?= interactive.parse (optional (lean.parser.tk ":=" *> interactive.types.texpr))
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 546
[type_context.is_def_eq_detail] assign: ?m_1 := 546
[type_context.is_def_eq_detail] process_assignment ?m_1 := 7
[type_context.is_def_eq_detail] assign: ?m_1 := 7
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 546, column := 7}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 546, column := 7}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 546, column := 7}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 546, column := 7}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7})
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7}))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7}))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7})))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7})))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 537, column := 2})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5})))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))))
(has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7}))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 537, column := 2})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5})))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))))
(has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7}))))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 546
[type_context.is_def_eq_detail] assign: ?m_1 := 546
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 546, column := 6}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 546, column := 6}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 546, column := 6}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 546, column := 6}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 546
[type_context.is_def_eq_detail] assign: ?m_1 := 546
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] process_assignment ?m_1 := 546
[type_context.is_def_eq_detail] assign: ?m_1 := 546
[type_context.is_def_eq_detail] process_assignment ?m_1 := 6
[type_context.is_def_eq_detail] assign: ?m_1 := 6
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := (tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := (tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none])))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none])))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 547
[type_context.is_def_eq_detail] assign: ?m_1 := 547
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 547, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 547, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 547, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 547, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 547
[type_context.is_def_eq_detail] assign: ?m_1 := 547
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 547, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 547, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 547, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 547, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 547
[type_context.is_def_eq_detail] assign: ?m_1 := 547
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 547
[type_context.is_def_eq_detail] assign: ?m_1 := 547
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := (tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := (tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none])))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none])))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))))
(has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none])))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))))
(has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none])))))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 548
[type_context.is_def_eq_detail] assign: ?m_1 := 548
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 548, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 548, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 548, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 548, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 548
[type_context.is_def_eq_detail] assign: ?m_1 := 548
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 548, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 548, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 548, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 548, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 548
[type_context.is_def_eq_detail] assign: ?m_1 := 548
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 548
[type_context.is_def_eq_detail] assign: ?m_1 := 548
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.congr
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.congr
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 548 4 548 4 tactic.interactive.congr
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 548 4 548 4 tactic.interactive.congr
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 548, column := 4}) (tactic.istep 548 4 548 4 tactic.interactive.congr)
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 548, column := 4}) (tactic.istep 548 4 548 4 tactic.interactive.congr)
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4}) (tactic.istep 548 4 548 4 tactic.interactive.congr))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4}) (tactic.istep 548 4 548 4 tactic.interactive.congr))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 549
[type_context.is_def_eq_detail] assign: ?m_1 := 549
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 549, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 549, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 549, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 549, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 549
[type_context.is_def_eq_detail] assign: ?m_1 := 549
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 549, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 549, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 549, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 549, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 549
[type_context.is_def_eq_detail] assign: ?m_1 := 549
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 549
[type_context.is_def_eq_detail] assign: ?m_1 := 549
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.symmetry
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.symmetry
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 549 4 549 4 tactic.interactive.symmetry
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 549 4 549 4 tactic.interactive.symmetry
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 549, column := 4}) (tactic.istep 549 4 549 4 tactic.interactive.symmetry)
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 549, column := 4}) (tactic.istep 549 4 549 4 tactic.interactive.symmetry)
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4}) (tactic.istep 549 4 549 4 tactic.interactive.symmetry))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4}) (tactic.istep 549 4 549 4 tactic.interactive.symmetry))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4}) (tactic.istep 548 4 548 4 tactic.interactive.congr)))
(has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4})
(tactic.istep 549 4 549 4 tactic.interactive.symmetry)))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4}) (tactic.istep 548 4 548 4 tactic.interactive.congr)))
(has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4})
(tactic.istep 549 4 549 4 tactic.interactive.symmetry)))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))))
(has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4})
(tactic.istep 548 4 548 4 tactic.interactive.congr)))
(has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4})
(tactic.istep 549 4 549 4 tactic.interactive.symmetry))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))))
(has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4})
(tactic.istep 548 4 548 4 tactic.interactive.congr)))
(has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4})
(tactic.istep 549 4 549 4 tactic.interactive.symmetry))))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 550
[type_context.is_def_eq_detail] assign: ?m_1 := 550
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 550, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 550, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 550, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 550, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 550
[type_context.is_def_eq_detail] assign: ?m_1 := 550
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 550, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 550, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 550, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 550, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 550
[type_context.is_def_eq_detail] assign: ?m_1 := 550
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 550
[type_context.is_def_eq_detail] assign: ?m_1 := 550
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a))
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a))))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 551
[type_context.is_def_eq_detail] assign: ?m_1 := 551
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 551, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 551, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 551, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 551, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5})
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 550, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5}))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 550, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5}))
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 551
[type_context.is_def_eq_detail] assign: ?m_1 := 551
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 551, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 551, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 551, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 551, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 551
[type_context.is_def_eq_detail] assign: ?m_1 := 551
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 551
[type_context.is_def_eq_detail] assign: ?m_1 := 551
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: option pexpr =?= interactive.parse (optional (lean.parser.tk "with" *> interactive.types.texpr))
[type_context.is_def_eq_detail] unfold right: interactive.parse
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none])
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none])
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 551 4 551 4 (tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 551 4 551 4 (tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4 (tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none])))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4 (tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none])))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 552
[type_context.is_def_eq_detail] assign: ?m_1 := 552
[type_context.is_def_eq_detail] process_assignment ?m_1 := 5
[type_context.is_def_eq_detail] assign: ?m_1 := 5
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 552, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 552, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 552, column := 5}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 552, column := 5}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4 (tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4 (tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5})
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] process_assignment ?m_1 ?m_2 := tactic ?m_3
[type_context.is_def_eq_detail] process_assignment ?m_1 := ?m_2
[type_context.is_def_eq_detail] assign: ?m_1 := ?m_2
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic
[type_context.is_def_eq_detail] assign: ?m_1 := tactic
[type_context.is_def_eq_detail] process_assignment ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: has_bind ?m_1 =?= has_bind tactic
[type_context.is_def_eq_detail] [2]: has_bind =?= has_bind
[type_context.is_def_eq_detail] assign: ?m_1 := monad.to_has_bind
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 552
[type_context.is_def_eq_detail] assign: ?m_1 := 552
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 552, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 552, column := 4}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 552, column := 4}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 552, column := 4}
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 552
[type_context.is_def_eq_detail] assign: ?m_1 := 552
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] process_assignment ?m_1 := 552
[type_context.is_def_eq_detail] assign: ?m_1 := 552
[type_context.is_def_eq_detail] process_assignment ?m_1 := 4
[type_context.is_def_eq_detail] assign: ?m_1 := 4
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic ?m_1
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.interactive.exact ``(p)
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.interactive.exact ``(p)
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq (tactic.save_info {line := 552, column := 4}) (tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p)))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq (tactic.save_info {line := 552, column := 4}) (tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p)))
[type_context.is_def_eq_detail] [1]: tactic ?m_1 =?= tactic unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := unit
[type_context.is_def_eq_detail] assign: ?m_1 := unit
[type_context.is_def_eq_detail] process_assignment ?m_1 := 553
[type_context.is_def_eq_detail] assign: ?m_1 := 553
[type_context.is_def_eq_detail] process_assignment ?m_1 := 3
[type_context.is_def_eq_detail] assign: ?m_1 := 3
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 553, column := 3}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 553, column := 3}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 553, column := 3}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 553, column := 3}
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3})
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3})
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4
(tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3}))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4
(tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3}))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4
(tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3})))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4
(tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3})))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))))
(has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4})
(tactic.istep 548 4 548 4 tactic.interactive.congr)))
(has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4})
(tactic.istep 549 4 549 4 tactic.interactive.symmetry)))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4
(tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3}))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))))
(has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4})
(tactic.istep 548 4 548 4 tactic.interactive.congr)))
(has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4})
(tactic.istep 549 4 549 4 tactic.interactive.symmetry)))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous)) (some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4
(tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3}))))
[type_context.is_def_eq_detail] process_assignment ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 537, column := 2})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5})))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))))
(has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend
(limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7})))))
(has_bind.seq
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))))
(has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4})
(tactic.istep 548 4 548 4 tactic.interactive.congr)))
(has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4})
(tactic.istep 549 4 549 4 tactic.interactive.symmetry)))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous))
(some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4
(tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3})))))
[type_context.is_def_eq_detail] assign: ?m_1 := has_bind.seq
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 537, column := 2})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 538, column := 4})
(tactic.istep 538 4 538 4 (tactic.interactive.haveI none none ``(d))))
(tactic.save_info {line := 539, column := 5})))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 539, column := 4})
(tactic.istep 539 4 539 4 (tactic.interactive.haveI none none ``(dense_prod_map_id j A m))))
(has_bind.seq (tactic.save_info {line := 540, column := 5})
(has_bind.seq (tactic.save_info {line := 540, column := 4})
(tactic.istep 540 4 540 4
(tactic.interactive.refine
``(_
(_
(_
(cchat
[field_notation
[field_notation
[field_notation (s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]]])
_))
_)))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(tactic.istep 541 4 543 60
(tactic.solve1
(interactive.executor.execute_explicit tactic
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 4})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 541, column := 6})
(tactic.istep 541 6 541 6
(tactic.interactive.rw
{rules := [{pos := {line := 541, column := 9},
symm := tt,
rule := ``(exp_transpose_natural_left)}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 542, column := 7})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 542, column := 6})
(tactic.istep 542 6 542 6
(tactic.interactive.rw
{rules := [{pos := {line := 542, column := 9},
symm := ff,
rule := ``([field_notation
[field_notation
[field_notation
(s.unique_extend
(limits.prod.map (𝟙 A) m)
(unhat f'))]]])}],
end_pos := none pos}
(interactive.loc.ns [none]))))
(tactic.save_info {line := 543, column := 7}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 543, column := 6})
(tactic.istep 543 6 543 6
(tactic.interactive.exact
``([field_notation ([field_notation (exp.adjunction _)] _ _)] f'))))
(tactic.save_info {line := 543, column := 61}))))
(tactic.save_info {line := 543, column := 60}))))))
(tactic.save_info {line := 544, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 544, column := 4})
(tactic.istep 544 4 544 4
(tactic.interactive.rintro
(sum.inl
[tactic.rcases_patt.many
[[tactic.rcases_patt.one (name.mk_string "a" name.anonymous), tactic.rcases_patt.one
(name.mk_string "ha" name.anonymous)]]]))))
(tactic.save_info {line := 545, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 545, column := 4})
(tactic.istep 545 4 545 4
(tactic.interactive.have (some (name.mk_string "z" name.anonymous))
(some ``(eq (category_struct.comp (limits.prod.map (𝟙 A) m) (unhat a)) (unhat f')))
none)))
(tactic.save_info {line := 546, column := 7})))))
(has_bind.seq
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 546, column := 6})
(tactic.istep 546 6 546 6
(tactic.interactive.rw
{rules := [{pos := {line := 546, column := 10},
symm := tt,
rule := ``(exp_transpose_natural_left_symm m a)}, {pos := {line := 546, column := 49},
symm := ff,
rule := ``(ha)}],
end_pos := some {line := 546, column := 51}}
(interactive.loc.ns [none]))))
(has_bind.seq (tactic.save_info {line := 547, column := 5})
(has_bind.seq (tactic.save_info {line := 547, column := 4})
(tactic.istep 547 4 547 4
(tactic.interactive.rw
{rules := [{pos := {line := 547, column := 7},
symm := tt,
rule := ``([field_notation
(s.unique_extend (limits.prod.map (𝟙 A) m) (unhat f'))]
(_ (unhat a) z))}],
end_pos := none pos}
(interactive.loc.ns [none]))))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 548, column := 5})
(has_bind.seq (tactic.save_info {line := 548, column := 4})
(tactic.istep 548 4 548 4 tactic.interactive.congr)))
(has_bind.seq (tactic.save_info {line := 549, column := 5})
(has_bind.seq (tactic.save_info {line := 549, column := 4})
(tactic.istep 549 4 549 4 tactic.interactive.symmetry)))))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 5})
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 550, column := 4})
(tactic.istep 550 4 550 4
(tactic.interactive.have (some (name.mk_string "p" name.anonymous))
(some ``(eq (cchat (unhat a)) a))
(some ``([field_notation ([field_notation (exp.adjunction A)] _ _)] a)))))
(tactic.save_info {line := 551, column := 5})))
(has_bind.seq
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 551, column := 4})
(tactic.istep 551 4 551 4
(tactic.interactive.change ``(eq (cchat (unhat a)) a) none (interactive.loc.ns [none]))))
(tactic.save_info {line := 552, column := 5}))
(has_bind.seq
(has_bind.seq (tactic.save_info {line := 552, column := 4})
(tactic.istep 552 4 552 4 (tactic.interactive.exact ``(p))))
(tactic.save_info {line := 553, column := 3})))))
[type_context.is_def_eq_detail] process_assignment ?m_1 := 553
[type_context.is_def_eq_detail] assign: ?m_1 := 553
[type_context.is_def_eq_detail] process_assignment ?m_1 := 2
[type_context.is_def_eq_detail] assign: ?m_1 := 2
[type_context.is_def_eq_detail] process_assignment ?m_1 := {line := 553, column := 2}
[type_context.is_def_eq_detail] assign: ?m_1 := {line := 553, column := 2}
[type_context.is_def_eq_detail] process_assignment ?m_1 := tactic.save_info {line := 553, column := 2}
[type_context.is_def_eq_detail] assign: ?m_1 := tactic.save_info {line := 553, column := 2}
[type_context.is_def_eq_detail] [1]: tactic unit =?= tactic unit
[type_context.is_def_eq_detail] [1]: B' ⟶ B =?= B' ⟶ B
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [1]: B' ⟶ A⟹s.A =?= B' ⟶ ?A
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [1]: closure.dense j m =?= closure.dense ?m_5 m
[type_context.is_def_eq_detail] [2]: closure.dense =?= closure.dense
[type_context.is_def_eq_detail] [1]: unique {f // m ≫ f = f'} =?= unique {f // m ≫ f = f'}
[type_context.is_def_eq_detail] [2]: unique =?= unique
[type_context.is_def_eq_detail] [2]: {f // m ≫ f = f'} =?= {f // m ≫ f = f'}
[type_context.is_def_eq_detail] [3]: subtype =?= subtype
[type_context.is_def_eq_detail] [3]: B ⟶ A⟹s.A =?= B ⟶ ?A
[type_context.is_def_eq_detail] [4]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [4]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [5]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [5]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [3]: m ≫ f = f' =?= m ≫ f = f'
[type_context.is_def_eq_detail] [4]: eq =?= eq
[type_context.is_def_eq_detail] [4]: m ≫ f =?= m ≫ f
[type_context.is_def_eq_detail] [5]: category_struct.comp =?= category_struct.comp
[type_context.is_def_eq_detail] [5]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: B' ⟶ A⟹s.A =?= B' ⟶ ?A
[type_context.is_def_eq_detail] [5]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [5]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [6]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [7]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [3]: B ⟶ A⟹s.A =?= B ⟶ ?A
[type_context.is_def_eq_detail] [4]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [4]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [5]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [5]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] process_assignment ?unique_extend := λ (B B' : C) (m : B' ⟶ B) (f' : B' ⟶ A⟹s.A) (d : closure.dense j m),
{to_inhabited := {default := ⟨cchat (default {f // prod.map (𝟙 A) m ≫ f = unhat f'}).val, _⟩}, uniq := _}
[type_context.is_def_eq_detail] [1]: B' ⟶ B =?= B' ⟶ B
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [1]: B' ⟶ ?A =?= B' ⟶ A⟹s.A
[type_context.is_def_eq_detail] [2]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [2]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [3]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [1]: closure.dense ?m_5 m =?= closure.dense j m
[type_context.is_def_eq_detail] [2]: closure.dense =?= closure.dense
[type_context.is_def_eq_detail] [1]: unique {f // m ≫ f = f'} =?= unique {f // m ≫ f = f'}
[type_context.is_def_eq_detail] [2]: unique =?= unique
[type_context.is_def_eq_detail] [2]: {f // m ≫ f = f'} =?= {f // m ≫ f = f'}
[type_context.is_def_eq_detail] [3]: subtype =?= subtype
[type_context.is_def_eq_detail] [3]: B ⟶ ?A =?= B ⟶ A⟹s.A
[type_context.is_def_eq_detail] [4]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [4]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [5]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [5]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [3]: m ≫ f = f' =?= m ≫ f = f'
[type_context.is_def_eq_detail] [4]: eq =?= eq
[type_context.is_def_eq_detail] [4]: m ≫ f =?= m ≫ f
[type_context.is_def_eq_detail] [5]: category_struct.comp =?= category_struct.comp
[type_context.is_def_eq_detail] [5]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [4]: B' ⟶ ?A =?= B' ⟶ A⟹s.A
[type_context.is_def_eq_detail] [5]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [5]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [6]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [7]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [3]: B ⟶ ?A =?= B ⟶ A⟹s.A
[type_context.is_def_eq_detail] [4]: has_hom.hom =?= has_hom.hom
[type_context.is_def_eq_detail] [4]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [5]: category_struct.to_has_hom =?= category_struct.to_has_hom
[type_context.is_def_eq_detail] [5]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] [6]: to_category_struct =?= to_category_struct
[type_context.is_def_eq_detail] assign: ?unique_extend := λ (B B' : C) (m : B' ⟶ B) (f' : B' ⟶ A⟹s.A) (d : closure.dense j m),
{to_inhabited := {default := ⟨cchat (default {f // prod.map (𝟙 A) m ≫ f = unhat f'}).val, _⟩}, uniq := _}
[type_context.is_def_eq_detail] [1]: sheaf' ?m_1 ?m_5 =?= sheaf C j
[type_context.is_def_eq_detail] unfold right: sheaf
[type_context.is_def_eq_detail] [2]: sheaf' ?m_1 ?m_5 =?= induced_category C (forget_sheaf C j)
[type_context.is_def_eq_detail] unfold right: category_theory.induced_category
[type_context.is_def_eq_detail] [3]: sheaf' ?m_1 ?m_5 =?= sheaf' C j
[type_context.is_def_eq_detail] [4]: sheaf' =?= sheaf'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment