awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Basic (hypothesis)
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
F_obj : C → D
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F_obj X ⟶ Y) (X ⟶ G.obj Y)
he :
  ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X ⟶ G.obj Y') ((e X Y' : (a : F_obj X ⟶ Y') → X ⟶ G.obj Y') (h ≫ g) : X ⟶ G.obj Y')
      ((e X Y : (a : F_obj X ⟶ Y) → X ⟶ G.obj Y) h ≫ G.map g : X ⟶ G.obj Y')
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ Eq.{v₂ + 1} (α := (leftAdjointOfEquiv e he).obj X' ⟶ Y)
    (((e X' Y).symm : (a : X' ⟶ G.obj Y) → (leftAdjointOfEquiv e he).obj X' ⟶ Y) (f ≫ g) :
      (leftAdjointOfEquiv e he).obj X' ⟶ Y)
    ((leftAdjointOfEquiv e he).map f ≫ ((e X Y).symm : (a : X ⟶ G.obj Y) → (leftAdjointOfEquiv e he).obj X ⟶ Y) g :
      (leftAdjointOfEquiv e he).obj X' ⟶ Y)
have this : ∀ {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y'),
  Eq.{v₂ + 1} (α := F_obj X ⟶ Y') (((e X Y').symm : (a : X ⟶ G.obj Y') → F_obj X ⟶ Y') (f ≫ G.map g) : F_obj X ⟶ Y')
    (((e X Y).symm : (a : X ⟶ G.obj Y) → F_obj X ⟶ Y) f ≫ g : F_obj X ⟶ Y')
Tactic: have {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
            (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g := by
          rw [Equiv.symm_apply_eq, he]; simp
-- 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_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ Eq (α := F.obj X' ⟶ Y) (F.map f ≫ ((e X Y).symm : (a : X ⟶ G_obj Y) → F.obj X ⟶ Y) g)
    (((e X' Y).symm : (a : X' ⟶ G_obj Y) → F.obj X' ⟶ Y) (f ≫ g))
have rw : f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) (((e X Y).symm : (a : X ⟶ G_obj Y) → F.obj X ⟶ Y) g) = f ≫ g
Tactic: rw [Equiv.eq_symm_apply, he]
-- 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
G_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ Eq.{v₁ + 1} (α := G_obj Y ⟶ G_obj Y'')
    ((e (G_obj Y) Y'' : (a : F.obj (G_obj Y) ⟶ Y'') → G_obj Y ⟶ G_obj Y'')
        ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g ≫ g') :
      G_obj Y ⟶ G_obj Y'')
    (CategoryStruct.comp (Y := G_obj Y')
        ((e (G_obj Y) Y' : (a : F.obj (G_obj Y) ⟶ Y') → G_obj Y ⟶ G_obj Y')
          ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g))
        ((e (G_obj Y') Y'' : (a : F.obj (G_obj Y') ⟶ Y'') → G_obj Y' ⟶ G_obj Y'')
          ((Equiv.symm (e (G_obj Y') Y') : (a : G_obj Y' ⟶ G_obj Y') → F.obj (G_obj Y') ⟶ Y') (𝟙 (G_obj Y')) ≫ g')) :
      G_obj Y ⟶ G_obj Y'')
have rw : Eq.{v₂ + 1} (α := F.obj (G_obj Y) ⟶ Y'')
  ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g ≫ g' :
    F.obj (G_obj Y) ⟶ Y'')
  (CategoryStruct.comp (Y := F.obj (G_obj Y'))
      (F.map
        ((e (G_obj Y) Y' : (a : F.obj (G_obj Y) ⟶ Y') → G_obj Y ⟶ G_obj Y')
          ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g)))
      ((Equiv.symm (e (G_obj Y') Y') : (a : G_obj Y' ⟶ G_obj Y') → F.obj (G_obj Y') ⟶ Y') (𝟙 (G_obj Y')) ≫ g') :
    F.obj (G_obj Y) ⟶ Y'')
Tactic: rw [← Equiv.eq_symm_apply, ← he'' e he, Equiv.symm_apply_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
G_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| Eq.{v₂ + 1} (α := F.obj (G_obj Y) ⟶ Y'')
    ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g ≫ g' :
      F.obj (G_obj Y) ⟶ Y'')
    (CategoryStruct.comp (Y := F.obj (G_obj Y'))
        (F.map
          ((e (G_obj Y) Y' : (a : F.obj (G_obj Y) ⟶ Y') → G_obj Y ⟶ G_obj Y')
            ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g)))
        ((Equiv.symm (e (G_obj Y') Y') : (a : G_obj Y' ⟶ G_obj Y') → F.obj (G_obj Y') ⟶ Y') (𝟙 (G_obj Y')) ≫ g') :
      F.obj (G_obj Y) ⟶ Y'')
have rhs : CategoryStruct.comp (Y := F.obj (G_obj Y'))
  (F.map
    ((e (G_obj Y) Y' : (a : F.obj (G_obj Y) ⟶ Y') → G_obj Y ⟶ G_obj Y')
      ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g)))
  ((Equiv.symm (e (G_obj Y') Y') : (a : G_obj Y' ⟶ G_obj Y') → F.obj (G_obj Y') ⟶ Y') (𝟙 (G_obj Y')) ≫ g')
Tactic: rhs
-- 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
G_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| CategoryStruct.comp (Y := F.obj (G_obj Y'))
    (F.map
      ((e (G_obj Y) Y' : (a : F.obj (G_obj Y) ⟶ Y') → G_obj Y ⟶ G_obj Y')
        ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g)))
    ((Equiv.symm (e (G_obj Y') Y') : (a : G_obj Y' ⟶ G_obj Y') → F.obj (G_obj Y') ⟶ Y') (𝟙 (G_obj Y')) ≫ g')
have rw : (((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g) ≫ g' :
  F.obj (G_obj Y) ⟶ Y'')
Tactic: rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_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
G_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| Eq.{v₂ + 1} (α := F.obj (G_obj Y) ⟶ Y'')
    ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g ≫ g' :
      F.obj (G_obj Y) ⟶ Y'')
    (CategoryStruct.comp (Y := F.obj (G_obj Y'))
        (F.map
          ((e (G_obj Y) Y' : (a : F.obj (G_obj Y) ⟶ Y') → G_obj Y ⟶ G_obj Y')
            ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g)))
        ((Equiv.symm (e (G_obj Y') Y') : (a : G_obj Y' ⟶ G_obj Y') → F.obj (G_obj Y') ⟶ Y') (𝟙 (G_obj Y')) ≫ g') :
      F.obj (G_obj Y) ⟶ Y'')
have rw : (((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g) ≫ g' :
  F.obj (G_obj Y) ⟶ Y'')
Tactic: rhs
      rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_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
G_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ Eq.{v₂ + 1} (α := F.obj (G_obj Y) ⟶ Y'')
    ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g ≫ g' :
      F.obj (G_obj Y) ⟶ Y'')
    (CategoryStruct.comp (Y := F.obj (G_obj Y'))
        (F.map
          ((e (G_obj Y) Y' : (a : F.obj (G_obj Y) ⟶ Y') → G_obj Y ⟶ G_obj Y')
            ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g)))
        ((Equiv.symm (e (G_obj Y') Y') : (a : G_obj Y' ⟶ G_obj Y') → F.obj (G_obj Y') ⟶ Y') (𝟙 (G_obj Y')) ≫ g') :
      F.obj (G_obj Y) ⟶ Y'')
have conv : Eq.{v₂ + 1} (α := F.obj (G_obj Y) ⟶ Y'')
  ((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g ≫ g' :
    F.obj (G_obj Y) ⟶ Y'')
  (((Equiv.symm (e (G_obj Y) Y) : (a : G_obj Y ⟶ G_obj Y) → F.obj (G_obj Y) ⟶ Y) (𝟙 (G_obj Y)) ≫ g) ≫ g' :
    F.obj (G_obj Y) ⟶ Y'')
Tactic: conv =>
      rhs
      rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_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
G_obj : D → C
e : (X : C) → (Y : D) → Equiv.{v₂ + 1, v₁ + 1} (F.obj X ⟶ Y) (X ⟶ G_obj Y)
he :
  ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
    Eq.{v₁ + 1} (α := X' ⟶ G_obj Y) ((e X' Y : (a : F.obj X' ⟶ Y) → X' ⟶ G_obj Y) (F.map f ≫ g) : X' ⟶ G_obj Y)
      (f ≫ (e X Y : (a : F.obj X ⟶ Y) → X ⟶ G_obj Y) g : X' ⟶ G_obj Y)
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ Y)
    (((e X Y).symm : (a : X ⟶ (rightAdjointOfEquiv e he).obj Y) → F.obj X ⟶ Y) (f ≫ g) : F.obj X ⟶ Y)
    (F.map f ≫ ((e X' Y).symm : (a : X' ⟶ (rightAdjointOfEquiv e he).obj Y) → F.obj X' ⟶ Y) g : F.obj X ⟶ Y)
have rw : f ≫ g =
  (e X Y : (a : F.obj X ⟶ Y) → X ⟶ (rightAdjointOfEquiv e he).obj Y)
    (F.map f ≫ ((e X' Y).symm : (a : X' ⟶ (rightAdjointOfEquiv e he).obj Y) → F.obj X' ⟶ Y) g)
Tactic: rw [Equiv.symm_apply_eq]
-- 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 Y : C
f : X ⟶ Y
Z : D
⊢ (Function.Bijective (β := F.obj X ⟶ Z) fun (g : F.obj Y ⟶ Z) ↦ F.map f ≫ g) ↔
    Function.Bijective (β := X ⟶ G.obj Z) fun (g : Y ⟶ G.obj Z) ↦ f ≫ g
have rw : Function.Bijective.{v₁ + 1, v₁ + 1} (α := Y ⟶ G.obj Z) (β := X ⟶ G.obj Z)
    (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
      (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) fun (g : F.obj Y ⟶ Z) ↦
        F.map f ≫ g)
      (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z)) ↔
  Function.Bijective (β := X ⟶ G.obj Z) fun (g : Y ⟶ G.obj Z) ↦ f ≫ g
Tactic: rw [← Function.Bijective.of_comp_iff' (adj.homEquiv _ _).bijective,
    ← Function.Bijective.of_comp_iff _ (adj.homEquiv _ _).symm.bijective]
-- 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 Y : C
f : X ⟶ Y
Z : D
⊢ Function.Bijective.{v₁ + 1, v₁ + 1} (α := Y ⟶ G.obj Z) (β := X ⟶ G.obj Z)
      (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
        (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z)
          fun (g : F.obj Y ⟶ Z) ↦ F.map f ≫ g)
        (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z)) ↔
    Function.Bijective (β := X ⟶ G.obj Z) fun (g : Y ⟶ G.obj Z) ↦ f ≫ g
have a : ∀ (x : Y ⟶ G.obj Z),
  Eq (α := (Y ⟶ G.obj Z) → (X ⟶ G.obj Z))
    (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
      (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) fun (g : F.obj Y ⟶ Z) ↦
        F.map f ≫ g)
      (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z))
    (CategoryStruct.comp f)
Tactic: congr!
-- 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 Y : C
f : X ⟶ Y
Z : D
x : Y ⟶ G.obj Z
⊢ Eq (α := (Y ⟶ G.obj Z) → (X ⟶ G.obj Z))
    (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
      (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) fun (g : F.obj Y ⟶ Z) ↦
        F.map f ≫ g)
      (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z))
    (CategoryStruct.comp f)
have a : ∀ (g : Y ⟶ G.obj Z),
  Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Y ⟶ Z)
      (Function.comp (β := F.obj X ⟶ Z) (⇑(adj.homEquiv X Z) : (a : F.obj X ⟶ Z) → X ⟶ G.obj Z) fun (g : F.obj Y ⟶ Z) ↦
        F.map f ≫ g)
      (⇑(adj.homEquiv Y Z).symm : (a : Y ⟶ G.obj Z) → F.obj Y ⟶ Z) g =
    f ≫ g
Tactic: ext g
-- 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 Y : D
g : X ⟶ Y
Z : C
⊢ (Function.Bijective (β := Z ⟶ G.obj Y) fun (f : Z ⟶ G.obj X) ↦ f ≫ G.map g) ↔
    Function.Bijective (β := F.obj Z ⟶ Y) fun (f : F.obj Z ⟶ X) ↦ f ≫ g
have rw : (Function.Bijective (β := Z ⟶ G.obj Y) fun (f : Z ⟶ G.obj X) ↦ f ≫ G.map g) ↔
  Function.Bijective.{v₁ + 1, v₁ + 1} (α := Z ⟶ G.obj X) (β := Z ⟶ G.obj Y)
    (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Z ⟶ X)
      (Function.comp (β := F.obj Z ⟶ Y) (⇑(adj.homEquiv Z Y) : (a : F.obj Z ⟶ Y) → Z ⟶ G.obj Y) fun (f : F.obj Z ⟶ X) ↦
        f ≫ g)
      (⇑(adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X))
Tactic: rw [← Function.Bijective.of_comp_iff' (adj.homEquiv _ _).bijective,
    ← Function.Bijective.of_comp_iff _ (adj.homEquiv _ _).symm.bijective]
-- 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 Y : D
g : X ⟶ Y
Z : C
⊢ (Function.Bijective (β := Z ⟶ G.obj Y) fun (f : Z ⟶ G.obj X) ↦ f ≫ G.map g) ↔
    Function.Bijective.{v₁ + 1, v₁ + 1} (α := Z ⟶ G.obj X) (β := Z ⟶ G.obj Y)
      (Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Z ⟶ X)
        (Function.comp (β := F.obj Z ⟶ Y) (⇑(adj.homEquiv Z Y) : (a : F.obj Z ⟶ Y) → Z ⟶ G.obj Y)
          fun (f : F.obj Z ⟶ X) ↦ f ≫ g)
        (⇑(adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X))
have a : ∀ (x : Z ⟶ G.obj X),
  x ≫ G.map g =
    Function.comp.{v₁ + 1, v₂ + 1, v₁ + 1} (β := F.obj Z ⟶ X)
      (Function.comp (β := F.obj Z ⟶ Y) (⇑(adj.homEquiv Z Y) : (a : F.obj Z ⟶ Y) → Z ⟶ G.obj Y) fun (f : F.obj Z ⟶ X) ↦
        f ≫ g)
      (⇑(adj.homEquiv Z X).symm : (a : Z ⟶ G.obj X) → F.obj Z ⟶ X) x
Tactic: congr!
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Comma (hypothesis)
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), HasInitial (StructuredArrow A G)
A : C
B : D
g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk (StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
⊢ (fun (f : A ⟶ G.obj B) ↦
        (CommaMorphism.right (initial.to (StructuredArrow.mk f)) :
          Comma.right.{0, v₂, v₁, 0, u₂, u₁} (A := Discrete PUnit.{1}) (T := C) (L := Functor.fromPUnit A) (R := G)
              (⊥_ StructuredArrow A G) ⟶
            (StructuredArrow.mk f).right))
      ((fun (g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B) ↦
          StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
        g) =
    g
have this : initial.to B' = g'
Tactic: have : initial.to _ = g' := by cat_disch
-- 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
inst_2 : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk (StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
this : initial.to B' = g'
⊢ (fun (f : A ⟶ G.obj B) ↦
        (CommaMorphism.right (initial.to (StructuredArrow.mk f)) :
          Comma.right.{0, v₂, v₁, 0, u₂, u₁} (A := Discrete PUnit.{1}) (T := C) (L := Functor.fromPUnit A) (R := G)
              (⊥_ StructuredArrow A G) ⟶
            (StructuredArrow.mk f).right))
      ((fun (g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B) ↦
          StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
        g) =
    g
have change : CommaMorphism.right (initial.to B') = g
Tactic: change CommaMorphism.right (initial.to B') = _
-- 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
inst_2 : ∀ (A : C), HasInitial (StructuredArrow A G)
A : C
B : D
g : StructuredArrow.right.{v₂, v₁, u₂, u₁} (D := C) (S := A) (T := G) (⊥_ StructuredArrow A G) ⟶ B
B' : StructuredArrow A G := StructuredArrow.mk (StructuredArrow.hom (⊥_ StructuredArrow A G) ≫ G.map g)
g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g ⋯
this : initial.to B' = g'
⊢ CommaMorphism.right (initial.to B') = g
have rw : g'.right = g
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Adjunction.Comma (hypothesis)
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 ⋯
⊢ (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
have this : terminal.from B' = g'
Tactic: have : terminal.from _ = g' := by cat_disch
-- 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
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'
⊢ CommaMorphism.left (terminal.from B') = g
have rw : g'.left = g
Tactic: rw [this]
-- 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
inst_2 : ∀ (A : C), HasTerminal (CostructuredArrow G A)
B₁ B₂ : D
A : C
f : B₁ ⟶ B₂
g : G.obj B₂ ⟶ A
⊢ 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))
have 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)
Tactic: rw [← Equiv.eq_symm_apply]
-- 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 : 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
⊢ 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)
      ⋯
have 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)
      sorry)
Tactic: apply StructuredArrow.ext