awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Comma (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : F ⊣ G
A : D
s : Cone (C := CostructuredArrow F A) (Functor.empty (CostructuredArrow F A))
m :
  s.pt ⟶
    Cone.pt (J := Discrete PEmpty.{1}) (F := Functor.empty (CostructuredArrow F A))
      (asEmptyCone (CostructuredArrow.mk (h.counit.app A)))
h_1 :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫ NatTrans.app (Cone.π (asEmptyCone (CostructuredArrow.mk (h.counit.app A)))) j = s.π.app j
⊢ m =
    CostructuredArrow.homMk
      (((h.homEquiv s.pt.left A : Equiv.{v₂ + 1, v₁ + 1} (F.obj s.pt.left ⟶ A) (s.pt.left ⟶ G.obj A)) :
          (a : F.obj s.pt.left ⟶ A) → s.pt.left ⟶ G.obj A)
        s.pt.hom)
      ⋯
have h₁ : m.left =
  CommaMorphism.left
    (CostructuredArrow.homMk
      (((h.homEquiv s.pt.left A : Equiv.{v₂ + 1, v₁ + 1} (F.obj s.pt.left ⟶ A) (s.pt.left ⟶ G.obj A)) :
          (a : F.obj s.pt.left ⟶ A) → s.pt.left ⟶ G.obj A)
        s.pt.hom)
      sorry)
Tactic: apply CostructuredArrow.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₁' : Functor.{v_2, v_2, u_2, u_2} C₁ C₁
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₁'₁ : Functor.{v_2, v_2, u_2, u_2} C₁ C₁
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₁' : F₁₁' ⊣ G₁'₁
e₀₁₁' : G₁'₁ ⋙ G₁₀ ≅ G₁₀
e₁'₁ : G₁'₁ ≅ 𝟭 C₁
h : e₀₁₁' = isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor
⊢ adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ e₀₁₁' = F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor
have subst : adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ (isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor) =
  F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor
Tactic: subst h
Cleared hypotheses: e₀₁₁', h
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₁' : Functor.{v_2, v_2, u_2, u_2} C₁ C₁
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₁'₁ : Functor.{v_2, v_2, u_2, u_2} C₁ C₁
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₁' : F₁₁' ⊣ G₁'₁
e₁'₁ : G₁'₁ ≅ 𝟭 C₁
⊢ adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ (isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor) =
    F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor
have w : ∀ (X₀ : C₀),
  (adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ (isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor)).hom.app X₀ =
    (F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor).hom.app X₀
Tactic: ext X₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
F₀₀' : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
F₀'₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
G₀'₀ : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
G₁₀' : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀₀'₁ : G₁₀' ⋙ G₀'₀ ≅ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
h : e₀₀'₁ = G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor
⊢ adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ e₀₀'₁ = isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor
have subst : adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor) =
  isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor
Tactic: subst h
Cleared hypotheses: e₀₀'₁, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
F₀₀' : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
F₀'₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
G₀'₀ : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
G₁₀' : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
⊢ adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor) =
    isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor
