awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (hypothesis)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T × T
Y Z : CostructuredArrow (C := Over.{v₁, u₁} X.1) (Over.forget X.1) X.2
m : Y ⟶ Z
⊢ Eq (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) (Functor.obj (proj (Over.forget X.1) X.2 ⋙ Over.forget X.1) Y) ⟶ X)
    (Functor.map (Functor.diag T) (Functor.map (proj (Over.forget X.1) X.2 ⋙ Over.forget X.1) m) ≫
      (fun (f : CostructuredArrow (C := Over.{v₁, u₁} X.1) (Over.forget X.1) X.2) ↦ (f.left.hom, f.hom)) Z)
    ((fun (f : CostructuredArrow (C := Over.{v₁, u₁} X.1) (Over.forget X.1) X.2) ↦ (f.left.hom, f.hom)) Y)
have this : Functor.map (Over.forget X.1) m.left ≫ Z.hom = Y.hom ≫ Functor.map (Functor.fromPUnit X.2) m.right
Tactic: have := m.w
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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₁} (op X)
f : Z ⟶ Y
⊢ (unop (op (Under.mk Y.hom.unop))).hom ≫ (Hom.left f).unop = (unop (op (Under.mk Z.hom.unop))).hom
have dsimp : Y.hom.unop ≫ (Hom.left f).unop = Z.hom.unop
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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₁} (op X)
f : Z ⟶ Y
⊢ Y.hom.unop ≫ (Hom.left f).unop = Z.hom.unop
have rw : (Hom.left f ≫ Y.hom).unop = Z.hom.unop
Tactic: rw [← unop_comp, Over.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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₁} (op X)
f : Z ⟶ Y
rw : (Hom.left f ≫ Y.hom).unop = Z.hom.unop
⊢ Y.hom.unop ≫ (Hom.left f).unop = Z.hom.unop
have rw₁ : Z.hom.unop = Z.hom.unop
Tactic: rw [← unop_comp, Over.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
Z Y : (Under.{v₁, u₁} X)ᵒᵖ
f : Z ⟶ Y
⊢ Eq.{v₁ + 1} (α := left.{v₁, u₁} (X := op X) (mk (unop Z).hom.op) ⟶ op X)
    ((Under.Hom.right f.unop).op ≫ hom (mk (unop Y).hom.op)) (hom (mk (unop Z).hom.op))
have dsimp : (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = (unop Z).hom.op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
Z Y : (Under.{v₁, u₁} X)ᵒᵖ
f : Z ⟶ Y
⊢ (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = (unop Z).hom.op
have rw : (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = ((unop Y).hom ≫ Under.Hom.right f.unop).op
Tactic: rw [← Under.w f.unop, op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
Z Y : (Under.{v₁, u₁} X)ᵒᵖ
f : Z ⟶ Y
rw : (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = ((unop Y).hom ≫ Under.Hom.right f.unop).op
⊢ (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = (unop Z).hom.op
have rw₁ : Eq.{v₁ + 1} (α := op (unop Z).right ⟶ op X) ((Under.Hom.right f.unop).op ≫ (unop Y).hom.op)
  ((Under.Hom.right f.unop).op ≫ (unop Y).hom.op)
Tactic: rw [← Under.w f.unop, op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
Z Y : Under.{v₁, u₁} (op X)
f : Z ⟶ Y
⊢ (Hom.right f).unop ≫ (unop (op (Over.mk Z.hom.unop))).hom = (unop (op (Over.mk Y.hom.unop))).hom
have dsimp : (Hom.right f).unop ≫ Z.hom.unop = Y.hom.unop
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
Z Y : Under.{v₁, u₁} (op X)
f : Z ⟶ Y
⊢ (Hom.right f).unop ≫ Z.hom.unop = Y.hom.unop
have rw : (Z.hom ≫ Hom.right f).unop = Y.hom.unop
Tactic: rw [← unop_comp, Under.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : T
Z Y : Under.{v₁, u₁} (op X)
f : Z ⟶ Y
rw : (Z.hom ≫ Hom.right f).unop = Y.hom.unop
⊢ (Hom.right f).unop ≫ Z.hom.unop = Y.hom.unop
have rw₁ : Y.hom.unop = Y.hom.unop
Tactic: rw [← unop_comp, Under.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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
⊢ 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))
have dsimp : (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (unop Y).hom.op
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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
⊢ (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (unop Y).hom.op
have rw : (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (Over.Hom.left f.unop ≫ (unop Z).hom).op
Tactic: rw [← Over.w f.unop, op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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
⊢ (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (unop Y).hom.op
have 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)
Tactic: rw [← Over.w f.unop, op_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.OverClass (goal)
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
⊢ HomIsOver f S'
have comp_over : autoParam (f ≫ Y ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.OverClass (goal)
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
⊢ autoParam (f ≫ Y ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam
have comp_over : autoParam (f ≫ Y ↘ S ≫ S ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam
Tactic: rw [← comp_over (Y ↘ S), comp_over_assoc f, comp_over]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.OverClass (goal)
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
⊢ autoParam (f ≫ Y ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam
have comp_over₁ : autoParam (Eq.{v + 1} (α := X ⟶ S') (X ↘ S ≫ S ↘ S') (X ↘ S')) HomIsOver.comp_over._autoParam
Tactic: rw [← comp_over (Y ↘ S), comp_over_assoc f, comp_over]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.OverClass (goal)
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
⊢ autoParam (f ≫ Y ↘ S' = X ↘ S') HomIsOver.comp_over._autoParam
have comp_over₂ : autoParam (Eq.{v + 1} (α := X ⟶ S') (X ↘ S') (X ↘ S')) HomIsOver.comp_over._autoParam
Tactic: rw [← comp_over (Y ↘ S), comp_over_assoc f, comp_over]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ (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
have h : Hom.left
    ((fun (u : (map f).obj x ⟶ y) ↦ (homMk (pullback.lift (Hom.left u) x.hom sorry) sorry : x ⟶ (pullback f).obj y))
      ((fun (v : x ⟶ (pullback f).obj y) ↦ homMk (Hom.left v ≫ pullback.fst y.hom f) sorry) v)) =
  Hom.left v
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
      ((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
have h : pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom sorry = Hom.left v
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ = Hom.left v
have h : CategoryStruct.comp (Y := Limits.pullback y.hom f) (pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom sorry)
    (pullback.fst y.hom f) =
  Hom.left v ≫ pullback.fst y.hom f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom ⋯ = Hom.left v
have h₁ : CategoryStruct.comp (Y := Limits.pullback y.hom f) (pullback.lift (Hom.left v ≫ pullback.fst y.hom f) x.hom sorry)
    (pullback.snd y.hom f) =
  Hom.left v ≫ pullback.snd y.hom f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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)
have simp : Epi (homMk (pullback.fst Z.hom f) sorry)
Tactic: simp only [Functor.comp_obj, Functor.id_obj, mapPullbackAdj_counit_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (hypothesis)
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)
⊢ (pullback f).Faithful
have this : ∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = ((map f).obj y).hom
have simp : x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ y.hom
Tactic: simp only [map_obj_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ y.hom
have rw : x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ ((pushout f).obj x).hom ≫ Hom.right u
Tactic: rw [← Under.w u]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ ((pushout f).obj x).hom ≫ Hom.right u
have simp : x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ pushout.inr x.hom f ≫ Hom.right u
Tactic: simp only [map_obj_right, pushout_obj, mk_right, mk_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ pushout.inr x.hom f ≫ Hom.right u
have rw : (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ pushout.inr x.hom f ≫ Hom.right u
have rw₁ : (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ x.hom ≫ pushout.inl x.hom f ≫ Hom.right u = f ≫ pushout.inr x.hom f ≫ Hom.right u
have rw₂ : (f ≫ pushout.inr x.hom f) ≫ Hom.right u = (f ≫ pushout.inr x.hom f) ≫ Hom.right u
Tactic: rw [← assoc, ← assoc, pushout.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ (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
have h : Hom.right
    ((fun (v : x ⟶ (map f).obj y) ↦ (homMk (pushout.desc (Hom.right v) y.hom sorry) sorry : (pushout f).obj x ⟶ y))
      ((fun (u : (pushout f).obj x ⟶ y) ↦ homMk (pushout.inl x.hom f ≫ Hom.right u) sorry) u)) =
  Hom.right u
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ 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
have h : pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom sorry = Hom.right u
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = Hom.right u
have 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 sorry) =
  pushout.inl x.hom f ≫ Hom.right u
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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
⊢ pushout.desc (pushout.inl x.hom f ≫ Hom.right u) y.hom ⋯ = Hom.right u
have 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 sorry) =
  pushout.inr x.hom f ≫ Hom.right u
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (goal)
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)
have simp : Mono (homMk (pushout.inl Z.hom f) sorry)
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Pullback (hypothesis)
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)
⊢ (pushout f).Faithful
have this : ∀ (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
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Presheaf.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A F G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : Functor.obj yoneda X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
⊢ Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (μ.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (G.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X)) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (G.obj (op X)))
            u :
          (fun (X : Type v) ↦ X) (G.obj (op X))) :
      (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
have rw : Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X) ≫ μ.app (op X)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → A.obj (op X))
      u :
    A.obj (op X))
  ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
Tactic: rw [← comp_apply, ← NatTrans.comp_app, hε, h.app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Presheaf.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A F G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : Functor.obj yoneda X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
rw :
  Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X) ≫ μ.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → A.obj (op X))
        u :
      A.obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
⊢ Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (μ.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (G.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X)) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (G.obj (op X)))
            u :
          (fun (X : Type v) ↦ X) (G.obj (op X))) :
      (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
have rw₁ : Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((ε ≫ μ).app (op X)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → A.obj (op X))
      u :
    A.obj (op X))
  ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
Tactic: rw [← comp_apply, ← NatTrans.comp_app, hε, h.app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Presheaf.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A F G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : Functor.obj yoneda X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
rw :
  Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X) ≫ μ.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → A.obj (op X))
        u :
      A.obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
rw₁ :
  Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((ε ≫ μ).app (op X)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → A.obj (op X))
        u :
      A.obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
⊢ Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (μ.app (op X)) :
          (a : (fun (X : Type v) ↦ X) (G.obj (op X))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X)) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (G.obj (op X)))
            u :
          (fun (X : Type v) ↦ X) (G.obj (op X))) :
      (fun (X : Type v) ↦ X) (A.obj (op X)))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
have rw₂ : Eq (α := (fun (X : Type v) ↦ X) (A.obj (op X)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → A.obj (op X))
      u :
    A.obj (op X))
  ((yonedaEquiv : (a : yoneda.obj X ⟶ A) → A.obj (op X)) s : A.obj (op X))
Tactic: rw [← comp_apply, ← NatTrans.comp_app, hε, h.app]