awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
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_6} D₁
inst_4 : Category.{v_5, u_7} D₂
inst_5 : Category.{v_6, u_8} D₃
inst_6 : Category.{v_13, u_13} E
L₁ : Functor.{v_1, v_4, u_1, u_6} C₁ D₁
L₂ : Functor.{v_2, v_5, u_2, u_7} C₂ D₂
L₃ : Functor.{v_3, v_6, u_3, u_8} C₃ D₃
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₃ : MorphismProperty.{v_3, u_3} C₃
inst_7 : L₁.IsLocalization W₁
inst_8 : L₂.IsLocalization W₂
inst_9 : L₃.IsLocalization W₃
inst_10 : W₁.ContainsIdentities
inst_11 : W₂.ContainsIdentities
inst_12 : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_13, u_3, u_13} C₃ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ Functor.{v_6, v_13, u_8, u_13} D₃ E
inst_13 : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst_14 : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ NatTrans.app
      (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (obj uncurry₃ F₁) (obj uncurry₃ F₂) (obj uncurry₃ F₁')
        (obj uncurry₃ F₂') (map uncurry₃ τ))
      (L₁.obj X₁, L₂.obj X₂, L₃.obj X₃) =
    (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃ ≫
      ((τ.app X₁).app X₂).app X₃ ≫ (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃

Tactic:
liftNatTrans_app _ _ _ _ (uncurry₃.obj F₁') (uncurry₃.obj F₂') (uncurry₃.map τ) ⟨X₁, X₂, X₃⟩

Premises used: CategoryTheory.Functor.uncurry₃, Prod.mk, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.Functor.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Localization.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
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_6} D₁
inst_4 : Category.{v_5, u_7} D₂
inst_5 : Category.{v_6, u_8} D₃
inst_6 : Category.{v_13, u_13} E
L₁ : Functor.{v_1, v_4, u_1, u_6} C₁ D₁
L₂ : Functor.{v_2, v_5, u_2, u_7} C₂ D₂
L₃ : Functor.{v_3, v_6, u_3, u_8} C₃ D₃
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₃ : MorphismProperty.{v_3, u_3} C₃
inst_7 : L₁.IsLocalization W₁
inst_8 : L₂.IsLocalization W₂
inst_9 : L₃.IsLocalization W₃
inst_10 : W₁.ContainsIdentities
inst_11 : W₂.ContainsIdentities
inst_12 : W₃.ContainsIdentities
F₁ F₂ : C₁ ⥤ C₂ ⥤ Functor.{v_3, v_13, u_3, u_13} C₃ E
F₁' F₂' : D₁ ⥤ D₂ ⥤ Functor.{v_6, v_13, u_8, u_13} D₃ E
inst_13 : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'
inst_14 : Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'
τ : F₁ ⟶ F₂
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ NatTrans.app
      (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (obj uncurry₃ F₁) (obj uncurry₃ F₂) (obj uncurry₃ F₁')
        (obj uncurry₃ F₂') (map uncurry₃ τ))
      (L₁.obj X₁, L₂.obj X₂, L₃.obj X₃) =
    (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁').hom.app X₁).app X₂).app X₃ ≫
      ((τ.app X₁).app X₂).app X₃ ≫ (((Lifting₃.iso L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂').inv.app X₁).app X₂).app X₃

Tactic:
exact liftNatTrans_app _ _ _ _ (uncurry₃.obj F₁') (uncurry₃.obj F₂') (uncurry₃.map τ) ⟨X₁, X₂, X₃⟩

Premises used: CategoryTheory.Functor.uncurry₃, Prod.mk, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.Functor.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Localization.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_13
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_6} D₁
inst_4 : Category.{v_5, u_7} D₂
inst_5 : Category.{v_6, u_8} D₃
inst_6 : Category.{v_13, u_13} E
L₁ : Functor.{v_1, v_4, u_1, u_6} C₁ D₁
L₂ : Functor.{v_2, v_5, u_2, u_7} C₂ D₂
L₃ : Functor.{v_3, v_6, u_3, u_8} C₃ D₃
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
W₃ : MorphismProperty.{v_3, u_3} C₃
inst_7 : L₁.IsLocalization W₁
inst_8 : L₂.IsLocalization W₂
inst_9 : L₃.IsLocalization W₃
inst_10 : W₁.ContainsIdentities
inst_11 : W₂.ContainsIdentities
inst_12 : W₃.ContainsIdentities
F₁' F₂' : D₁ ⥤ D₂ ⥤ Functor.{v_6, v_13, u_8, u_13} D₃ E
τ τ' : F₁' ⟶ F₂'
h :
  ∀ (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
    Eq (α :=
      ((F₁'.obj (L₁.obj X₁)).obj (L₂.obj X₂)).obj (L₃.obj X₃) ⟶ ((F₂'.obj (L₁.obj X₁)).obj (L₂.obj X₂)).obj (L₃.obj X₃))
      (NatTrans.app (NatTrans.app (τ.app (L₁.obj X₁)) (L₂.obj X₂)) (L₃.obj X₃))
      (NatTrans.app (NatTrans.app (τ'.app (L₁.obj X₁)) (L₂.obj X₂)) (L₃.obj X₃))
⊢ τ = τ'

Tactic:
uncurry₃.map_injective (natTrans_ext (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃))
    (fun _ ↦ h _ _ _))

Premises used: CategoryTheory.Localization.natTrans_ext, CategoryTheory.Functor.uncurry₃, CategoryTheory.MorphismProperty.prod, CategoryTheory.Functor.prod, Prod.fst, CategoryTheory.Functor.map_injective, Prod.snd
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
Y : Over.{v₁, u₁} X
rw :
  Eq (α := Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (𝟭 (Over.{v₁, u₁} X)) (Functor.obj (map (𝟙 X)) Y))
    (CategoryStruct.comp (Y := Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
        (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y)
        (NatTrans.app (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))
          (Functor.obj (map (𝟙 X)) Y)) :
      Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (𝟭 (Over.{v₁, u₁} X)) (Functor.obj (map (𝟙 X)) Y))
    (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y :
      Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
rw₁ rw₂ :
  Eq (α := Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (𝟭 (Over.{v₁, u₁} X)) (Functor.obj (map (𝟙 X)) Y))
    (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y :
      Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)) Y)
    (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y :
      Functor.obj (𝟭 (Over.{v₁, u₁} X)) Y ⟶ Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
⊢ CategoryStruct.comp (Y := Functor.obj (map (𝟙 X) ⋙ pullback (𝟙 X)) Y)
      (NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y)
      (NatTrans.app (Iso.hom (pullbackId X)) (Functor.obj (map (𝟙 X)) Y)) =
    NatTrans.app (Adjunction.unit (mapPullbackAdj (𝟙 X))) Y

Tactic:
rw [pullbackId, Adjunction.unit_rightAdjointUniq_hom_app]

Premises used: CategoryTheory.ChosenPullbacksAlong.pullbackId, CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_app
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
rw :
  Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := map (𝟙 X) ⋙ pullback (𝟙 X)) (Adjunction.unit (mapPullbackAdj (𝟙 X)))
        (Functor.whiskerLeft (map (𝟙 X))
          (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))) :
      Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
    (Adjunction.unit (mapPullbackAdj (𝟙 X)) :
      Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ pullback (𝟙 X)))
rw₁ rw₂ :
  Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
    (Adjunction.unit (mapPullbackAdj (𝟙 X)) :
      Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
    (Adjunction.unit (mapPullbackAdj (𝟙 X)) :
      Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ pullback (𝟙 X)))
⊢ Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (𝟭 (Over.{v₁, u₁} X)) (map (𝟙 X) ⋙ 𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := map (𝟙 X) ⋙ pullback (𝟙 X)) (Adjunction.unit (mapPullbackAdj (𝟙 X)))
      (Functor.whiskerLeft (map (𝟙 X)) (Iso.hom (pullbackId X))))
    (Adjunction.unit (mapPullbackAdj (𝟙 X)))

Tactic:
rw [pullbackId, Adjunction.unit_rightAdjointUniq_hom]

Premises used: CategoryTheory.ChosenPullbacksAlong.pullbackId, CategoryTheory.Adjunction.unit_rightAdjointUniq_hom
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
⊢ Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := pullback (𝟙 X) ⋙ map (𝟙 X))
      (Functor.whiskerRight (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))
        (map (𝟙 X)))
      (Adjunction.counit (mapPullbackAdj (𝟙 X))))
    (Adjunction.counit (mapPullbackAdj (𝟙 X)))

Tactic:
have := Adjunction.rightAdjointUniq_hom_counit (mapPullbackAdj (𝟙 X)) (id X).mapPullbackAdj
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : ChosenPullbacksAlong.{v₁, u₁} (𝟙 X)
this :
  Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := pullback (𝟙 X) ⋙ map (𝟙 X))
      (Functor.whiskerRight (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))
        (map (𝟙 X)))
      (Adjunction.counit (mapPullbackAdj (𝟙 X))))
    (Adjunction.counit (mapPullbackAdj (𝟙 X)))
rw :
  Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
    (CategoryStruct.comp (Y := 𝟭 (Over.{v₁, u₁} X) ⋙ map (𝟙 X))
      (Functor.whiskerRight (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (𝟙 X)) (mapPullbackAdj (𝟙 X))))
          (map (𝟙 X)) :
        Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X))
          (𝟭 (Over.{v₁, u₁} X) ⋙ map (𝟙 X)))
      (Adjunction.counit (mapPullbackAdj (𝟙 X)) :
        Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X))))
    (Adjunction.counit (mapPullbackAdj (𝟙 X)))
