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
f_1 g_1 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
A B : Over.{v₁, u₁} X
f g : A ⟶ B
h : Eq (α := Functor.obj (post F) A ⟶ Functor.obj (post F) B) (Functor.map (post F) f) (Functor.map (post F) g)
h₁ : Hom.left f = Hom.left g
⊢ f = g

Tactic:
ext
-- 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
f_1 g_1 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
A B : Over.{v₁, u₁} X
f g : A ⟶ B
h : Eq (α := Functor.obj (post F) A ⟶ Functor.obj (post F) B) (Functor.map (post F) f) (Functor.map (post F) g)
⊢ Hom.left f = Hom.left g

Tactic:
F.map_injective (congrArg CommaMorphism.left h)

Premises used: congrArg, CategoryTheory.CommaMorphism.left, CategoryTheory.Functor.map_injective
-- 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
f_1 g_1 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
A B : Over.{v₁, u₁} X
f g : A ⟶ B
h : Eq (α := Functor.obj (post F) A ⟶ Functor.obj (post F) B) (Functor.map (post F) f) (Functor.map (post F) g)
⊢ Hom.left f = Hom.left g

Tactic:
exact F.map_injective (congrArg CommaMorphism.left h)

Premises used: congrArg, CategoryTheory.CommaMorphism.left, CategoryTheory.Functor.map_injective
-- 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
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Over.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
obtain : ∀ (a : A.left ⟶ B.left) (ha : F.map a = Hom.left f), ∃ (a : A ⟶ B), Functor.map (post F) a = f
⊢ ∃ (a : A ⟶ B), Functor.map (post F) a = f

Tactic:
obtain ⟨a, ha⟩ := F.map_surjective f.left

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.Functor.map_surjective
-- 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
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Over.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
a : A.left ⟶ B.left
ha : F.map a = Hom.left f
⊢ F.map (a ≫ B.hom) = F.map A.hom

Tactic:
simp [ha, dsimp% f.w]

Premises used: CategoryTheory.Over.Hom.w
-- 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
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Over.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
a : A.left ⟶ B.left
ha : F.map a = Hom.left f
⊢ ∃ (a : A ⟶ B), Functor.map (post F) a = f

Tactic:
exact ⟨Over.homMk a (F.map_injective (by simp [ha, dsimp% f.w])), by cat_disch⟩
-- 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
f g : Over.{v₁, u₁} X
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Over.{v₂, u₂} (F.obj X)
obtain : ∀ (A' : T) (e : F.obj A' ≅ B.left), Functor.essImage (post F) B
⊢ Functor.essImage (post F) B

Tactic:
obtain ⟨A', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.left

Premises used: CategoryTheory.Functor.EssSurj.mem_essImage, CategoryTheory.Over.left
-- 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
f g : Over.{v₁, u₁} X
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Over.{v₂, u₂} (F.obj X)
A' : T
e : F.obj A' ≅ B.left
obtain : ∀ (f : A' ⟶ X) (hf : F.map f = e.hom ≫ B.hom), Functor.essImage (post F) B
⊢ Functor.essImage (post F) B

Tactic:
obtain ⟨f, hf⟩ := F.map_surjective (e.hom ≫ B.hom)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Over.hom, CategoryTheory.Functor.map_surjective
-- 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
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Over.{v₂, u₂} (F.obj X)
A' : T
e : F.obj A' ≅ B.left
f : A' ⟶ X
hf : F.map f = e.hom ≫ B.hom
⊢ Functor.essImage (post F) B

Tactic:
⟨Over.mk f, ⟨Over.isoMk e⟩⟩

Premises used: CategoryTheory.Over.mk, CategoryTheory.Functor.essImage, Nonempty.intro, CategoryTheory.Over.isoMk, Exists.intro
-- 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
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Over.{v₂, u₂} (F.obj X)
A' : T
e : F.obj A' ≅ B.left
f : A' ⟶ X
hf : F.map f = e.hom ≫ B.hom
⊢ Functor.essImage (post F) B

Tactic:
exact ⟨Over.mk f, ⟨Over.isoMk e⟩⟩
-- 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
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
h : F.FullyFaithful
A B : Over.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
⊢ F.map (h.preimage (Hom.left f) ≫ B.hom) = F.map A.hom

Tactic:
simpa using Over.w f

Premises used: CategoryTheory.Over.w
-- 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
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y)
f : x ⟶ x_1
h :
  Eq (α :=
    ((post G ⋙ post F ⋙ map (a.counit.app Y)).obj x).left ⟶
      (Functor.obj (𝟭 (Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y))) x_1).left)
    (Hom.left ((post G ⋙ post F ⋙ map (a.counit.app Y)).map f ≫ homMk (a.counit.app x_1.left) ⋯))
    (Hom.left
      (homMk (a.counit.app x.left) ⋯ ≫ Functor.map (𝟭 (Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y))) f))
