awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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
inst_2 : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A)
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ CostructuredArrow.hom (⊤_ CostructuredArrow G A))
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g ⋯
⊢ terminal.from B' = g'

Tactic:
have : terminal.from _ = g' := by cat_disch
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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
inst_2 : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A)
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ CostructuredArrow.hom (⊤_ CostructuredArrow G A))
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g ⋯
this : terminal.from B' = g'
change : CommaMorphism.left (terminal.from B') = g
⊢ (fun (g : G.obj B ⟶ A) ↦
        (CommaMorphism.left (terminal.from (CostructuredArrow.mk g)) :
          (CostructuredArrow.mk g).left ⟶
            Comma.left.{v₂, 0, v₁, u₂, 0, u₁} (B := Discrete PUnit.{1}) (T := C) (L := G) (R := Functor.fromPUnit A)
              (⊤_ CostructuredArrow G A)))
      ((fun (g : B ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A)) ↦
          G.map g ≫ CostructuredArrow.hom (⊤_ CostructuredArrow G A))
        g) =
    g

Tactic:
change CommaMorphism.left (terminal.from B') = _

Premises used: CategoryTheory.Limits.terminal.from, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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
inst_2 : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A)
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ CostructuredArrow.hom (⊤_ CostructuredArrow G A))
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g ⋯
this : terminal.from B' = g'
rw : g'.left = g
⊢ CommaMorphism.left (terminal.from B') = g

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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
inst_2 : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B : D
A : C
g : B ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A)
B' : CostructuredArrow G A := CostructuredArrow.mk (G.map g ≫ CostructuredArrow.hom (⊤_ CostructuredArrow G A))
g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g ⋯
this : terminal.from B' = g'
⊢ g'.left = g

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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
inst_2 : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
rw :
  G.map f ≫ g =
    ((Equiv.symm (rightAdjointOfCostructuredArrowTerminalsAux G B₁ A) :
          Equiv.{v₂ + 1, v₁ + 1}
            (B₁ ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A))
            (G.obj B₁ ⟶ A)) :
        (a : B₁ ⟶ (⊤_ CostructuredArrow G A).left) → G.obj B₁ ⟶ A)
      (f ≫
        ((rightAdjointOfCostructuredArrowTerminalsAux G B₂ A :
              Equiv.{v₁ + 1, v₂ + 1} (G.obj B₂ ⟶ A)
                (B₂ ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A))) :
            (a : G.obj B₂ ⟶ A) → B₂ ⟶ (⊤_ CostructuredArrow G A).left)
          g)
⊢ Eq.{v₂ + 1} (α := B₁ ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A))
    (((rightAdjointOfCostructuredArrowTerminalsAux G B₁ A :
            Equiv.{v₁ + 1, v₂ + 1} (G.obj B₁ ⟶ A)
              (B₁ ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A))) :
          (a : G.obj B₁ ⟶ A) → B₁ ⟶ (⊤_ CostructuredArrow G A).left)
        (G.map f ≫ g) :
      B₁ ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A))
    (f ≫
        ((rightAdjointOfCostructuredArrowTerminalsAux G B₂ A :
              Equiv.{v₁ + 1, v₂ + 1} (G.obj B₂ ⟶ A)
                (B₂ ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A))) :
            (a : G.obj B₂ ⟶ A) → B₂ ⟶ (⊤_ CostructuredArrow G A).left)
          g :
      B₁ ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A))