rw₁ rw₂ :
  Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
    (Adjunction.counit (mapPullbackAdj (𝟙 X))) (Adjunction.counit (mapPullbackAdj (𝟙 X)))
⊢ Eq (α := Quiver.Hom (V := Over.{v₁, u₁} X ⥤ Over.{v₁, u₁} X) (pullback (𝟙 X) ⋙ map (𝟙 X)) (𝟭 (Over.{v₁, u₁} X)))
    (Functor.whiskerRight (Iso.hom (pullbackId X)) (map (𝟙 X)) ≫ Adjunction.counit (mapPullbackAdj (𝟙 X)))
    (Adjunction.counit (mapPullbackAdj (𝟙 X)))

Tactic:
rw [pullbackId, Adjunction.rightAdjointUniq_hom_counit]

Premises used: CategoryTheory.ChosenPullbacksAlong.pullbackId, CategoryTheory.Adjunction.rightAdjointUniq_hom_counit
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
rw :
  Eq (α := 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
    (CategoryStruct.comp (Y := map (f ≫ g) ⋙ pullback (f ≫ g)) (Adjunction.unit (mapPullbackAdj (f ≫ g)))
        ((map (f ≫ g)).whiskerLeft
          (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (f ≫ g)) (mapPullbackAdj (f ≫ g))))) :
      𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
    (Adjunction.unit (mapPullbackAdj (f ≫ g)) : 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback (f ≫ g))