⊢ Eq (α :=
    (post G ⋙ post F ⋙ map (a.counit.app Y)).obj x ⟶
      Functor.obj (𝟭 (Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y))) x_1)
    ((post G ⋙ post F ⋙ map (a.counit.app Y)).map f ≫ homMk (a.counit.app x_1.left) ⋯)
    (homMk (a.counit.app x.left) ⋯ ≫ Functor.map (𝟭 (Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y))) f)

Tactic:
ext
-- 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
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y)
f : x ⟶ x_1
⊢ Eq (α :=
    ((post G ⋙ post F ⋙ map (a.counit.app Y)).obj x).left ⟶
      (Functor.obj (𝟭 (Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y))) x_1).left)
    (Hom.left ((post G ⋙ post F ⋙ map (a.counit.app Y)).map f ≫ homMk (a.counit.app x_1.left) ⋯))
    (Hom.left
      (homMk (a.counit.app x.left) ⋯ ≫ Functor.map (𝟭 (Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y))) f))

Tactic:
a.counit_naturality f.left

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.Adjunction.counit_naturality
-- 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
f_1 g : Over.{v₁, u₁} X
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y)
f : x ⟶ x_1
⊢ Eq (α :=
    ((post G ⋙ post F ⋙ map (a.counit.app Y)).obj x).left ⟶
      (Functor.obj (𝟭 (Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y))) x_1).left)
    (Hom.left ((post G ⋙ post F ⋙ map (a.counit.app Y)).map f ≫ homMk (a.counit.app x_1.left) ⋯))
    (Hom.left
      (homMk (a.counit.app x.left) ⋯ ≫ Functor.map (𝟭 (Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y))) f))

Tactic:
exact a.counit_naturality f.left

Premises used: CategoryTheory.Over.Hom.left, CategoryTheory.Adjunction.counit_naturality
-- 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
f g : Over.{v₁, u₁} X
φ : f ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
A : Over.{v₁, u₁} (G.obj Y)
h :
  Hom.left
      ((post F ⋙ map (a.counit.app Y)).map
          (NatTrans.app
            { app := fun (A : Over.{v₁, u₁} (G.obj Y)) ↦ homMk (a.unit.app A.left) ⋯, naturality := ⋯ :
              NatTrans (𝟭 (Over.{v₁, u₁} (G.obj Y))) ((post F ⋙ map (a.counit.app Y)) ⋙ post G) }
            A) ≫
        NatTrans.app
          { app := fun (A : Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y)) ↦ homMk (a.counit.app A.left) ⋯,
            naturality := ⋯ }
          ((post F ⋙ map (a.counit.app Y)).obj A)) =
    Hom.left (𝟙 ((post F ⋙ map (a.counit.app Y)).obj A))