have w : ∀ (X₀ : C₀),
  (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀
Tactic: ext X₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (hypothesis)
Goal:
C₀ : Type u_1
C₁ : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
F₀₀' : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
F₀'₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
G₀'₀ : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
G₁₀' : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀
have h₁ : F₀'₁.map ((G₀'₀ ⋙ F₀₀').map (adj₀'₁.unit.app X₀) ≫ adj₀₀'.counit.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
  F₀'₁.map (adj₀₀'.counit.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C₀) X₀) ≫ map (𝟭 C₀) (adj₀'₁.unit.app X₀))
Tactic: have h₁ := congr_map F₀'₁ (adj₀₀'.counit.naturality (adj₀'₁.unit.app X₀))
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (hypothesis)
Goal:
C₀ : Type u_1
C₁ : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
F₀₀' : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
F₀'₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
G₀'₀ : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
G₁₀' : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
h₁ :
  F₀'₁.map ((G₀'₀ ⋙ F₀₀').map (adj₀'₁.unit.app X₀) ≫ adj₀₀'.counit.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
    F₀'₁.map (adj₀₀'.counit.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C₀) X₀) ≫ map (𝟭 C₀) (adj₀'₁.unit.app X₀))
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀
have h₂ : (F₀₀' ⋙ F₀'₁).map (map (𝟭 C₀) (adj₀'₁.unit.app X₀) ≫ e₀'₀.inv.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
  (F₀₀' ⋙ F₀'₁).map (e₀'₀.inv.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C₀) X₀) ≫ G₀'₀.map (adj₀'₁.unit.app X₀))
Tactic: have h₂ := congr_map (F₀₀' ⋙ F₀'₁) (e₀'₀.inv.naturality (adj₀'₁.unit.app X₀))
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (hypothesis)
Goal:
C₀ : Type u_1
C₁ : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
F₀₀' : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
F₀'₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
G₀'₀ : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
G₁₀' : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
h₁ :
  F₀'₁.map ((G₀'₀ ⋙ F₀₀').map (adj₀'₁.unit.app X₀) ≫ adj₀₀'.counit.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
    F₀'₁.map (adj₀₀'.counit.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C₀) X₀) ≫ map (𝟭 C₀) (adj₀'₁.unit.app X₀))
h₂ :
  (F₀₀' ⋙ F₀'₁).map (map (𝟭 C₀) (adj₀'₁.unit.app X₀) ≫ e₀'₀.inv.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
    (F₀₀' ⋙ F₀'₁).map (e₀'₀.inv.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C₀) X₀) ≫ G₀'₀.map (adj₀'₁.unit.app X₀))
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀
have h₃ : F₀'₁.map (F₀₀'.map (G₀'₀.map (adj₀'₁.unit.app X₀))) ≫ F₀'₁.map (adj₀₀'.counit.app (G₁₀'.obj (F₀'₁.obj X₀))) =
  F₀'₁.map (adj₀₀'.counit.app X₀) ≫ F₀'₁.map (adj₀'₁.unit.app X₀)
Tactic: simp only [id_obj, comp_obj, Functor.id_map, Functor.comp_map, Functor.map_comp] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (hypothesis)
Goal:
C₀ : Type u_1
C₁ : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
F₀₀' : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
F₀'₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
G₀'₀ : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
G₁₀' : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
adj₀₀' : F₀₀' ⊣ G₀'₀
adj₀'₁ : F₀'₁ ⊣ G₁₀'
e₀'₀ : G₀'₀ ≅ 𝟭 C₀
X₀ : C₀
h₁ :
  F₀'₁.map ((G₀'₀ ⋙ F₀₀').map (adj₀'₁.unit.app X₀) ≫ adj₀₀'.counit.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
    F₀'₁.map (adj₀₀'.counit.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C₀) X₀) ≫ map (𝟭 C₀) (adj₀'₁.unit.app X₀))
h₂ :
  (F₀₀' ⋙ F₀'₁).map (map (𝟭 C₀) (adj₀'₁.unit.app X₀) ≫ e₀'₀.inv.app ((F₀'₁ ⋙ G₁₀').obj X₀)) =
    (F₀₀' ⋙ F₀'₁).map (e₀'₀.inv.app (obj.{v_1, v_1, u_1, u_1} (𝟭 C₀) X₀) ≫ G₀'₀.map (adj₀'₁.unit.app X₀))
h₃ :
  F₀'₁.map (F₀₀'.map (G₀'₀.map (adj₀'₁.unit.app X₀))) ≫ F₀'₁.map (adj₀₀'.counit.app (G₁₀'.obj (F₀'₁.obj X₀))) =
    F₀'₁.map (adj₀₀'.counit.app X₀) ≫ F₀'₁.map (adj₀'₁.unit.app X₀)
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀
have h₄ : F₀'₁.map (F₀₀'.map (adj₀'₁.unit.app X₀)) ≫ F₀'₁.map (F₀₀'.map (e₀'₀.inv.app (G₁₀'.obj (F₀'₁.obj X₀)))) =
  F₀'₁.map (F₀₀'.map (e₀'₀.inv.app X₀)) ≫ F₀'₁.map (F₀₀'.map (G₀'₀.map (adj₀'₁.unit.app X₀)))
Tactic: simp only [id_obj, comp_obj, Functor.id_map, Functor.comp_map, Functor.map_comp] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₁₃ : Functor.{v_2, v_4, u_2, u_4} C₁ C₃
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₃₁ : Functor.{v_4, v_2, u_4, u_2} C₃ C₁
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₁₂₃ : G₃₁ ⟶ G₃₂ ⋙ G₂₁
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
⊢ F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃) ≫ adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₁₃ ≫ whiskerRight τ₁₂₃ G₁₀)
have obtain : ∀ (τ₁₂₃ : F₁₂ ⋙ F₂₃ ⟶ F₁₃),
  F₀₁.whiskerLeft
        (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
          ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₁₃ ≫
        whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃) G₁₀)