rw₁ rw₂ :
  Eq (α := 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
    (Adjunction.unit (mapPullbackAdj (f ≫ g)) : 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
    (Adjunction.unit (mapPullbackAdj (f ≫ g)) : 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback (f ≫ g))
⊢ Eq (α := 𝟭 (Over.{v₁, u₁} X) ⟶ map (f ≫ g) ⋙ pullback g ⋙ pullback f)
    (CategoryStruct.comp (Y := map (f ≫ g) ⋙ pullback (f ≫ g)) (Adjunction.unit (mapPullbackAdj (f ≫ g)))
      ((map (f ≫ g)).whiskerLeft (Iso.hom (pullbackComp f g))))
    (Adjunction.unit (mapPullbackAdj (f ≫ g)))

Tactic:
rw [pullbackComp, Adjunction.unit_rightAdjointUniq_hom]

Premises used: CategoryTheory.Adjunction.unit_rightAdjointUniq_hom, CategoryTheory.ChosenPullbacksAlong.pullbackComp
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
rw :
  Eq (α := pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z))
    (CategoryStruct.comp (Y := (pullback g ⋙ pullback f) ⋙ map (f ≫ g))
      (Functor.whiskerRight (Iso.hom (Adjunction.rightAdjointUniq (mapPullbackAdj (f ≫ g)) (mapPullbackAdj (f ≫ g))))
          (map (f ≫ g)) :
        pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ (pullback g ⋙ pullback f) ⋙ map (f ≫ g))
      (Adjunction.counit (mapPullbackAdj (f ≫ g)) : pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z)))
    (Adjunction.counit (mapPullbackAdj (f ≫ g)))