⊢ (post F ⋙ map (a.counit.app Y)).map
        (NatTrans.app
          { app := fun (A : Over.{v₁, u₁} (G.obj Y)) ↦ homMk (a.unit.app A.left) ⋯, naturality := ⋯ :
            NatTrans (𝟭 (Over.{v₁, u₁} (G.obj Y))) ((post F ⋙ map (a.counit.app Y)) ⋙ post G) }
          A) ≫
      NatTrans.app
        { app := fun (A : Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y)) ↦ homMk (a.counit.app A.left) ⋯,
          naturality := ⋯ }
        ((post F ⋙ map (a.counit.app Y)).obj A) =
    𝟙 ((post F ⋙ map (a.counit.app Y)).obj A)

Tactic:
ext
-- 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
f g : Over.{v₁, u₁} X
φ : f ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
A : Over.{v₁, u₁} (G.obj Y)
⊢ Hom.left
      ((post F ⋙ map (a.counit.app Y)).map
          (NatTrans.app
            { app := fun (A : Over.{v₁, u₁} (G.obj Y)) ↦ homMk (a.unit.app A.left) ⋯, naturality := ⋯ :
              NatTrans (𝟭 (Over.{v₁, u₁} (G.obj Y))) ((post F ⋙ map (a.counit.app Y)) ⋙ post G) }
            A) ≫
        NatTrans.app
          { app := fun (A : Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y)) ↦ homMk (a.counit.app A.left) ⋯,
            naturality := ⋯ }
          ((post F ⋙ map (a.counit.app Y)).obj A)) =
    Hom.left (𝟙 ((post F ⋙ map (a.counit.app Y)).obj A))

Tactic:
simp [-Functor.id_obj]

Premises used: CategoryTheory.Functor.id_obj
-- 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
f g : Over.{v₁, u₁} X
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
G : Functor.{v₂, v₁, u₂, u₁} D T
inst_2 : G.IsRightAdjoint
⊢ Functor.IsRightAdjoint (C := Over.{v₁, u₁} (G.obj Y)) (post G)

Tactic:
let ⟨F, ⟨a⟩⟩ := ‹G.IsRightAdjoint›; ⟨_, ⟨postAdjunctionRight a⟩⟩

Premises used: CategoryTheory.Over.map, CategoryTheory.Functor.comp, CategoryTheory.Functor.IsRightAdjoint, CategoryTheory.Over.postAdjunctionRight, Nonempty.intro, CategoryTheory.Adjunction.counit, CategoryTheory.Over.post, Exists.intro, _private.0.CategoryTheory.Over.isRightAdjoint_post.match_1, CategoryTheory.Functor.IsRightAdjoint.mk, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f_1 g : Over.{v₁, u₁} X_1
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : D ⟶ Functor.obj (Functor.const J) X
X_2 Y : J
f : X_2 ⟶ Y
⊢ D.map f ≫ (mk (s.app Y)).hom = (mk (s.app X_2)).hom

Tactic:
simpa using s.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Over.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : D ⟶ Functor.obj (Functor.const J) X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
j : J := Classical.arbitrary J
⊢ hc.lift (Functor.mapCone (forget X) t) ≫ (liftCone D s c p hp).pt.hom = t.pt.hom

Tactic:
simp [← hp j, dsimp% (t.π.app j).w, dsimp% hc.fac_assoc ((forget X).mapCone t) j]

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Over.forget, CategoryTheory.Limits.IsLimit.fac_assoc, CategoryTheory.Over.Hom.w, CategoryTheory.Functor.mapCone, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Over.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : D ⟶ Functor.obj (Functor.const J) X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
j : J
h : Hom.left (homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯ ≫ (liftCone D s c p hp).π.app j) = Hom.left (t.π.app j)
⊢ homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯ ≫ (liftCone D s c p hp).π.app j = t.π.app j

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Over.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : D ⟶ Functor.obj (Functor.const J) X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
j : J
⊢ Hom.left (homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯ ≫ (liftCone D s c p hp).π.app j) = Hom.left (t.π.app j)

Tactic:
simp [dsimp% hc.fac ((forget X).mapCone t) j]