Tactic: obtain ⟨τ₁₂₃, rfl⟩ := (conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃)).surjective τ₁₂₃
Cleared hypotheses: τ₁₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₁₃ : Functor.{v_2, v_4, u_2, u_4} C₁ C₃
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₃₁ : Functor.{v_4, v_2, u_4, u_2} C₃ C₁
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₃ : G₃₀ ⟶ G₃₁ ⋙ G₁₀
τ₁₂₃ : F₁₂ ⋙ F₂₃ ⟶ F₁₃
⊢ F₀₁.whiskerLeft
        (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
          ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃ =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₁₃ ≫
        whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃) G₁₀)
have obtain : ∀ (τ₀₁₃ : F₀₁ ⋙ F₁₃ ⟶ F₀₃),
  F₀₁.whiskerLeft
        (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
          ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃
        ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃) : (a : F₀₁ ⋙ F₁₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₁ ⋙ G₁₀) τ₀₁₃) =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (CategoryStruct.comp (Y := G₃₁ ⋙ G₁₀)
        ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃) : (a : F₀₁ ⋙ F₁₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₁ ⋙ G₁₀) τ₀₁₃)
        (whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃) G₁₀))
Tactic: obtain ⟨τ₀₁₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃)).surjective τ₀₁₃
Cleared hypotheses: τ₀₁₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₁₃ : Functor.{v_2, v_4, u_2, u_4} C₁ C₃
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₃₁ : Functor.{v_4, v_2, u_4, u_2} C₃ C₁
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
τ₁₂₃ : F₁₂ ⋙ F₂₃ ⟶ F₁₃
τ₀₁₃ : F₀₁ ⋙ F₁₃ ⟶ F₀₃
⊢ F₀₁.whiskerLeft
        (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
          ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
      adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃
        ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃) : (a : F₀₁ ⋙ F₁₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₁ ⋙ G₁₀) τ₀₁₃) =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (CategoryStruct.comp (Y := G₃₁ ⋙ G₁₀)
        ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃) : (a : F₀₁ ⋙ F₁₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₁ ⋙ G₁₀) τ₀₁₃)
        (whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃) G₁₀))
