awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
rw : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ γ₁ ≫ f) ((snd f' g' ≫ γ₂) ≫ g)
rw₁ : Eq (α := pullbackObj f' g' ⟶ X) (fst f' g' ≫ f' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₂ : Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ f') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₃ : Eq (α := pullbackObj f' g' ⟶ X) ((snd f' g' ≫ g') ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₄ : Eq (α := pullbackObj f' g' ⟶ X) (snd f' g' ≫ g' ≫ γ₃) ((snd f' g' ≫ γ₂) ≫ g)
rw₅ : Eq (α := pullbackObj f' g' ⟶ X) (snd f' g' ≫ γ₂ ≫ g) ((snd f' g' ≫ γ₂) ≫ g)
rw₆ rw₇ : Eq (α := pullbackObj f' g' ⟶ X) (snd f' g' ≫ γ₂ ≫ g) (snd f' g' ≫ γ₂ ≫ g)
⊢ Eq (α := pullbackObj f' g' ⟶ X) ((fst f' g' ≫ γ₁) ≫ f) ((snd f' g' ≫ γ₂) ≫ g)

Tactic:
rw [assoc, ← comm₁, ← assoc, condition, assoc, comm₂, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ChosenPullbacksAlong.condition
-- 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
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
⊢ Eq (α := pullbackObj f' g' ⟶ Y)
    (CategoryStruct.comp (Y := pullbackObj f g) (pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) (fst f g)) (fst f' g' ≫ γ₁)

Tactic:
simp only [pullbackMap, lift_fst]

Premises used: CategoryTheory.ChosenPullbacksAlong.lift_fst
-- 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
Y' Z' X' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
inst_2 : ChosenPullbacksAlong g'
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
comm₁ : f' ≫ γ₃ = γ₁ ≫ f
comm₂ : g' ≫ γ₃ = γ₂ ≫ g
⊢ Eq (α := pullbackObj f' g' ⟶ Z)
    (CategoryStruct.comp (Y := pullbackObj f g) (pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) (snd f g)) (snd f' g' ≫ γ₂)

Tactic:
simp only [pullbackMap, lift_snd]

Premises used: CategoryTheory.ChosenPullbacksAlong.lift_snd
-- 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
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst_2 : ChosenPullbacksAlong g'
inst_3 : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_2
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_3
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_4
rw : δ₁ ≫ f' ≫ γ₃ = (δ₁ ≫ γ₁) ≫ f
rw₁ : δ₁ ≫ γ₁ ≫ f = (δ₁ ≫ γ₁) ≫ f
rw₂ rw₃ : δ₁ ≫ γ₁ ≫ f = δ₁ ≫ γ₁ ≫ f
⊢ f'' ≫ δ₃ ≫ γ₃ = (δ₁ ≫ γ₁) ≫ f

Tactic:
rw [reassoc_of% comm₁', comm₁, assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
Y' Z' X' Y'' Z'' X'' : C
f' : Y' ⟶ X'
g' : Z' ⟶ X'
f'' : Y'' ⟶ X''
g'' : Z'' ⟶ X''
inst_2 : ChosenPullbacksAlong g'
inst_3 : ChosenPullbacksAlong g''
γ₁ : Y' ⟶ Y
γ₂ : Z' ⟶ Z
γ₃ : X' ⟶ X
δ₁ : Y'' ⟶ Y'
δ₂ : Z'' ⟶ Z'
δ₃ : X'' ⟶ X'
comm₁ : autoParam (f' ≫ γ₃ = γ₁ ≫ f) pullbackMap_comp._auto_1
comm₂ : autoParam (g' ≫ γ₃ = γ₂ ≫ g) pullbackMap_comp._auto_2
comm₁' : autoParam (f'' ≫ δ₃ = δ₁ ≫ f') pullbackMap_comp._auto_3
comm₂' : autoParam (g'' ≫ δ₃ = δ₂ ≫ g') pullbackMap_comp._auto_4
rw : δ₂ ≫ g' ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g
rw₁ : δ₂ ≫ γ₂ ≫ g = (δ₂ ≫ γ₂) ≫ g
rw₂ rw₃ : δ₂ ≫ γ₂ ≫ g = δ₂ ≫ γ₂ ≫ g
⊢ g'' ≫ δ₃ ≫ γ₃ = (δ₂ ≫ γ₂) ≫ g

Tactic:
rw [reassoc_of% comm₂', comm₂, assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
rw rw₁ : Eq (α := pullbackObj f g ⟶ X) (snd f g ≫ g) (snd f g ≫ g)
⊢ Eq (α := pullbackObj f g ⟶ X) (fst f g ≫ f) (snd f g ≫ g)

Tactic:
rw [condition]

Premises used: CategoryTheory.ChosenPullbacksAlong.condition
-- 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
⊢ (pullbackCone f g).fst = 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
⊢ (pullbackCone f g).snd = 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
W : C
⊢ ∀ (h : W ⟶ X), HasPullback h g

Tactic:
fun f => (isPullback f g).hasPullback

Premises used: CategoryTheory.ChosenPullbacksAlong.isPullback, CategoryTheory.IsPullback.hasPullback
-- 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
inst_2 : ChosenPullbacks.{v₁, u₁} C
⊢ HasPullbacks.{v₁, u₁} C

Tactic:
hasPullbacks_of_hasLimit_cospan _

Premises used: CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X : C
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
T : Over.{v₁, u₁} X
⊢ Eq (α := ((pullback g).obj T).left ⟶ T.left)
    (Hom.left (NatTrans.app (Iso.hom (pullbackIsoOverPullback g)) T) ≫ pullback.fst T.hom g) (fst T.hom g)

Tactic:
simpa using (Over.forget _).congr_map
    ((ChosenPullbacksAlong.mapPullbackAdj g).rightAdjointUniq_hom_app_counit
      (Over.mapPullbackAdj g) T)

Premises used: CategoryTheory.Over.forget, CategoryTheory.Adjunction.rightAdjointUniq_hom_app_counit, CategoryTheory.Functor.congr_map, CategoryTheory.Over.mapPullbackAdj, CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X : C
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
T : Over.{v₁, u₁} X
⊢ Eq (α := ((pullback g).obj T).left ⟶ Z)
    (Hom.left (NatTrans.app (Iso.hom (pullbackIsoOverPullback g)) T) ≫ pullback.snd T.hom g) (snd T.hom g)

Tactic:
Over.w ((pullbackIsoOverPullback g).hom.app T)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Over, CategoryTheory.Over.mk, CategoryTheory.CostructuredArrow, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback, CategoryTheory.Over.w, CategoryTheory.CostructuredArrow.mk, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X : C
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
T : Over.{v₁, u₁} X
⊢ Eq (α := ((Over.pullback g).obj T).left ⟶ T.left)
    (CategoryStruct.comp (Y := ((pullback g).obj T).left)
        (Hom.left (NatTrans.app (Iso.inv (pullbackIsoOverPullback g)) T)) (fst T.hom g) :
      ((Over.pullback g).obj T).left ⟶ T.left)
    (pullback.fst T.hom g : Limits.pullback T.hom g ⟶ T.left)

Tactic:
simp [← pullbackIsoOverPullback_hom_app_comp_fst, ← Over.comp_left_assoc]

Premises used: CategoryTheory.Over.comp_left_assoc, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X : C
g : Z ⟶ X
inst_1 : ChosenPullbacksAlong g
T : Over.{v₁, u₁} X
⊢ Eq (α := ((Over.pullback g).obj T).left ⟶ Z)
    (CategoryStruct.comp (Y := ((pullback g).obj T).left)
        (Hom.left (NatTrans.app (Iso.inv (pullbackIsoOverPullback g)) T)) (snd T.hom g) :
      ((Over.pullback g).obj T).left ⟶ Z)
    (pullback.snd T.hom g : Limits.pullback T.hom g ⟶ Z)

Tactic:
Over.w ((pullbackIsoOverPullback g).inv.app T)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Over, CategoryTheory.Over.mk, CategoryTheory.CostructuredArrow, CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback, CategoryTheory.Over.w, CategoryTheory.CostructuredArrow.mk, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : ChosenPullbacks.{v, u} C
I J : C
f : I ⟶ J
inst_2 : ExponentiableMorphism f
⊢ IsExponentiable f

Tactic:
⟨pushforward f, ⟨pullbackPushforwardAdj f⟩⟩

Premises used: CategoryTheory.ExponentiableMorphism.pushforward, CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
⊢ Eq (α := @pushforward _ _ _ _ f inst_1 _ ⋙ pullback f ⟶ 𝟭 (Over.{v, u} I)) (ev f) (counit (pullbackPushforwardAdj f))

Tactic:
rfl

Premises used: CategoryTheory.ExponentiableMorphism.ev, rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
⊢ Eq (α := 𝟭 (Over.{v, u} J) ⟶ pullback f ⋙ @pushforward _ _ _ _ f inst_1 _) (coev f) (unit (pullbackPushforwardAdj f))

Tactic:
rfl

Premises used: CategoryTheory.ExponentiableMorphism.coev, rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
X Y : Over.{v, u} I
g : X ⟶ Y
⊢ (pullback f).map ((@pushforward _ _ _ _ f inst_1 _).map g) ≫ NatTrans.app (ev f) Y = NatTrans.app (ev f) X ≫ g

Tactic:
ev f |>.naturality g

Premises used: CategoryTheory.Over, CategoryTheory.ExponentiableMorphism.ev, CategoryTheory.CostructuredArrow, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
X Y : Over.{v, u} J
g : X ⟶ Y
⊢ g ≫ NatTrans.app (coev f) Y = NatTrans.app (coev f) X ≫ (@pushforward _ _ _ _ f inst_1 _).map ((pullback f).map g)

Tactic:
coev f |>.naturality g

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow, CategoryTheory.NatTrans.naturality, CategoryTheory.ExponentiableMorphism.coev
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
X : Over.{v, u} J
⊢ CategoryStruct.comp (Y := (pullback f).obj ((pullback f ⋙ @pushforward _ _ _ _ f inst_1 _).obj X))
      ((pullback f).map (NatTrans.app (coev f) X)) (NatTrans.app (ev f) ((pullback f).obj X)) =
    𝟙 ((pullback f).obj X)

Tactic:
pullbackPushforwardAdj f |>.left_triangle_components X

Premises used: CategoryTheory.Over, CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj, CategoryTheory.CostructuredArrow, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
Y : Over.{v, u} I
⊢ NatTrans.app (coev f) ((@pushforward _ _ _ _ f inst_1 _).obj Y) ≫
      (@pushforward _ _ _ _ f inst_1 _).map (NatTrans.app (ev f) Y) =
    𝟙 ((@pushforward _ _ _ _ f inst_1 _).obj Y)

Tactic:
pullbackPushforwardAdj f |>.right_triangle_components Y

Premises used: CategoryTheory.Over, CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj, CategoryTheory.CostructuredArrow, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
X : Over.{v, u} I
A : Over.{v, u} J
u : (pullback f).obj A ⟶ X
⊢ Eq (α := A ⟶ (@pushforward _ _ _ _ f inst_1 _).obj X)
    ((homEquiv (pullbackPushforwardAdj f) A X : (a : (pullback f).obj A ⟶ X) → A ⟶ (pushforward f).obj X) u :
      A ⟶ (@pushforward _ _ _ _ f inst_1 _).obj X)
    (pushforwardCurry u : A ⟶ (@pushforward _ _ _ _ f inst_1 _).obj X)

Tactic:
rfl

Premises used: CategoryTheory.ExponentiableMorphism.pushforwardCurry, rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
X : Over.{v, u} I
A : Over.{v, u} J
v : A ⟶ (@pushforward _ _ _ _ f inst_1 _).obj X
⊢ (Equiv.symm (homEquiv (pullbackPushforwardAdj f) A X) : (a : A ⟶ (pushforward f).obj X) → (pullback f).obj A ⟶ X) v =
    pushforwardUncurry v

Tactic:
rfl

Premises used: CategoryTheory.ExponentiableMorphism.pushforwardUncurry, rfl
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
X : Over.{v, u} I
A : Over.{v, u} J
u : (pullback f).obj A ⟶ X
⊢ pushforwardUncurry (pushforwardCurry u) = u

Tactic:
pullbackPushforwardAdj f |>.homEquiv A X |>.left_inv u

Premises used: CategoryTheory.ExponentiableMorphism.pushforwardUncurry, CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj, CategoryTheory.ExponentiableMorphism.pushforwardCurry, CategoryTheory.Adjunction.homEquiv, Equiv.left_inv
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J : C
f : I ⟶ J
inst_1 : ChosenPullbacksAlong f
inst_2 : ExponentiableMorphism f
X : Over.{v, u} I
A : Over.{v, u} J
v : A ⟶ (@pushforward _ _ _ _ f inst_1 _).obj X
⊢ pushforwardCurry (pushforwardUncurry v) = v

Tactic:
pullbackPushforwardAdj f |>.homEquiv A X |>.right_inv v

Premises used: CategoryTheory.ExponentiableMorphism.pushforwardUncurry, CategoryTheory.Over, Equiv.right_inv, CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj, CategoryTheory.CostructuredArrow, CategoryTheory.ExponentiableMorphism.pushforwardCurry, CategoryTheory.Adjunction.homEquiv
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I : C
inst_1 : ChosenPullbacksAlong.{v, u} (𝟙 I)
⊢ Eq (α := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _) (𝟭 (Over.{v, u} I))

Tactic:
dsimp +instances only [id]

Premises used: CategoryTheory.ExponentiableMorphism.id
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I : C
inst_1 : ChosenPullbacksAlong.{v, u} (𝟙 I)
inst_2 : ExponentiableMorphism.{v, u} (𝟙 I)
rw :
  Eq (α := Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
    (CategoryStruct.comp (Y := pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _)
        (unit (pullbackPushforwardAdj (𝟙 I)))
        (Functor.whiskerLeft (pullback (𝟙 I))
          (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (𝟙 I)) (pullbackPushforwardAdj (𝟙 I))))) :
      Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
    (unit (pullbackPushforwardAdj (𝟙 I)) :
      Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I))
        (pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _))
rw₁ rw₂ :
  Eq (α := Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
    (unit (pullbackPushforwardAdj (𝟙 I)) :
      Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
    (unit (pullbackPushforwardAdj (𝟙 I)) :
      Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I))
        (pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _))
⊢ Eq (α := Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (𝟭 (Over.{v, u} I)) (pullback (𝟙 I) ⋙ 𝟭 (Over.{v, u} I)))
    (CategoryStruct.comp (Y := pullback (𝟙 I) ⋙ @pushforward _ _ _ _ (𝟙 I) inst_1 _)
      (unit (pullbackPushforwardAdj (𝟙 I))) (Functor.whiskerLeft (pullback (𝟙 I)) (Iso.hom (pushforwardId I))))
    (unit (pullbackPushforwardAdj (𝟙 I)))

Tactic:
rw [pushforwardId, Adjunction.unit_rightAdjointUniq_hom]

Premises used: CategoryTheory.Adjunction.unit_rightAdjointUniq_hom, CategoryTheory.ExponentiableMorphism.pushforwardId
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I : C
inst_1 : ChosenPullbacksAlong.{v, u} (𝟙 I)
inst_2 : ExponentiableMorphism.{v, u} (𝟙 I)
rw :
  Eq (α :=
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
      (𝟭 (Over.{v, u} I)))
    (CategoryStruct.comp (Y := 𝟭 (Over.{v, u} I) ⋙ pullback (𝟙 I))
      (Functor.whiskerRight (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (𝟙 I)) (pullbackPushforwardAdj (𝟙 I))))
          (pullback (𝟙 I)) :
        Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
          (𝟭 (Over.{v, u} I) ⋙ pullback (𝟙 I)))
      (counit (pullbackPushforwardAdj (𝟙 I)) :
        Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
          (𝟭 (Over.{v, u} I))))
    (counit (pullbackPushforwardAdj (𝟙 I)))
