awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
⊢ CategoryStruct.comp (Y := G.obj ((fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) PUnit.unit))
      ((fun (x : PUnit.{w + 1}) ↦
          (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
            Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
        PUnit.unit)
      (G.map
        (((Equiv.symm (Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B) :
              Equiv.{v + 1, v₁ + 1} (A ⟶ G.obj B) (G.leftAdjoint.obj A ⟶ B)) :
            (a : A ⟶ G.obj B) → G.leftAdjoint.obj A ⟶ B)
          h)) =
    h
have rw : ((Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B :
        Equiv.{v₁ + 1, v + 1} (G.leftAdjoint.obj A ⟶ B) (A ⟶ G.obj B)) :
      (a : G.leftAdjoint.obj A ⟶ B) → A ⟶ G.obj B)
    (((Equiv.symm (Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B) :
          Equiv.{v + 1, v₁ + 1} (A ⟶ G.obj B) (G.leftAdjoint.obj A ⟶ B)) :
        (a : A ⟶ G.obj B) → G.leftAdjoint.obj A ⟶ B)
      h) =
  h
Tactic: rw [← Adjunction.homEquiv_unit, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : G.IsRightAdjoint
A : C
B : D
h : A ⟶ G.obj B
rw :
  ((Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B :
          Equiv.{v₁ + 1, v + 1} (G.leftAdjoint.obj A ⟶ B) (A ⟶ G.obj B)) :
        (a : G.leftAdjoint.obj A ⟶ B) → A ⟶ G.obj B)
      (((Equiv.symm (Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B) :
            Equiv.{v + 1, v₁ + 1} (A ⟶ G.obj B) (G.leftAdjoint.obj A ⟶ B)) :
          (a : A ⟶ G.obj B) → G.leftAdjoint.obj A ⟶ B)
        h) =
    h
⊢ CategoryStruct.comp (Y := G.obj ((fun (x : PUnit.{w + 1}) ↦ G.leftAdjoint.obj A) PUnit.unit))
      ((fun (x : PUnit.{w + 1}) ↦
          (NatTrans.app (Adjunction.unit (Adjunction.ofIsRightAdjoint G)) A :
            Functor.obj.{v, v, u, u} (𝟭 C) A ⟶ (G.leftAdjoint ⋙ G).obj A))
        PUnit.unit)
      (G.map
        (((Equiv.symm (Adjunction.homEquiv (Adjunction.ofIsRightAdjoint G) A B) :
              Equiv.{v + 1, v₁ + 1} (A ⟶ G.obj B) (G.leftAdjoint.obj A ⟶ B)) :
            (a : A ⟶ G.obj B) → G.leftAdjoint.obj A ⟶ B)
          h)) =
    h
have rw₁ : h = h
Tactic: rw [← Adjunction.homEquiv_unit, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : HasLimits.{v₁, u₁} D
inst_3 : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
hG : SolutionSetCondition G
⊢ G.IsRightAdjoint
have refine : ∀ (A : C), HasInitial (StructuredArrow A G)
Tactic: refine @isRightAdjointOfStructuredArrowInitials _ _ _ _ G ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : HasLimits.{v₁, u₁} D
inst_3 : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
hG : SolutionSetCondition G
A : C
⊢ HasInitial (StructuredArrow A G)
have hG₁ : ∃ (ι : Type v₁) (B : ι → D) (f : (i : ι) → A ⟶ G.obj (B i)),
  ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h
Tactic: specialize hG A
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : HasLimits.{v₁, u₁} D
inst_3 : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
hG :
  ∃ (ι : Type v₁) (B : ι → D) (f : (i : ι) → A ⟶ G.obj (B i)),
    ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)
have choose : ∀ (ι : Type v₁) (B : ι → D) (f : (i : ι) → A ⟶ G.obj (B i))
  (g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h), HasInitial (StructuredArrow A G)
Tactic: choose ι B f g using hG
Cleared hypotheses: hG
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : HasLimits.{v₁, u₁} D
inst_3 : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun (i : ι) ↦ StructuredArrow.mk (f i)
A' : StructuredArrow A G
⊢ ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')
have obtain : ∀ (i : ι) (w : B i ⟶ A'.right) (t : f i ≫ G.map w = A'.hom), ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')
Tactic: obtain ⟨i, _, t⟩ := g _ A'.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : HasLimits.{v₁, u₁} D
inst_3 : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun (i : ι) ↦ StructuredArrow.mk (f i)
⊢ HasInitial (StructuredArrow A G)
have hB' : ∀ (A' : StructuredArrow A G), ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')
Tactic: have hB' : ∀ A' : StructuredArrow A G, ∃ i, Nonempty (B' i ⟶ A') := by
    intro A'
    obtain ⟨i, _, t⟩ := g _ A'.hom
    exact ⟨i, ⟨StructuredArrow.homMk _ t⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
G : Functor.{v₁, v, u₁, u} D C
inst_2 : HasLimits.{v₁, u₁} D
inst_3 : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ (i : ι) (g : B i ⟶ X), f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun (i : ι) ↦ StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ (i : ι), Nonempty.{v₁ + 1} (B' i ⟶ A')
⊢ HasInitial (StructuredArrow A G)
have obtain : ∀ (T : StructuredArrow A G) (hT : ∀ (X : StructuredArrow A G), Nonempty.{v₁ + 1} (T ⟶ X)),
  HasInitial (StructuredArrow A G)
Tactic: obtain ⟨T, hT⟩ := has_weakly_initial_of_weakly_initial_set_and_hasProducts hB'
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v, u'} D
inst_2 : HasLimits.{v, u'} D
inst_3 : WellPowered.{v, v, u'} D
P : ObjectProperty.{v, u'} D
inst_4 : ObjectProperty.Small.{v, v, u'} P
hP : P.IsCoseparating
G : Functor.{v, v, u', u} D C
inst_5 : PreservesLimits G
⊢ G.IsRightAdjoint
have this : ∀ (A : C), HasInitial (StructuredArrow A G)
Tactic: have : ∀ A, HasInitial (StructuredArrow A G) := fun A ↦
    hasInitial_of_isCoseparating.{v} (StructuredArrow.isCoseparating_inverseImage_proj A G hP)
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X : C
Y : D
g : X ⟶ G.obj Y
⊢ (fun (f : F.obj X ⟶ Y) ↦ adj.unit.app X ≫ G.map f) ((fun (g : X ⟶ G.obj Y) ↦ F.map g ≫ adj.counit.app Y) g) = g
have simp : adj.unit.app X ≫ G.map (F.map g) ≫ G.map (adj.counit.app Y) = g
Tactic: simp only [Functor.comp_obj, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X : C
Y : D
g : X ⟶ G.obj Y
⊢ adj.unit.app X ≫ G.map (F.map g) ≫ G.map (adj.counit.app Y) = g
have rw : (map (𝟭 C) g ≫ adj.unit.app (G.obj Y)) ≫ G.map (adj.counit.app Y) = g
Tactic: rw [← assoc, ← Functor.comp_map, ← adj.unit.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
h' : adj.counit = adj'.counit
⊢ adj = adj'
have mk : ∀ (unit : 𝟭 C ⟶ F ⋙ G) (counit : G ⋙ F ⟶ 𝟭 D)
  (left_triangle_components : ∀ (X : C), F.map (unit.app X) ≫ counit.app (F.obj X) = 𝟙 (F.obj X))
  (right_triangle_components : ∀ (Y : D), unit.app (G.obj Y) ≫ G.map (counit.app Y) = 𝟙 (G.obj Y))
  (h :
    { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
          right_triangle_components := right_triangle_components : F ⊣ G }.unit =
      adj'.unit)
  (h' :
    { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
          right_triangle_components := right_triangle_components : F ⊣ G }.counit =
      adj'.counit),
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
      right_triangle_components := right_triangle_components : F ⊣ G } =
    adj'
Tactic: cases adj
Cleared hypotheses: adj, h, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj' : F ⊣ G
unit : 𝟭 C ⟶ F ⋙ G
counit : G ⋙ F ⟶ 𝟭 D
left_triangle_components : ∀ (X : C), F.map (unit.app X) ≫ counit.app (F.obj X) = 𝟙 (F.obj X)
right_triangle_components : ∀ (Y : D), unit.app (G.obj Y) ≫ G.map (counit.app Y) = 𝟙 (G.obj Y)
h :
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components : F ⊣ G }.unit =
    adj'.unit
h' :
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components : F ⊣ G }.counit =
    adj'.counit
⊢ { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
      right_triangle_components := right_triangle_components : F ⊣ G } =
    adj'
have mk : ∀ (unit_1 : 𝟭 C ⟶ F ⋙ G) (counit_1 : G ⋙ F ⟶ 𝟭 D)
  (left_triangle_components_1 : ∀ (X : C), F.map (unit_1.app X) ≫ counit_1.app (F.obj X) = 𝟙 (F.obj X))
  (right_triangle_components_1 : ∀ (Y : D), unit_1.app (G.obj Y) ≫ G.map (counit_1.app Y) = 𝟙 (G.obj Y))
  (h :
    { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
          right_triangle_components := right_triangle_components : F ⊣ G }.unit =
      { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
          right_triangle_components := right_triangle_components_1 }.unit)
  (h' :
    { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
          right_triangle_components := right_triangle_components : F ⊣ G }.counit =
      { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
          right_triangle_components := right_triangle_components_1 }.counit),
  { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
      right_triangle_components := right_triangle_components : F ⊣ G } =
    { unit := unit_1, counit := counit_1, left_triangle_components := left_triangle_components_1,
      right_triangle_components := right_triangle_components_1 }
Tactic: cases adj'
Cleared hypotheses: adj', h, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
⊢ adj = adj'
have suffices : adj.counit = adj'.counit
Tactic: suffices h' : adj.counit = adj'.counit by cases adj; cases adj'; aesop
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
⊢ adj.counit = adj'.counit
have w : ∀ (X : D), adj.counit.app X = adj'.counit.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ adj.counit.app X = adj'.counit.app X
have w : Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
  (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
            (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
        (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
      (adj.counit.app X) :
    G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
  (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
            (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
        (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
      (adj'.counit.app X) :
    G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
Tactic: apply (adj.homEquiv _ _).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj'.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
have w : adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) =
  ((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
        Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
          (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
      (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
    (adj'.counit.app X)
Tactic: rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
    Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
w :
  adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) =
    ((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
            (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
        (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
      (adj'.counit.app X)
⊢ Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj'.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
have w₁ : adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
Tactic: rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
    Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
w :
  adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) =
    ((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
            (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
        (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
      (adj'.counit.app X)
w₁ : adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
⊢ Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj'.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
have w₂ : 𝟙 (G.obj X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
Tactic: rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
    Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
w :
  adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) =
    ((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
            (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
        (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
      (adj'.counit.app X)
w₁ : adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
w₂ : 𝟙 (G.obj X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
⊢ Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj'.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
have w₃ : 𝟙 (G.obj X) = adj'.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
Tactic: rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
    Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
w :
  adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) =
    ((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
          Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
            (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
        (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
      (adj'.counit.app X)
w₁ : adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
w₂ : 𝟙 (G.obj X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
w₃ : 𝟙 (G.obj X) = adj'.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
⊢ Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
    (((adj.homEquiv (G.obj X) (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X) :
            Equiv.{v₂ + 1, v₁ + 1} (F.obj (G.obj X) ⟶ obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)
              (G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))) :
          (a : F.obj (G.obj X) ⟶ (𝟭 D).obj X) → G.obj X ⟶ G.obj ((𝟭 D).obj X))
        (adj'.counit.app X) :
      G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X))
have w₄ : Eq.{v₁ + 1} (α := G.obj X ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 D) X)) (𝟙 (G.obj X)) (𝟙 (G.obj X))
Tactic: rw [Adjunction.homEquiv_unit, Adjunction.homEquiv_unit,
    Adjunction.right_triangle_components, h, Adjunction.right_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ Eq.{v₁ + 1} (α := X' ⟶ G.obj Y) ((adj.homEquiv X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G.obj Y) (F.map f ≫ g) : X' ⟶ G.obj Y)
    (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g : X' ⟶ G.obj Y)
have rw : F.map f ≫ g =
  ((adj.homEquiv X' Y).symm : (a : X' ⟶ G.obj Y) → F.obj X' ⟶ Y)
    (f ≫ (adj.homEquiv X Y : (a : F.obj X ⟶ Y) → X ⟶ G.obj Y) g)
Tactic: rw [← Equiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
adj : F ⊣ G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y')
    (((adj.homEquiv X Y').symm : (a : X ⟶ G.obj Y') → F.obj X ⟶ Y') (f ≫ G.map g) : F.obj X ⟶ Y')
    (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f ≫ g : F.obj X ⟶ Y')
have rw : f ≫ G.map g =
  (adj.homEquiv X Y' : (a : F.obj X ⟶ Y') → X ⟶ G.obj Y')
    (((adj.homEquiv X Y).symm : (a : X ⟶ G.obj Y) → F.obj X ⟶ Y) f ≫ g)
Tactic: rw [Equiv.symm_apply_eq]