Tactic:
rw [← Equiv.eq_symm_apply]

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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
inst_2 : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
⊢ G.map f ≫ g =
    ((Equiv.symm (rightAdjointOfCostructuredArrowTerminalsAux G B₁ A) :
          Equiv.{v₂ + 1, v₁ + 1}
            (B₁ ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A))
            (G.obj B₁ ⟶ A)) :
        (a : B₁ ⟶ (⊤_ CostructuredArrow G A).left) → G.obj B₁ ⟶ A)
      (f ≫
        ((rightAdjointOfCostructuredArrowTerminalsAux G B₂ A :
              Equiv.{v₁ + 1, v₂ + 1} (G.obj B₂ ⟶ A)
                (B₂ ⟶ CostructuredArrow.left.{v₂, v₁, u₂, u₁} (D := C) (S := G) (T := A) (⊤_ CostructuredArrow G A))) :
            (a : G.obj B₂ ⟶ A) → B₂ ⟶ (⊤_ CostructuredArrow G A).left)
          g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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 : C
s : Cocone (C := StructuredArrow A G) (Functor.empty (StructuredArrow A G))
m :
  Cocone.pt (J := Discrete PEmpty.{1}) (F := Functor.empty (StructuredArrow A G))
      (asEmptyCocone (StructuredArrow.mk (h.unit.app A))) ⟶
    s.pt
h_1 :
  ∀ (j : Discrete PEmpty.{1}),
    NatTrans.app (Cocone.ι (asEmptyCocone (StructuredArrow.mk (h.unit.app A)))) j ≫ m = s.ι.app j
a :
  StructuredArrow.Hom.right m =
    StructuredArrow.Hom.right
      (StructuredArrow.homMk
        (((Equiv.symm (h.homEquiv A s.pt.right) :
              Equiv.{v₁ + 1, v₂ + 1} (A ⟶ G.obj s.pt.right) (F.obj A ⟶ s.pt.right)) :
            (a : A ⟶ G.obj s.pt.right) → F.obj A ⟶ s.pt.right)
          s.pt.hom)
        ⋯)
⊢ m =
    StructuredArrow.homMk
      (((Equiv.symm (h.homEquiv A s.pt.right) : Equiv.{v₁ + 1, v₂ + 1} (A ⟶ G.obj s.pt.right) (F.obj A ⟶ s.pt.right)) :
          (a : A ⟶ G.obj s.pt.right) → F.obj A ⟶ s.pt.right)
        s.pt.hom)
      ⋯

Tactic:
apply StructuredArrow.ext

Premises used: CategoryTheory.StructuredArrow.ext
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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 : C
s : Cocone (C := StructuredArrow A G) (Functor.empty (StructuredArrow A G))
m :
  Cocone.pt (J := Discrete PEmpty.{1}) (F := Functor.empty (StructuredArrow A G))
      (asEmptyCocone (StructuredArrow.mk (h.unit.app A))) ⟶
    s.pt
h_1 :
  ∀ (j : Discrete PEmpty.{1}),
    NatTrans.app (Cocone.ι (asEmptyCocone (StructuredArrow.mk (h.unit.app A)))) j ≫ m = s.ι.app j
⊢ StructuredArrow.Hom.right m =
    StructuredArrow.Hom.right
      (StructuredArrow.homMk
        (((Equiv.symm (h.homEquiv A s.pt.right) :
              Equiv.{v₁ + 1, v₂ + 1} (A ⟶ G.obj s.pt.right) (F.obj A ⟶ s.pt.right)) :
            (a : A ⟶ G.obj s.pt.right) → F.obj A ⟶ s.pt.right)
          s.pt.hom)
        ⋯)

Tactic:
simp [← StructuredArrow.w m]

Premises used: CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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
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)
        ⋯)
⊢ 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)
      ⋯

Tactic:
apply CostructuredArrow.ext

Premises used: CategoryTheory.CostructuredArrow.ext
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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.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)
        ⋯)

Tactic:
simp [← CostructuredArrow.w m]

Premises used: CategoryTheory.CostructuredArrow.w
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
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
⊢ G.IsRightAdjoint ↔ ∀ (A : C), HasInitial (StructuredArrow A G)

Tactic:
⟨fun _ A => (mkInitialOfLeftAdjoint _ (Adjunction.ofIsRightAdjoint G) A).hasInitial,
    fun _ => isRightAdjointOfStructuredArrowInitials _⟩

Premises used: CategoryTheory.isRightAdjointOfStructuredArrowInitials, CategoryTheory.Limits.IsInitial.hasInitial, Iff.intro, CategoryTheory.Adjunction.ofIsRightAdjoint, CategoryTheory.mkInitialOfLeftAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.Comma
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ F.IsLeftAdjoint ↔ ∀ (A : D), HasTerminal (CostructuredArrow F A)