rw₁ rw₂ :
  Eq (α :=
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
      (𝟭 (Over.{v, u} I)))
    (counit (pullbackPushforwardAdj (𝟙 I))) (counit (pullbackPushforwardAdj (𝟙 I)))
⊢ Eq (α :=
    Quiver.Hom (V := Over.{v, u} I ⥤ Over.{v, u} I) (@pushforward _ _ _ _ (𝟙 I) inst_1 _ ⋙ pullback (𝟙 I))
      (𝟭 (Over.{v, u} I)))
    (Functor.whiskerRight (Iso.hom (pushforwardId I)) (pullback (𝟙 I)) ≫ counit (pullbackPushforwardAdj (𝟙 I)))
    (counit (pullbackPushforwardAdj (𝟙 I)))

Tactic:
rw [pushforwardId, Adjunction.rightAdjointUniq_hom_counit]

Premises used: CategoryTheory.ExponentiableMorphism.pushforwardId, CategoryTheory.Adjunction.rightAdjointUniq_hom_counit
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
inst_4 : ExponentiableMorphism f
inst_5 : ExponentiableMorphism g
⊢ @pushforward _ _ _ _ (f ≫ g) inst_3 _ = @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _

Tactic:
dsimp +instances only [comp]

Premises used: CategoryTheory.ExponentiableMorphism.comp
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
inst_4 : ExponentiableMorphism f
inst_5 : ExponentiableMorphism g
inst_6 : ExponentiableMorphism (f ≫ g)
rw :
  Eq (α := 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
    (CategoryStruct.comp (Y := pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
        (unit (pullbackPushforwardAdj (f ≫ g)))
        ((pullback (f ≫ g)).whiskerLeft
          (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (f ≫ g)) (pullbackPushforwardAdj (f ≫ g))))) :
      𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
    (unit (pullbackPushforwardAdj (f ≫ g)) :
      𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
rw₁ rw₂ :
  Eq (α := 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
    (unit (pullbackPushforwardAdj (f ≫ g)) :
      𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
    (unit (pullbackPushforwardAdj (f ≫ g)) :
      𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
⊢ Eq (α := 𝟭 (Over.{v, u} K) ⟶ pullback (f ≫ g) ⋙ @pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _)
    (CategoryStruct.comp (Y := pullback (f ≫ g) ⋙ @pushforward _ _ _ _ (f ≫ g) inst_3 _)
      (unit (pullbackPushforwardAdj (f ≫ g))) ((pullback (f ≫ g)).whiskerLeft (Iso.hom (pushforwardComp f g))))
    (unit (pullbackPushforwardAdj (f ≫ g)))

Tactic:
rw [pushforwardComp, Adjunction.unit_rightAdjointUniq_hom]

Premises used: CategoryTheory.Adjunction.unit_rightAdjointUniq_hom, CategoryTheory.ExponentiableMorphism.pushforwardComp
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
Goal:
C : Type u
inst : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst_1 : ChosenPullbacksAlong f
inst_2 : ChosenPullbacksAlong g
inst_3 : ChosenPullbacksAlong (f ≫ g)
inst_4 : ExponentiableMorphism f
inst_5 : ExponentiableMorphism g
inst_6 : ExponentiableMorphism (f ≫ g)
rw :
  Eq (α := @pushforward _ _ _ _ (f ≫ g) inst_3 _ ⋙ pullback (f ≫ g) ⟶ 𝟭 (Over.{v, u} I))
    (CategoryStruct.comp (Y := (@pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _) ⋙ pullback (f ≫ g))
      (Functor.whiskerRight
          (Iso.hom (rightAdjointUniq (pullbackPushforwardAdj (f ≫ g)) (pullbackPushforwardAdj (f ≫ g))))
          (pullback (f ≫ g)) :
        @pushforward _ _ _ _ (f ≫ g) inst_3 _ ⋙ pullback (f ≫ g) ⟶
          (@pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _) ⋙ pullback (f ≫ g))
      (counit (pullbackPushforwardAdj (f ≫ g)) :
        @pushforward _ _ _ _ (f ≫ g) inst_3 _ ⋙ pullback (f ≫ g) ⟶ 𝟭 (Over.{v, u} I)))
    (counit (pullbackPushforwardAdj (f ≫ g)))
rw₁ rw₂ :
  Eq (α := @pushforward _ _ _ _ (f ≫ g) inst_3 _ ⋙ pullback (f ≫ g) ⟶ 𝟭 (Over.{v, u} I))
    (counit (pullbackPushforwardAdj (f ≫ g))) (counit (pullbackPushforwardAdj (f ≫ g)))
⊢ Eq (α := @pushforward _ _ _ _ (f ≫ g) inst_3 _ ⋙ pullback (f ≫ g) ⟶ 𝟭 (Over.{v, u} I))
    (CategoryStruct.comp (Y := (@pushforward _ _ _ _ f inst_1 _ ⋙ @pushforward _ _ _ _ g inst_2 _) ⋙ pullback (f ≫ g))
      (Functor.whiskerRight (Iso.hom (pushforwardComp f g)) (pullback (f ≫ g)))
      (counit (pullbackPushforwardAdj (f ≫ g))))
    (counit (pullbackPushforwardAdj (f ≫ g)))

Tactic:
rw [pushforwardComp, Adjunction.rightAdjointUniq_hom_counit]

Premises used: CategoryTheory.ExponentiableMorphism.pushforwardComp, CategoryTheory.Adjunction.rightAdjointUniq_hom_counit
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Y Z : Over.{v₁, u₁} X
inst_1 : ChosenPullbacksAlong Z.hom
T : Over.{v₁, u₁} X
u : T ⟶ Y
v : T ⟶ Z
rw : T.hom = Over.Hom.left v ≫ Z.hom
rw₁ rw₂ : T.hom = T.hom
⊢ Over.Hom.left u ≫ Y.hom = Over.Hom.left v ≫ Z.hom

Tactic:
rw [Over.w u, Over.w v]

Premises used: CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
Y Z : Over.{v₁, u₁} X
inst_1 : ChosenPullbacksAlong Z.hom
T : Over.{v₁, u₁} X
u : T ⟶ Y
v : T ⟶ Z
⊢ lift (Over.Hom.left u) (Over.Hom.left v) ⋯ ≫ (binaryFan Y Z).pt.hom = T.hom

Tactic:
simp