awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
Z Y : (Over.{v₁, u₁} X)ᵒᵖ
f : Z ⟶ Y
dsimp : (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (unop Y).hom.op
⊢ Eq.{v₁ + 1} (α := op X ⟶ right.{v₁, u₁} (X := op X) (mk (unop Y).hom.op))
    (hom (mk (unop Z).hom.op) ≫ (Over.Hom.left f.unop).op) (hom (mk (unop Y).hom.op))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
Z Y : (Over.{v₁, u₁} X)ᵒᵖ
f : Z ⟶ Y
rw : (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (Over.Hom.left f.unop ≫ (unop Z).hom).op
rw₁ rw₂ :
  Eq.{v₁ + 1} (α := op X ⟶ op (unop Y).left) ((unop Z).hom.op ≫ (Over.Hom.left f.unop).op)
    ((unop Z).hom.op ≫ (Over.Hom.left f.unop).op)
⊢ (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (unop Y).hom.op

Tactic:
rw [← Over.w f.unop, op_comp]

Premises used: CategoryTheory.op_comp, Quiver.Hom.unop, CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
S S' : C
⊢ IsIso.{v, u} (S ↘ S)

Tactic:
inferInstanceAs (IsIso (𝟙 S))

Premises used: _private.0.CategoryTheory.instIsIsoOverInferInstanceOverClass._proof_1
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
S : C
inst_1 : OverClass X S
inst_2 : OverClass Y S
inst_3 : HomIsOver f S
⊢ f ≫ Y ↘ S = X ↘ S

Tactic:
HomIsOver.comp_over

Premises used: CategoryTheory.HomIsOver.comp_over
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
S S' : C
inst_1 : CanonicallyOverClass X Y
inst_2 : OverClass Y S
⊢ IsOverTower.{v, u} X Y S

Tactic:
⟨rfl⟩

Premises used: CategoryTheory.HomIsOver.mk, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst_1 : OverClass X S
inst_2 : OverClass X S'
inst_3 : OverClass Y S
inst_4 : OverClass Y S'
inst_5 : OverClass S S'
inst_6 : IsOverTower.{v, u} X S S'
inst_7 : IsOverTower.{v, u} Y S S'
inst_8 : HomIsOver f S
comp_over : autoParam (f ≫ Y ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam
⊢ HomIsOver f S'

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
S S' : C
inst_1 : OverClass X S
inst_2 : OverClass X S'
inst_3 : OverClass Y S
inst_4 : OverClass Y S'
inst_5 : OverClass S S'
inst_6 : IsOverTower.{v, u} X S S'
inst_7 : IsOverTower.{v, u} Y S S'
inst_8 : HomIsOver f S
comp_over : autoParam (f ≫ Y ↘ S ≫ S ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam
comp_over₁ : autoParam (Eq.{v + 1} (α := X ⟶ S') (X ↘ S ≫ S ↘ S') (X ↘ S')) HomIsOver.comp_over._autoParam
comp_over₂ comp_over₃ : autoParam (Eq.{v + 1} (α := X ⟶ S') (X ↘ S') (X ↘ S')) HomIsOver.comp_over._autoParam
⊢ autoParam (f ≫ Y ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam

Tactic:
rw [← comp_over (Y ↘ S), comp_over_assoc f, comp_over]

Premises used: inferInstance, CategoryTheory.over, CategoryTheory.comp_over_assoc, CategoryTheory.comp_over
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
S S' : C
inst_1 : CanonicallyOverClass X S
inst_2 : OverClass X S'
inst_3 : OverClass Y S
inst_4 : OverClass Y S'
inst_5 : OverClass S S'
inst_6 : IsOverTower.{v, u} X S S'
inst_7 : IsOverTower.{v, u} Y S S'
inst_8 : HomIsOver f S
⊢ HomIsOver f S'

Tactic:
homIsOver_of_isOverTower f S S'

Premises used: CategoryTheory.homIsOver_of_isOverTower
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
S S' : C
inst_1 : OverClass X S
inst_2 : OverClass X S'
inst_3 : CanonicallyOverClass Y S
inst_4 : OverClass Y S'
inst_5 : OverClass S S'
inst_6 : IsOverTower.{v, u} X S S'
inst_7 : IsOverTower.{v, u} Y S S'
inst_8 : HomIsOver f S
⊢ HomIsOver f S'

Tactic:
homIsOver_of_isOverTower f S S'

Premises used: CategoryTheory.homIsOver_of_isOverTower
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f_1 : X ⟶ Y
S S' : C
inst_1 : OverClass X S
inst_2 : OverClass Y S
inst_3 : OverClass Z S
f : X ⟶ Y
inst_4 : IsIso f
inst_5 : HomIsOver f S
⊢ IsIso (X := asOver X S) (Y := asOver Y S) (asOverHom S f)

Tactic:
have : IsIso ((Over.forget S).map (asOverHom S f)) := ‹_›
  isIso_of_reflects_iso _ (Over.forget _)

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.Over.forget, CategoryTheory.OverClass.asOverHom
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X S : C
inst_1 : OverClass X S
⊢ Eq.{v + 1} (α := Quiver.Hom (V := Over.{v, u} S) (asOver X S) (asOver X S)) (asOverHom S (𝟙 X)) (𝟙 (asOver X S))

Tactic:
rfl

Premises used: CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Over.homMk, CategoryTheory.OverClass.asOverHom, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z S : C
inst_1 : OverClass X S
inst_2 : OverClass Y S
inst_3 : OverClass Z S
f : X ⟶ Y
g : Y ⟶ Z
inst_4 : HomIsOver f S
inst_5 : HomIsOver g S
⊢ Eq (α := Quiver.Hom (V := Over.{v, u} S) (asOver X S) (asOver Z S)) (asOverHom S (f ≫ g))
    (CategoryStruct.comp (Y := asOver Y S) (asOverHom S f) (asOverHom S g))

Tactic:
rfl

Premises used: CategoryTheory.over, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Over.homMk, CategoryTheory.OverClass.asOverHom, rfl
-- Module: Mathlib.CategoryTheory.Comma.Over.OverClass
Goal:
C : Type u
inst : Category.{v, u} C
X Y S : C
inst_1 : OverClass X S
inst_2 : OverClass Y S
f : X ⟶ Y
inst_3 : IsIso f
inst_4 : HomIsOver f S
⊢ Eq (α := Quiver.Hom (V := Over.{v, u} S) (asOver Y S) (asOver X S)) (asOverHom S (inv f)) (inv (asOverHom S f))

Tactic:
simp [← hom_comp_eq_id, ← asOverHom_comp]

Premises used: CategoryTheory.hom_comp_eq_id, CategoryTheory.OverClass.asOverHom_comp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
g h : Over.{v, u} Y
k : g ⟶ h
⊢ Eq (α := (mk (Y := Limits.pullback g.hom f) (pullback.snd g.hom f)).left ⟶ Y)
    ((pullback.fst g.hom f ≫ Hom.left k) ≫ h.hom) (pullback.snd g.hom f ≫ f)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
x : Over.{v, u} X
y : Over.{v, u} Y
u : (map f).obj x ⟶ y
⊢ Hom.left u ≫ y.hom = x.hom ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
x : Over.{v, u} X
y : Over.{v, u} Y
v : x ⟶ (pullback f).obj y
⊢ (Hom.left v ≫ pullback.fst y.hom f) ≫ y.hom = ((map f).obj x).hom

Tactic:
simp [← Over.w v, pullback.condition]

Premises used: CategoryTheory.Over.w, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
x : Over.{v, u} X
y : Over.{v, u} Y
v : x ⟶ (pullback f).obj y
h :
  Hom.left
      ((fun (u : (map f).obj x ⟶ y) ↦ (homMk (pullback.lift (Hom.left u) x.hom ⋯) ⋯ : x ⟶ (pullback f).obj y))
        ((fun (v : x ⟶ (pullback f).obj y) ↦ homMk (Hom.left v ≫ pullback.fst y.hom f) ⋯) v)) =
    Hom.left v
⊢ (fun (u : (map f).obj x ⟶ y) ↦ (homMk (pullback.lift (Hom.left u) x.hom ⋯) ⋯ : x ⟶ (pullback f).obj y))
      ((fun (v : x ⟶ (pullback f).obj y) ↦ homMk (Hom.left v ≫ pullback.fst y.hom f) ⋯) v) =
    v

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
x : Over.{v, u} X
y : Over.{v, u} Y
v : x ⟶ (pullback f).obj y
h : pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ = Hom.left v
⊢ Hom.left
      ((fun (u : (map f).obj x ⟶ y) ↦ (homMk (pullback.lift (Hom.left u) x.hom ⋯) ⋯ : x ⟶ (pullback f).obj y))
        ((fun (v : x ⟶ (pullback f).obj y) ↦ homMk (Hom.left v ≫ pullback.fst y.hom f) ⋯) v)) =
    Hom.left v

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
x : Over.{v, u} X
y : Over.{v, u} Y
v : x ⟶ (pullback f).obj y
h :
  CategoryStruct.comp (Y := Limits.pullback y.hom f) (pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯)
      (pullback.fst y.hom f) =
    Hom.left v ≫ pullback.fst y.hom f
h₁ :
  CategoryStruct.comp (Y := Limits.pullback y.hom f) (pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯)
      (pullback.snd y.hom f) =
    Hom.left v ≫ pullback.snd y.hom f
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ = Hom.left v

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
x : Over.{v, u} X
y : Over.{v, u} Y
v : x ⟶ (pullback f).obj y
⊢ CategoryStruct.comp (Y := Limits.pullback y.hom f) (pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯)
      (pullback.fst y.hom f) =
    Hom.left v ≫ pullback.fst y.hom f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
x : Over.{v, u} X
y : Over.{v, u} Y
v : x ⟶ (pullback f).obj y
⊢ CategoryStruct.comp (Y := Limits.pullback y.hom f) (pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯)
      (pullback.snd y.hom f) =
    Hom.left v ≫ pullback.snd y.hom f

Tactic:
simpa using (Over.w v).symm

Premises used: CategoryTheory.Over.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
inst_3 : ∀ (Z : C) (g : Z ⟶ Y), Epi (X := Limits.pullback g f) (pullback.fst g f)
Z : Over.{v, u} Y
simp : Epi (homMk (pullback.fst Z.hom f) ⋯)
⊢ Epi (X := (pullback f ⋙ map f).obj Z) (NatTrans.app (Adjunction.counit (mapPullbackAdj f)) Z)

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, mapPullbackAdj_counit_app]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Over.mapPullbackAdj_counit_app, CategoryTheory.Functor.id_obj
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
inst_3 : ∀ (Z : C) (g : Z ⟶ Y), Epi (X := Limits.pullback g f) (pullback.fst g f)
Z : Over.{v, u} Y
⊢ Epi (homMk (pullback.fst Z.hom f) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
inst_3 : ∀ (Z : C) (g : Z ⟶ Y), Epi (X := Limits.pullback g f) (pullback.fst g f)
⊢ ∀ (Z : Over.{v, u} Y), Epi (X := (pullback f ⋙ map f).obj Z) (NatTrans.app (Adjunction.counit (mapPullbackAdj f)) Z)

Tactic:
have (Z : Over Y) : Epi ((mapPullbackAdj f).counit.app Z) := by
    simp only [Functor.comp_obj, Functor.id_obj, mapPullbackAdj_counit_app]; infer_instance
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
inst_3 : ∀ (Z : C) (g : Z ⟶ Y), Epi (X := Limits.pullback g f) (pullback.fst g f)
this :
  ∀ (Z : Over.{v, u} Y), Epi (X := (pullback f ⋙ map f).obj Z) (NatTrans.app (Adjunction.counit (mapPullbackAdj f)) Z)
⊢ (pullback f).Faithful

Tactic:
(mapPullbackAdj f).faithful_R_of_epi_counit_app

Premises used: CategoryTheory.Over.mapPullbackAdj, CategoryTheory.Adjunction.faithful_R_of_epi_counit_app
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
inst_3 : ∀ (Z : C) (g : Z ⟶ Y), Epi (X := Limits.pullback g f) (pullback.fst g f)
this :
  ∀ (Z : Over.{v, u} Y), Epi (X := (pullback f ⋙ map f).obj Z) (NatTrans.app (Adjunction.counit (mapPullbackAdj f)) Z)
⊢ (pullback f).Faithful

Tactic:
exact (mapPullbackAdj f).faithful_R_of_epi_counit_app

Premises used: CategoryTheory.Over.mapPullbackAdj, CategoryTheory.Adjunction.faithful_R_of_epi_counit_app
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPullbacksAlong f
⊢ (pullback f).IsRightAdjoint

Tactic:
⟨_, ⟨mapPullbackAdj f⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Over.mapPullbackAdj, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{v, u} C
F : Functor.{v, v₂, u, u₂} C D
inst_3 : F.IsLeftAdjoint
⊢ Functor.IsLeftAdjoint (C := Over.{v, u} X) (post F)

Tactic:
let ⟨G, ⟨a⟩⟩ := ‹F.IsLeftAdjoint›; ⟨_, ⟨postAdjunctionLeft a⟩⟩

Premises used: CategoryTheory.Over.pullback, CategoryTheory.Over.postAdjunctionLeft, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.unit, Nonempty.intro, CategoryTheory.Functor.IsLeftAdjoint, CategoryTheory.Over.post, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, _private.0.CategoryTheory.Over.isLeftAdjoint_post.match_1, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := Functor.obj.{v, v, u, u} (star X ⋙ forget X) Y ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y)
    (NatTrans.app (Adjunction.counit (forgetAdjStar X)) Y) prod.snd

Tactic:
simp [Over.forgetAdjStar, CategoryTheory.coalgebraEquivOver]

Premises used: CategoryTheory.coalgebraEquivOver, CategoryTheory.Over.forgetAdjStar
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
X : C
Y : Over.{v, u} X
⊢ Eq (α := (Functor.obj (𝟭 (Over.{v, u} X)) Y).left ⟶ (Functor.obj (forget X ⋙ star X) Y).left)
    (Hom.left (NatTrans.app (Adjunction.unit (forgetAdjStar X)) Y)) (prod.lift Y.hom (𝟙 Y.left))

Tactic:
simp [Over.forgetAdjStar, CategoryTheory.coalgebraEquivOver]

Premises used: CategoryTheory.coalgebraEquivOver, CategoryTheory.Over.forgetAdjStar
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasBinaryProducts.{v, u} C
⊢ Functor.IsRightAdjoint (C := Over.{v, u} X) (star X)

Tactic:
⟨_, ⟨forgetAdjStar X⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk, CategoryTheory.Over.forgetAdjStar
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasBinaryProducts.{v, u} C
⊢ Functor.IsLeftAdjoint (C := Over.{v, u} X) (forget X)

Tactic:
⟨_, ⟨forgetAdjStar X⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Over.forgetAdjStar
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq.{v + 1} (α := left.{v, u} (Functor.obj (star Y) Z) ⟶ Y) (hom (Functor.obj (star Y) Z)) prod.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
⊢ CategoryStruct.comp (Y := left.{v, u} (Functor.obj (star X) Z))
      (Iso.hom
        (Iso.trans (Y := Limits.pullback (X := left.{v, u} (Functor.obj (star Y) Z)) prod.fst f) (pullback.congrHom ⋯ ⋯)
          (pullbackSymmetry prod.fst f ≪≫ pullbackProdFstIsoProd f Z)))
      (hom (Functor.obj (star X) Z)) =
    ((star Y ⋙ pullback f).obj Z).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x x' : Under.{v, u} X
u : x ⟶ x'
⊢ Eq (α := X ⟶ (mk (Y := Limits.pushout x'.hom f) (pushout.inr x'.hom f)).right)
    (x.hom ≫ Hom.right u ≫ pushout.inl x'.hom f) (f ≫ pushout.inr x'.hom f)

Tactic:
simp [← pushout.condition]

Premises used: CategoryTheory.Limits.pushout.condition
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
u : (pushout f).obj x ⟶ y
simp : x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ y.hom
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = ((map f).obj y).hom

Tactic:
simp only [map_obj_hom]

Premises used: CategoryTheory.Under.map_obj_hom
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
u : (pushout f).obj x ⟶ y
rw : x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ ((pushout f).obj x).hom ≫ Hom.right u
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ y.hom

Tactic:
rw [← Under.w u]

Premises used: CategoryTheory.Under.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
u : (pushout f).obj x ⟶ y
simp : x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ pushout.inr x.hom f ≫ Hom.right u
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ ((pushout f).obj x).hom ≫ Hom.right u

Tactic:
simp only [map_obj_right, pushout_obj, mk_right, mk_hom]

Premises used: CategoryTheory.Under.mk_hom, CategoryTheory.Under.map_obj_right, CategoryTheory.Under.mk_right, CategoryTheory.Under.pushout_obj
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
u : (pushout f).obj x ⟶ y
rw : (x.hom ≫ pushout.inl x.hom f) ≫ Hom.right u = f ≫ pushout.inr x.hom f ≫ Hom.right u
rw₁ : (x.hom ≫ pushout.inl x.hom f) ≫ Hom.right u = (f ≫ pushout.inr x.hom f) ≫ Hom.right u
rw₂ rw₃ : (f ≫ pushout.inr x.hom f) ≫ Hom.right u = (f ≫ pushout.inr x.hom f) ≫ Hom.right u
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ pushout.inr x.hom f ≫ Hom.right u

Tactic:
rw [← assoc, ← assoc, pushout.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pushout.condition
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
v : x ⟶ (map f).obj y
⊢ x.hom ≫ Hom.right v = f ≫ y.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
u : (pushout f).obj x ⟶ y
h :
  Hom.right
      ((fun (v : x ⟶ (map f).obj y) ↦ (homMk (pushout.desc (Hom.right v) y.hom ⋯) ⋯ : (pushout f).obj x ⟶ y))
        ((fun (u : (pushout f).obj x ⟶ y) ↦ homMk (pushout.inl x.hom f ≫ Hom.right u) ⋯) u)) =
    Hom.right u
⊢ (fun (v : x ⟶ (map f).obj y) ↦ (homMk (pushout.desc (Hom.right v) y.hom ⋯) ⋯ : (pushout f).obj x ⟶ y))
      ((fun (u : (pushout f).obj x ⟶ y) ↦ homMk (pushout.inl x.hom f ≫ Hom.right u) ⋯) u) =
    u

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
u : (pushout f).obj x ⟶ y
h : pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = Hom.right u
⊢ Hom.right
      ((fun (v : x ⟶ (map f).obj y) ↦ (homMk (pushout.desc (Hom.right v) y.hom ⋯) ⋯ : (pushout f).obj x ⟶ y))
        ((fun (u : (pushout f).obj x ⟶ y) ↦ homMk (pushout.inl x.hom f ≫ Hom.right u) ⋯) u)) =
    Hom.right u

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
u : (pushout f).obj x ⟶ y
h :
  CategoryStruct.comp (Y := Limits.pushout x.hom f) (pushout.inl x.hom f)
      (pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯) =
    pushout.inl x.hom f ≫ Hom.right u
h₁ :
  CategoryStruct.comp (Y := Limits.pushout x.hom f) (pushout.inr x.hom f)
      (pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯) =
    pushout.inr x.hom f ≫ Hom.right u
⊢ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = Hom.right u

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
u : (pushout f).obj x ⟶ y
⊢ CategoryStruct.comp (Y := Limits.pushout x.hom f) (pushout.inl x.hom f)
      (pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯) =
    pushout.inl x.hom f ≫ Hom.right u

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
x : Under.{v, u} X
y : Under.{v, u} Y
u : (pushout f).obj x ⟶ y
⊢ CategoryStruct.comp (Y := Limits.pushout x.hom f) (pushout.inr x.hom f)
      (pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯) =
    pushout.inr x.hom f ≫ Hom.right u

Tactic:
simpa using (Under.w u).symm

Premises used: Eq.symm, CategoryTheory.Under.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
inst_3 : ∀ (Z : C) (g : X ⟶ Z), Mono (Y := Limits.pushout g f) (pushout.inl g f)
Z : Under.{v, u} X
simp : Mono (homMk (pushout.inl Z.hom f) ⋯)
⊢ Mono (Y := (pushout f ⋙ map f).obj Z) (NatTrans.app (Adjunction.unit (mapPushoutAdj f)) Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
inst_3 : ∀ (Z : C) (g : X ⟶ Z), Mono (Y := Limits.pushout g f) (pushout.inl g f)
Z : Under.{v, u} X
⊢ Mono (homMk (pushout.inl Z.hom f) ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Comma.Over.Pullback
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst_2 : HasPushoutsAlong f
inst_3 : ∀ (Z : C) (g : X ⟶ Z), Mono (Y := Limits.pushout g f) (pushout.inl g f)
⊢ ∀ (Z : Under.{v, u} X), Mono (Y := (pushout f ⋙ map f).obj Z) (NatTrans.app (Adjunction.unit (mapPushoutAdj f)) Z)

Tactic:
have (Z : Under X) : Mono ((mapPushoutAdj f).unit.app Z) := by simp; infer_instance