rw₁ rw₂ :
  Eq (α := pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z)) (Adjunction.counit (mapPullbackAdj (f ≫ g)))
    (Adjunction.counit (mapPullbackAdj (f ≫ g)))
⊢ Eq (α := pullback (f ≫ g) ⋙ map (f ≫ g) ⟶ 𝟭 (Over.{v₁, u₁} Z))
    (CategoryStruct.comp (Y := (pullback g ⋙ pullback f) ⋙ map (f ≫ g))
      (Functor.whiskerRight (Iso.hom (pullbackComp f g)) (map (f ≫ g))) (Adjunction.counit (mapPullbackAdj (f ≫ g))))
    (Adjunction.counit (mapPullbackAdj (f ≫ g)))

Tactic:
rw [pullbackComp, Adjunction.rightAdjointUniq_hom_counit]

Premises used: CategoryTheory.ChosenPullbacksAlong.pullbackComp, CategoryTheory.Adjunction.rightAdjointUniq_hom_counit
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
⊢ Eq (α := ((map g).obj ((pullback g).obj (Over.mk f))).left ⟶ (Over.mk f).left) (Hom.left (fst' f g)) (fst f g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
⊢ Eq (α := ((map g).obj ((pullback g).obj (Over.mk f))).left ⟶ (Over.mk g).left) (Hom.left (snd' f g)) (snd f g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
⊢ Eq (α := pullbackObj f g ⟶ X) (fst f g ≫ f) (snd f g ≫ g)

Tactic:
Over.w (fst' f g)

Premises used: CategoryTheory.Over, CategoryTheory.ChosenPullbacksAlong.fst', CategoryTheory.CostructuredArrow, CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
⊢ φ₂ ≫ ((pullback g).obj (Over.mk f)).hom = U.hom

Tactic:
simpa using h₂.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
a :
  Eq (α := (map g).obj U ⟶ Over.mk f)
    ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₁' :
      (map g).obj U ⟶ Over.mk f)
    ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₂' :
      (map g).obj U ⟶ Over.mk f)
⊢ φ₁' = φ₂'

Tactic:
apply (adj.homEquiv U _).symm.injective

Premises used: CategoryTheory.Adjunction.homEquiv, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
a :
  Eq.{v₁ + 1} (α := Functor.obj (forget X) ((map g).obj U) ⟶ Functor.obj (forget X) (Over.mk f))
    (Functor.map (forget X)
      ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₁'))
    (Functor.map (forget X)
      ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₂'))
⊢ Eq (α := (map g).obj U ⟶ Over.mk f)
    ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₁' :
      (map g).obj U ⟶ Over.mk f)
    ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₂' :
      (map g).obj U ⟶ Over.mk f)

Tactic:
apply (Over.forget X).map_injective

Premises used: CategoryTheory.Over.forget, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
⊢ Eq.{v₁ + 1} (α := Functor.obj (forget X) ((map g).obj U) ⟶ Functor.obj (forget X) (Over.mk f))
    (Functor.map (forget X)
      ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₁'))
    (Functor.map (forget X)
      ((Equiv.symm (adj.homEquiv U (Over.mk f)) : (a : U ⟶ (pullback g).obj (Over.mk f)) → (map g).obj U ⟶ Over.mk f)
        φ₂'))

Tactic:
simpa using h₁
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
⊢ φ₁' = φ₂'

Tactic:
have : φ₁' = φ₂' := by
    apply (adj.homEquiv U _).symm.injective
    apply (Over.forget X).map_injective
    simpa using h₁
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
this : φ₁' = φ₂'
⊢ φ₁ = φ₂

Tactic:
congr_arg CommaMorphism.left this

Premises used: congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
φ₁ φ₂ : W ⟶ pullbackObj f g
h₁ : φ₁ ≫ fst f g = φ₂ ≫ fst f g
h₂ : φ₁ ≫ snd f g = φ₂ ≫ snd f g
adj : map g ⊣ pullback g := mapPullbackAdj g
U : Over.{v₁, u₁} Z := Over.mk (φ₁ ≫ snd f g)
φ₁' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₁ ⋯
φ₂' : U ⟶ (pullback g).obj (Over.mk f) := homMk φ₂ ⋯
this : φ₁' = φ₂'
⊢ φ₁ = φ₂

Tactic:
exact congr_arg CommaMorphism.left this

Premises used: congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
adj : map g ⊣ pullback g := mapPullbackAdj g
a' : (map g).obj (Over.mk b) ⟶ Over.mk f := homMk a h
⊢ CategoryStruct.comp (Y := (map g).obj ((pullback g).obj (Over.mk f)))
      ((map g).map
        ((adj.homEquiv (Over.mk b) (Over.mk f) :
            (a : (map g).obj (Over.mk b) ⟶ Over.mk f) → Over.mk b ⟶ (pullback g).obj (Over.mk f))
          (homMk a ⋯)))
      (fst' f g) =
    a'

Tactic:
simp only [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply, adj, a']

Premises used: Equiv.symm_apply_apply, CategoryTheory.Adjunction.homEquiv_counit
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
adj : map g ⊣ pullback g := mapPullbackAdj g
a' : (map g).obj (Over.mk b) ⟶ Over.mk f := homMk a h
⊢ CategoryStruct.comp (Y := (map g).obj ((pullback g).obj (Over.mk f)))
      ((map g).map
        ((adj.homEquiv (Over.mk b) (Over.mk f) :
            (a : (map g).obj (Over.mk b) ⟶ Over.mk f) → Over.mk b ⟶ (pullback g).obj (Over.mk f))
          (homMk a ⋯)))
      (fst' f g) =
    a'

Tactic:
have : (Over.map g).map (adj.homEquiv (.mk b) (.mk f) (Over.homMk a)) ≫ fst' f g = a' := by
    simp only [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply, adj, a']
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
adj : map g ⊣ pullback g := mapPullbackAdj g
a' : (map g).obj (Over.mk b) ⟶ Over.mk f := homMk a h
this :
  CategoryStruct.comp (Y := (map g).obj ((pullback g).obj (Over.mk f)))
      ((map g).map
        ((adj.homEquiv (Over.mk b) (Over.mk f) :
            (a : (map g).obj (Over.mk b) ⟶ Over.mk f) → Over.mk b ⟶ (pullback g).obj (Over.mk f))
          (homMk a ⋯)))
      (fst' f g) =
    a'
⊢ CategoryStruct.comp (Y := pullbackObj f g) (lift a b h) (fst f g) = a

Tactic:
congr_arg CommaMorphism.left this

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.ChosenPullbacksAlong.lift
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
adj : map g ⊣ pullback g := mapPullbackAdj g
a' : (map g).obj (Over.mk b) ⟶ Over.mk f := homMk a h
this :
  CategoryStruct.comp (Y := (map g).obj ((pullback g).obj (Over.mk f)))
      ((map g).map
        ((adj.homEquiv (Over.mk b) (Over.mk f) :
            (a : (map g).obj (Over.mk b) ⟶ Over.mk f) → Over.mk b ⟶ (pullback g).obj (Over.mk f))
          (homMk a ⋯)))
      (fst' f g) =
    a'
⊢ CategoryStruct.comp (Y := pullbackObj f g) (lift a b h) (fst f g) = a

Tactic:
exact congr_arg CommaMorphism.left this

Premises used: congr_arg, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y Z X : C
f : Y ⟶ X
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
W : C
a : W ⟶ Y
b : W ⟶ Z
h : a ≫ f = b ≫ g
⊢ CategoryStruct.comp (Y := pullbackObj f g) (lift a b h) (snd f g) = b

Tactic:
simp [lift]

Premises used: CategoryTheory.ChosenPullbacksAlong.lift