Tactic:
⟨fun _ A => (mkTerminalOfRightAdjoint _ (Adjunction.ofIsLeftAdjoint F) A).hasTerminal,
    fun _ => isLeftAdjoint_of_costructuredArrowTerminals _⟩

Premises used: CategoryTheory.Adjunction.ofIsLeftAdjoint, CategoryTheory.isLeftAdjoint_of_costructuredArrowTerminals, Iff.intro, CategoryTheory.Limits.IsTerminal.hasTerminal, CategoryTheory.Functor.rightAdjoint, CategoryTheory.mkTerminalOfRightAdjoint
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
Goal:
C₀ : Type u_1
inst : Category.{v_1, u_1} C₀
F G : Functor.{v_1, v_1, u_1, u_1} C₀ C₀
adj : F ⊣ G
e : G ≅ 𝟭 C₀
⊢ (conjugateEquiv id adj : (a : F ⟶ 𝟭 C₀) → 𝟭 C₀ ⟶ G) (adj.leftAdjointIdIso e).hom = e.inv

Tactic:
simp [leftAdjointIdIso]

Premises used: CategoryTheory.Adjunction.leftAdjointIdIso
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} 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_1, v_3, u_1, u_3} 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_3, v_1, u_3, u_1} C₂ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₀₂ : F₀₂ ⊣ G₂₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
⊢ (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).hom = adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ e₀₁₂.inv

Tactic:
rfl

Premises used: CategoryTheory.Adjunction.leftAdjointCompNatTrans, rfl
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
Goal:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} 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_1, v_3, u_1, u_3} 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_3, v_1, u_3, u_1} C₂ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₀₂ : F₀₂ ⊣ G₂₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
⊢ (conjugateEquiv (adj₀₁.comp adj₁₂) adj₀₂ : (a : F₀₂ ⟶ F₀₁ ⋙ F₁₂) → G₂₁ ⋙ G₁₀ ⟶ G₂₀)
      (Iso.inv
        (((conjugateIsoEquiv adj₀₂ (adj₀₁.comp adj₁₂)).symm : (a : G₂₀ ≅ G₂₁ ⋙ G₁₀) → F₀₁ ⋙ F₁₂ ≅ F₀₂) e₀₁₂.symm)) =
    e₀₁₂.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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
subst :
  adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ (isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor) =
    F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor
⊢ adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ e₀₁₁' = F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₁
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₀
⊢ adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ (isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor) =
    F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor

Tactic:
ext X₀
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₁
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:
simp [leftAdjointCompIso_hom_app, leftAdjointIdIso_hom_app,
    ← Functor.map_comp_assoc, -Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Adjunction.leftAdjointCompIso_hom_app, CategoryTheory.Adjunction.leftAdjointIdIso_hom_app
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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
subst :
  adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor) =
    isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor
⊢ adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ e₀₀'₁ = isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₀
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₀
⊢ adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor) =
    isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor

Tactic:
ext X₀
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₀
⊢ 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₀))
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₀))
⊢ (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₀))
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₀))
⊢ 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₂

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.id_map, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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₀)
⊢ 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₂

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.id_map, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Adjunction.CompositionIso
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 (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₀)
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₀)))
⊢ (adj₀₀'.leftAdjointCompIso adj₀'₁ adj₀'₁ (G₁₀'.isoWhiskerLeft e₀'₀ ≪≫ G₁₀'.rightUnitor)).hom.app X₀ =
    (isoWhiskerRight (adj₀₀'.leftAdjointIdIso e₀'₀) F₀'₁ ≪≫ F₀'₁.leftUnitor).hom.app X₀

Tactic:
simp [leftAdjointCompIso_hom_app, leftAdjointIdIso_hom_app,
    reassoc_of% h₂, reassoc_of% h₁]

Premises used: CategoryTheory.Adjunction.leftAdjointCompIso_hom_app, CategoryTheory.Adjunction.leftAdjointIdIso_hom_app