have a : Eq (α := G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
  ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
      (F₀₁.whiskerLeft
          (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃
            ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)) ≫
        adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃
          ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃) : (a : F₀₁ ⋙ F₁₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₁ ⋙ G₁₀) τ₀₁₃)) :
    G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
  ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
      (((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
          (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
        (CategoryStruct.comp (Y := G₃₁ ⋙ G₁₀)
          ((conjugateEquiv adj₀₃ (adj₀₁.comp adj₁₃) : (a : F₀₁ ⋙ F₁₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₁ ⋙ G₁₀) τ₀₁₃)
          (whiskerRight ((conjugateEquiv adj₁₃ (adj₁₂.comp adj₂₃) : (a : F₁₂ ⋙ F₂₃ ⟶ F₁₃) → G₃₁ ⟶ G₃₂ ⋙ G₂₁) τ₁₂₃)
            G₁₀))) :
    G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
Tactic: apply (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : G₂₀ ⟶ G₂₁ ⋙ G₁₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₂₃ ≫ G₃₂.whiskerLeft τ₀₁₂ ≫ (G₃₂.associator G₂₁ G₁₀).inv)
have obtain : ∀ (τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂),
  (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight
          (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂
            ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂))
          F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₂₃ ≫
        G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
          (G₃₂.associator G₂₁ G₁₀).inv)
Tactic: obtain ⟨τ₀₁₂, rfl⟩ := (conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)).surjective τ₀₁₂
Cleared hypotheses: τ₀₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₂₃ : G₃₀ ⟶ G₃₂ ⋙ G₂₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight
          (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂
            ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂))
          F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃ =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (τ₀₂₃ ≫
        G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
          (G₃₂.associator G₂₁ G₁₀).inv)
have obtain : ∀ (τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃),
  (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight
          (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂
            ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂))
          F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃
          ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃) =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
        ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
        (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
          (G₃₂.associator G₂₁ G₁₀).inv))
Tactic: obtain ⟨τ₀₂₃, rfl⟩ := (conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃)).surjective τ₀₂₃
Cleared hypotheses: τ₀₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.CompositionIso (goal)
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
F₀₁ : Functor.{v_1, v_2, u_1, u_2} C₀ C₁
F₁₂ : Functor.{v_2, v_3, u_2, u_3} C₁ C₂
F₂₃ : Functor.{v_3, v_4, u_3, u_4} C₂ C₃
F₀₂ : Functor.{v_1, v_3, u_1, u_3} C₀ C₂
F₀₃ : Functor.{v_1, v_4, u_1, u_4} C₀ C₃
G₁₀ : Functor.{v_2, v_1, u_2, u_1} C₁ C₀
G₂₁ : Functor.{v_3, v_2, u_3, u_2} C₂ C₁
G₃₂ : Functor.{v_4, v_3, u_4, u_3} C₃ C₂
G₂₀ : Functor.{v_3, v_1, u_3, u_1} C₂ C₀
G₃₀ : Functor.{v_4, v_1, u_4, u_1} C₃ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₀₃ : F₀₃ ⊣ G₃₀
τ₀₁₂ : F₀₁ ⋙ F₁₂ ⟶ F₀₂
τ₀₂₃ : F₀₂ ⋙ F₂₃ ⟶ F₀₃
⊢ (F₀₁.associator F₁₂ F₂₃).inv ≫
      whiskerRight
          (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂
            ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂))
          F₂₃ ≫
        adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃
          ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃) =
    ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
        (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
      (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
        ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
        (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
          (G₃₂.associator G₂₁ G₁₀).inv))
have a : Eq (α := G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
  ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
      ((F₀₁.associator F₁₂ F₂₃).inv ≫
        whiskerRight
            (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂
              ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂))
            F₂₃ ≫
          adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃
            ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)) :
    G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
  ((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃)) : (a : F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
      (((conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm :
          (a : G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ⋙ F₂₃ ⟶ F₀₃)
        (CategoryStruct.comp (Y := G₃₂ ⋙ G₂₀)
          ((conjugateEquiv adj₀₃ (adj₀₂.comp adj₂₃) : (a : F₀₂ ⋙ F₂₃ ⟶ F₀₃) → G₃₀ ⟶ G₃₂ ⋙ G₂₀) τ₀₂₃)
          (G₃₂.whiskerLeft ((conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂) : (a : F₀₁ ⋙ F₁₂ ⟶ F₀₂) → G₂₀ ⟶ G₂₁ ⋙ G₁₀) τ₀₁₂) ≫
            (G₃₂.associator G₂₁ G₁₀).inv))) :
    G₃₀ ⟶ (G₃₂ ⋙ G₂₁) ⋙ G₁₀)
Tactic: apply (conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).injective