Premises used: CategoryTheory.Over.forget, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Over.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : D ⟶ Functor.obj (Functor.const J) X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
x : t.pt ⟶ (liftCone D s c p hp).pt
hm : ∀ (j : J), x ≫ (liftCone D s c p hp).π.app j = t.π.app j
h : Hom.left x = Hom.left (homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯)
⊢ x = homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Over.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : D ⟶ Functor.obj (Functor.const J) X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
x : t.pt ⟶ (liftCone D s c p hp).pt
hm : ∀ (j : J), x ≫ (liftCone D s c p hp).π.app j = t.π.app j
⊢ Hom.left x = Hom.left (homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯)

Tactic:
hc.hom_ext (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Over.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : D ⟶ Functor.obj (Functor.const J) X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
x : t.pt ⟶ (liftCone D s c p hp).pt
hm : ∀ (j : J), x ≫ (liftCone D s c p hp).π.app j = t.π.app j
h : ∀ (j : J), Hom.left x ≫ c.π.app j = Hom.left (homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯) ≫ c.π.app j
⊢ Hom.left x = Hom.left (homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯)

Tactic:
refine hc.hom_ext (fun j ↦ ?_)

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
X_1 : T
f g : Over.{v₁, u₁} X_1
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D_1
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : Nonempty J
D : Functor.{v_1, v₁, u_1, u₁} J T
X : T
s : D ⟶ Functor.obj (Functor.const J) X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
x : t.pt ⟶ (liftCone D s c p hp).pt
hm : ∀ (j : J), x ≫ (liftCone D s c p hp).π.app j = t.π.app j
j : J
⊢ Hom.left x ≫ c.π.app j = Hom.left (homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯) ≫ c.π.app j

Tactic:
simp [dsimp% hc.fac ((forget X).mapCone t) j, ← hm]

Premises used: CategoryTheory.Over.forget, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
inst_2 : F.Faithful
⊢ (toOver F X).Faithful

Tactic:
show (CostructuredArrow.pre _ _ _).Faithful from inferInstance

Premises used: CategoryTheory.Over, CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.toOver
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
inst_2 : F.Full
⊢ (toOver F X).Full

Tactic:
show (CostructuredArrow.pre _ _ _).Full from inferInstance

Premises used: CategoryTheory.Over, CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.toOver
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
inst_2 : F.EssSurj
⊢ (toOver F X).EssSurj

Tactic:
show (CostructuredArrow.pre _ _ _).EssSurj from inferInstance

Premises used: CategoryTheory.Over, CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.toOver
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
inst_2 : F.IsEquivalence
⊢ (toOver F X).IsEquivalence

Tactic:
CostructuredArrow.isEquivalence_pre _ _ _

Premises used: CategoryTheory.Over, CategoryTheory.CostructuredArrow.isEquivalence_pre, CategoryTheory.Functor.comp, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.toOver
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
Y : Over.{v₁, u₁} X
X_1 Y_1 : CostructuredArrow (toOver F X) Y
f : X_1 ⟶ Y_1
rw : F.map f.left.left ≫ (mk (Over.Hom.left Y_1.hom)).hom = (mk (Over.Hom.left ((toOver F X).map f.left ≫ Y_1.hom))).hom
⊢ F.map f.left.left ≫ (mk (Over.Hom.left Y_1.hom)).hom = (mk (Over.Hom.left X_1.hom)).hom

Tactic:
rw [← CostructuredArrow.w f]

Premises used: CategoryTheory.CostructuredArrow.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
Y : Over.{v₁, u₁} X
X_1 Y_1 : CostructuredArrow (toOver F X) Y
f : X_1 ⟶ Y_1
⊢ F.map f.left.left ≫ (mk (Over.Hom.left Y_1.hom)).hom = (mk (Over.Hom.left ((toOver F X).map f.left ≫ Y_1.hom))).hom

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
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
Y : Over.{v₁, u₁} X
X_1 Y_1 : CostructuredArrow F Y.left
f : X_1 ⟶ Y_1
h :
  Over.Hom.left ((toOver F X).map (homMk f.left ⋯) ≫ hom (mk (Y := mk (Y_1.hom ≫ Y.hom)) (Over.homMk Y_1.hom ⋯))) =
    Over.Hom.left (hom (mk (Y := mk (X_1.hom ≫ Y.hom)) (Over.homMk X_1.hom ⋯)))
⊢ (toOver F X).map (homMk f.left ⋯) ≫ hom (mk (Y := mk (Y_1.hom ≫ Y.hom)) (Over.homMk Y_1.hom ⋯)) =
    hom (mk (Y := mk (X_1.hom ≫ Y.hom)) (Over.homMk X_1.hom ⋯))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
Y : Over.{v₁, u₁} X
X_1 Y_1 : CostructuredArrow F Y.left
f : X_1 ⟶ Y_1
⊢ Over.Hom.left ((toOver F X).map (homMk f.left ⋯) ≫ hom (mk (Y := mk (Y_1.hom ≫ Y.hom)) (Over.homMk Y_1.hom ⋯))) =
    Over.Hom.left (hom (mk (Y := mk (X_1.hom ≫ Y.hom)) (Over.homMk X_1.hom ⋯)))

Tactic:
CostructuredArrow.w f

Premises used: CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.w, CategoryTheory.CostructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
Y : Over.{v₁, u₁} X
X_1 Y_1 : CostructuredArrow F Y.left
f : X_1 ⟶ Y_1
⊢ Over.Hom.left ((toOver F X).map (homMk f.left ⋯) ≫ hom (mk (Y := mk (Y_1.hom ≫ Y.hom)) (Over.homMk Y_1.hom ⋯))) =
    Over.Hom.left (hom (mk (Y := mk (X_1.hom ≫ Y.hom)) (Over.homMk X_1.hom ⋯)))

Tactic:
exact CostructuredArrow.w f

Premises used: CategoryTheory.CostructuredArrow.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₂, v₁, u₂, u₁} D T
X : T
Y : Over.{v₁, u₁} X
f : CostructuredArrow (toOver F X) Y
⊢ F.map (Iso.hom (Iso.refl (Functor.obj (𝟭 (CostructuredArrow (toOver F X) Y)) f).left.left)) ≫
      ((costructuredArrowToOverEquivalence.functor F Y ⋙ costructuredArrowToOverEquivalence.inverse F Y).obj
            f).left.hom =
    (Functor.obj (𝟭 (CostructuredArrow (toOver F X) Y)) f).left.hom

Tactic:
simpa using f.hom.w

Premises used: CategoryTheory.CostructuredArrow.hom, CategoryTheory.Over.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f g : Under.{v₁, u₁} X
φ : f ⟶ g
⊢ f.hom ≫ Hom.right φ = g.hom

Tactic:
simpa using (CommaMorphism.w φ).symm

Premises used: CategoryTheory.CommaMorphism.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
f g : Under.{v₁, u₁} X
φ : f ⟶ g
⊢ f.hom ≫ right φ = g.hom

Tactic:
Under.w φ

Premises used: CategoryTheory.Under.w
-- Module: Mathlib.CategoryTheory.Comma.Over.Basic
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Under.{v₁, u₁} X
f g : U ⟶ V
h : Hom.right f = Hom.right g
let :
  ∀ (left : U.left ⟶ V.left) (b : U.right ⟶ V.right)
    (w : Functor.map (Functor.fromPUnit X) left ≫ V.hom = U.hom ≫ Functor.map (𝟭 T) b)
    (h : Hom.right { left := left, right := b, w := w : CommaMorphism U V } = Hom.right g),
    { left := left, right := b, w := w : CommaMorphism U V } = g
⊢ f = g

Tactic:
let ⟨_,b,_⟩ := f