awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : T
f_1 g_1 : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g_1
X Y : T
f g : X ⟶ Y
h : f = g
A : Under.{v₁, u₁} Y
⊢ (map f).obj A = (map g).obj A
have rw : (map g).obj A = (map g).obj A
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
Y : Under.{v₁, u₁} X
⊢ Hom.right (Limits.IsInitial.to mkIdInitial Y) = Y.hom
have rw : Hom.right (homMk Y.hom sorry) = Y.hom
Tactic: rw [mkIdInitial.hom_ext (mkIdInitial.to Y) (homMk Y.hom)]
-- 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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
⊢ Epi (Hom.right k)
have refine : ∀ {Y : T} (l m : g.right ⟶ Y) (a : Hom.right k ≫ l = Hom.right k ≫ m), l = m
Tactic: refine ⟨fun {Y : T} l m a => ?_⟩
-- 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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ g.hom ≫ l = (mk (g.hom ≫ m)).hom
have dsimp : g.hom ≫ l = g.hom ≫ m
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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ g.hom ≫ l = g.hom ≫ m
have rw : (f.hom ≫ Hom.right k) ≫ l = (f.hom ≫ Hom.right k) ≫ m
Tactic: rw [← Under.w k, Category.assoc, a, Category.assoc]
-- 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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
rw : (f.hom ≫ Hom.right k) ≫ l = (f.hom ≫ Hom.right k) ≫ m
⊢ g.hom ≫ l = g.hom ≫ m
have rw₁ : f.hom ≫ Hom.right k ≫ l = (f.hom ≫ Hom.right k) ≫ m
Tactic: rw [← Under.w k, Category.assoc, a, Category.assoc]
-- 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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
rw : (f.hom ≫ Hom.right k) ≫ l = (f.hom ≫ Hom.right k) ≫ m
rw₁ : f.hom ≫ Hom.right k ≫ l = (f.hom ≫ Hom.right k) ≫ m
⊢ g.hom ≫ l = g.hom ≫ m
have rw₂ : f.hom ≫ Hom.right k ≫ m = (f.hom ≫ Hom.right k) ≫ m
Tactic: rw [← Under.w k, Category.assoc, a, Category.assoc]
-- 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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
rw : (f.hom ≫ Hom.right k) ≫ l = (f.hom ≫ Hom.right k) ≫ m
rw₁ : f.hom ≫ Hom.right k ≫ l = (f.hom ≫ Hom.right k) ≫ m
rw₂ : f.hom ≫ Hom.right k ≫ m = (f.hom ≫ Hom.right k) ≫ m
⊢ g.hom ≫ l = g.hom ≫ m
have rw₃ : f.hom ≫ Hom.right k ≫ m = f.hom ≫ Hom.right k ≫ m
Tactic: rw [← Under.w k, Category.assoc, a, Category.assoc]
-- 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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ l = m
have suffices : l' = homMk m sorry
Tactic: suffices l' = (homMk m) by apply congrArg CommaMorphism.right this
-- 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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ l' = homMk m ⋯
have rw : k ≫ l' = k ≫ homMk m sorry
Tactic: rw [← cancel_epi k]
-- 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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Under.{v₁, u₁} X
k : f ⟶ g
inst_2 : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ k ≫ l' = k ≫ homMk m ⋯
have h : Hom.right (k ≫ l') = Hom.right (k ≫ homMk m sorry)
Tactic: ext
-- 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
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v_1, u₂, u_1} D E
X_1 Y : Under.{v₁, u₁} X
f : X_1 ⟶ Y
⊢ Eq (α := Functor.obj (post (F ⋙ G)) X_1 ⟶ Functor.obj (post F ⋙ post G) Y)
    (Functor.map (post (F ⋙ G)) f ≫
      Iso.hom
        ((fun (X_2 : Under.{v₁, u₁} X) ↦
            (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
              Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
          Y))
    (Iso.hom
        ((fun (X_2 : Under.{v₁, u₁} X) ↦
            (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
              Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
          X_1) ≫
      Functor.map (post F ⋙ post G) f)
have h : Eq (α := (Functor.obj (post (F ⋙ G)) X_1).right ⟶ (Functor.obj (post F ⋙ post G) Y).right)
  (Hom.right
    (Functor.map (post (F ⋙ G)) f ≫
      Iso.hom
        ((fun (X_2 : Under.{v₁, u₁} X) ↦
            (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
              Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
          Y)))
  (Hom.right
    (Iso.hom
        ((fun (X_2 : Under.{v₁, u₁} X) ↦
            (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
              Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
          X_1) ≫
      Functor.map (post F ⋙ post G) f))
Tactic: ext
-- 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
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v_1, u₂, u_1} D E
X_1 Y : Under.{v₁, u₁} X
f : X_1 ⟶ Y
⊢ Eq (α := (Functor.obj (post (F ⋙ G)) X_1).right ⟶ (Functor.obj (post F ⋙ post G) Y).right)
    (Hom.right
      (Functor.map (post (F ⋙ G)) f ≫
        Iso.hom
          ((fun (X_2 : Under.{v₁, u₁} X) ↦
              (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
                Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
            Y)))
    (Hom.right
      (Iso.hom
          ((fun (X_2 : Under.{v₁, u₁} X) ↦
              (Iso.refl (Functor.obj (post (F ⋙ G)) X_2) :
                Functor.obj (post (F ⋙ G)) X_2 ≅ Functor.obj (post (F ⋙ G)) X_2))
            X_1) ≫
        Functor.map (post F ⋙ post G) f))
have h : Hom.right (Functor.map (post (F ⋙ G)) f) ≫ 𝟙 (Functor.obj (post (F ⋙ G)) Y).right =
  𝟙 (Functor.obj (post (F ⋙ G)) X_1).right ≫ Hom.right (Functor.map (post F ⋙ post G) f)
Tactic: dsimp only [Iso.refl_hom, Under.comp_right, Under.id_right]
-- 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
f_1 g_1 : Under.{v₁, u₁} X
φ : f_1 ⟶ g_1
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
A B : Under.{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)
⊢ f = g
have h₁ : Hom.right f = Hom.right g
Tactic: ext
-- 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
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Under.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
⊢ ∃ (a : A ⟶ B), Functor.map (post F) a = f
have obtain : ∀ (a : A.right ⟶ B.right) (ha : F.map a = Hom.right f), ∃ (a : A ⟶ B), Functor.map (post F) a = f
Tactic: obtain ⟨a, ha⟩ := F.map_surjective f.right
-- 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
f_1 g : Under.{v₁, u₁} X
φ : f_1 ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Faithful
inst_3 : F.Full
A B : Under.{v₁, u₁} X
f : Functor.obj (post F) A ⟶ Functor.obj (post F) B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ Functor.map (post F) (homMk a ⋯) = f
have h : Hom.right (Functor.map (post F) (homMk a sorry)) = Hom.right f
Tactic: ext
-- 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
f g : Under.{v₁, u₁} X
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Under.{v₂, u₂} (F.obj X)
⊢ Functor.essImage (post F) B
have obtain : ∀ (B' : T) (e : F.obj B' ≅ B.right), Functor.essImage (post F) B
Tactic: obtain ⟨B', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.right
-- 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
f g : Under.{v₁, u₁} X
φ : f ⟶ g
F : Functor.{v₁, v₂, u₁, u₂} T D
inst_2 : F.Full
inst_3 : F.EssSurj
B : Under.{v₂, u₂} (F.obj X)
B' : T
e : F.obj B' ≅ B.right
⊢ Functor.essImage (post F) B
have obtain : ∀ (f : X ⟶ B') (hf : F.map f = B.hom ≫ e.inv), Functor.essImage (post F) B
Tactic: obtain ⟨f, hf⟩ := F.map_surjective (B.hom ≫ e.inv)
-- 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_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)
f : x ⟶ x_1
⊢ Eq (α :=
    Functor.obj (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) x ⟶
      (post F ⋙ post G ⋙ map (a.unit.app X)).obj x_1)
    (Functor.map (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) f ≫ homMk (a.unit.app x_1.right) ⋯)
    (homMk (a.unit.app x.right) ⋯ ≫ (post F ⋙ post G ⋙ map (a.unit.app X)).map f)
have h : Eq (α :=
  (Functor.obj (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) x).right ⟶
    ((post F ⋙ post G ⋙ map (a.unit.app X)).obj x_1).right)
  (Hom.right
    (Functor.map (𝟭 (Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) f ≫ homMk (a.unit.app x_1.right) sorry))
  (Hom.right (homMk (a.unit.app x.right) sorry ≫ (post F ⋙ post G ⋙ map (a.unit.app X)).map f))
Tactic: ext
-- 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_1 : T
f_1 g : Under.{v₁, u₁} X_1
φ : f_1 ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
x x_1 : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))
f : x ⟶ x_1
⊢ ((post G ⋙ map (a.unit.app X)) ⋙ post F).map f ≫ homMk (a.counit.app x_1.right) ⋯ =
    homMk (a.counit.app x.right) ⋯ ≫ Functor.map (𝟭 (Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)))) f
have h : Hom.right (((post G ⋙ map (a.unit.app X)) ⋙ post F).map f ≫ homMk (a.counit.app x_1.right) sorry) =
  Hom.right
    (homMk (a.counit.app x.right) sorry ≫ Functor.map (𝟭 (Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)))) f)
Tactic: ext
-- 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_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)
⊢ Eq (α := Functor.obj (post F) A ⟶ Functor.obj (post F) A)
    (CategoryStruct.comp (Y := Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) A)))
        (Functor.map (post F)
          (NatTrans.app
            { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) ⋯,
              naturality := ⋯ }
            A))
        (NatTrans.app
          {
            app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
              homMk (a.counit.app A.right) ⋯,
            naturality := ⋯ }
          (Functor.obj (post F) A)) :
      Functor.obj (post F) A ⟶ Functor.obj (post F) A)
    (𝟙 (Functor.obj (post F) A) : Functor.obj (post F) A ⟶ Functor.obj (post F) A)
have h : Hom.right
    (CategoryStruct.comp (Y := Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) A)))
      (Functor.map (post F)
        (NatTrans.app
          { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) sorry,
            naturality := sorry }
          A))
      (NatTrans.app
        {
          app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
            homMk (a.counit.app A.right) sorry,
          naturality := sorry }
        (Functor.obj (post F) A))) =
  Hom.right (𝟙 (Functor.obj (post F) A))
Tactic: ext
-- 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_1 : T
f g : Under.{v₁, u₁} X_1
φ : f ⟶ g
F_1 : Functor.{v₁, v₂, u₁, u₂} T D
X : T
F : Functor.{v₁, v₂, u₁, u₂} T D
G : Functor.{v₂, v₁, u₂, u₁} D T
a : F ⊣ G
A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))
⊢ Eq.{v₁ + 1} (α := (post G ⋙ map (a.unit.app X)).obj A ⟶ (post G ⋙ map (a.unit.app X)).obj A)
    (CategoryStruct.comp (Y :=
        (post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj A)))
        (NatTrans.app
          { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) ⋯,
            naturality := ⋯ }
          ((post G ⋙ map (a.unit.app X)).obj A))
        ((post G ⋙ map (a.unit.app X)).map
          (NatTrans.app
            {
              app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
                homMk (a.counit.app A.right) ⋯,
              naturality := ⋯ }
            A)) :
      (post G ⋙ map (a.unit.app X)).obj A ⟶ (post G ⋙ map (a.unit.app X)).obj A)
    (𝟙 ((post G ⋙ map (a.unit.app X)).obj A) :
      (post G ⋙ map (a.unit.app X)).obj A ⟶ (post G ⋙ map (a.unit.app X)).obj A)
have h : Hom.right
    (CategoryStruct.comp (Y :=
      (post G ⋙ map (a.unit.app X)).obj (Functor.obj (post F) ((post G ⋙ map (a.unit.app X)).obj A)))
      (NatTrans.app
        { app := fun (A : Under.{v₁, u₁} (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X)) ↦ homMk (a.unit.app A.right) sorry,
          naturality := sorry }
        ((post G ⋙ map (a.unit.app X)).obj A))
      ((post G ⋙ map (a.unit.app X)).map
        (NatTrans.app
          {
            app := fun (A : Under.{v₂, u₂} (F.obj (Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 T) X))) ↦
              homMk (a.counit.app A.right) sorry,
            naturality := sorry }
          A))) =
  Hom.right (𝟙 ((post G ⋙ map (a.unit.app X)).obj A))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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 : Under.{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 : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J
⊢ (liftCocone D s c p hp).ι.app j ≫ homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯ = t.ι.app j
have h : Hom.right ((liftCocone D s c p hp).ι.app j ≫ homMk (hc.desc (Functor.mapCocone (forget X) t)) sorry) = Hom.right (t.ι.app j)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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 : Under.{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 : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x = t.ι.app j
⊢ x = homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯
have h : Hom.right x = Hom.right (homMk (hc.desc (Functor.mapCocone (forget X) t)) sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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 : Under.{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 : Functor.obj (Functor.const J) X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x = t.ι.app j
⊢ Hom.right x = Hom.right (homMk (hc.desc (Functor.mapCocone (forget X) t)) ⋯)
have h : ∀ (j : J), c.ι.app j ≫ Hom.right x = c.ι.app j ≫ Hom.right (homMk (hc.desc (Functor.mapCocone (forget X) t)) sorry)
Tactic: refine hc.hom_ext (fun j ↦ ?_)
-- 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
F : Functor.{v₂, v₁, u₂, u₁} D T
Y : T
X : D
Y_1 Z : StructuredArrow X (proj Y F)
m : Y_1 ⟶ Z
⊢ Eq (α := X ⟶ (proj X (proj Y F) ⋙ proj Y F).obj Z)
    ((fun (g : StructuredArrow X (proj Y F)) ↦ g.hom) Y_1 ≫ (proj X (proj Y F) ⋙ proj Y F).map m)
    ((fun (g : StructuredArrow X (proj Y F)) ↦ g.hom) Z)
have this : Y_1.hom ≫ (proj Y F).map (Hom.right m) = Z.hom
Tactic: have := m.w
-- 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
F : Functor.{v₂, v₁, u₂, u₁} D T
Y : T
X : D
Y_1 Z : StructuredArrow Y (Under.forget X ⋙ F)
m : Y_1 ⟶ Z
⊢ Eq (α := Y ⟶ F.obj ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).obj Z))
    ((fun (g : StructuredArrow Y (Under.forget X ⋙ F)) ↦ g.hom) Y_1 ≫
      F.map ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).map m))
    ((fun (g : StructuredArrow Y (Under.forget X ⋙ F)) ↦ g.hom) Z)
have this : Y_1.hom ≫ (Under.forget X ⋙ F).map (Hom.right m) = Z.hom
Tactic: have := m.w
-- 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 : StructuredArrow (C := Under.{v₁, u₁} X.1) X.2 (Under.forget X.1)
m : Y ⟶ Z
⊢ Eq (α :=
    X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) (Functor.obj (proj X.2 (Under.forget X.1) ⋙ Under.forget X.1) Z))
    ((fun (f : StructuredArrow (C := Under.{v₁, u₁} X.1) X.2 (Under.forget X.1)) ↦ (f.right.hom, f.hom)) Y ≫
      Functor.map (Functor.diag T) (Functor.map (proj X.2 (Under.forget X.1) ⋙ Under.forget X.1) m))
    ((fun (f : StructuredArrow (C := Under.{v₁, u₁} X.1) X.2 (Under.forget X.1)) ↦ (f.right.hom, f.hom)) Z)
have this : Y.hom ≫ Functor.map (Under.forget X.1) (Hom.right m) = Z.hom
Tactic: have := m.w
-- 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
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
X : T
Y_1 Z : CostructuredArrow (proj F Y) X
m : Y_1 ⟶ Z
⊢ Eq (α := (proj (proj F Y) X ⋙ proj F Y).obj Y_1 ⟶ X)
    ((proj (proj F Y) X ⋙ proj F Y).map m ≫ (fun (g : CostructuredArrow (proj F Y) X) ↦ g.hom) Z)
    ((fun (g : CostructuredArrow (proj F Y) X) ↦ g.hom) Y_1)
have this : (proj F Y).map m.left ≫ Z.hom = Y_1.hom ≫ Functor.map (Functor.fromPUnit X) m.right
Tactic: have := m.w
-- 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
F : Functor.{v₁, v₂, u₁, u₂} T D
Y : D
X : T
Y_1 Z : CostructuredArrow (Over.forget X ⋙ F) Y
m : Y_1 ⟶ Z
⊢ Eq (α := F.obj ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).obj Y_1) ⟶ Y)
    (F.map ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).map m) ≫
      (fun (g : CostructuredArrow (Over.forget X ⋙ F) Y) ↦ g.hom) Z)
    ((fun (g : CostructuredArrow (Over.forget X ⋙ F) Y) ↦ g.hom) Y_1)
have this : (Over.forget X ⋙ F).map m.left ≫ Z.hom = Y_1.hom ≫ Functor.map (Functor.fromPUnit Y) m.right
Tactic: have := m.w
-- 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.{v₁, v₁, u₁, u₁} (Functor.diag T) X
m : Y ⟶ Z
⊢ Eq (α := Functor.obj (proj (Functor.diag T) X) Y ⟶ X.1)
    (Functor.map (proj (Functor.diag T) X) m ≫
      (fun (g : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X) ↦ g.hom.1) Z)
    ((fun (g : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X) ↦ g.hom.1) Y)
have this : Eq.{v₁ + 1} (α :=
  (Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left).1 ⟶
    (Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right).1)
  ((fun
        (x :
          Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left ⟶
            Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right) ↦
      x.1)
    (Functor.map (Functor.diag T) m.left ≫ Z.hom))
  ((fun
        (x :
          Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left ⟶
            Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right) ↦
      x.1)
    (Y.hom ≫ Functor.map (Functor.fromPUnit X) m.right))
Tactic: have := congrArg (·.1) m.w
-- 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.{v₁, v₁, u₁, u₁} (Functor.diag T) X
m : Y ⟶ Z
⊢ Eq (α :=
    Functor.obj (Over.forget X.1)
        (Functor.obj
          (Functor.toOver (proj (Functor.diag T) X) X.1
            (fun (g : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X) ↦ g.hom.1) ⋯)
          Y) ⟶
      X.2)
    (Functor.map (Over.forget X.1)
        (Functor.map
          (Functor.toOver (proj (Functor.diag T) X) X.1
            (fun (g : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X) ↦ g.hom.1) ⋯)
          m) ≫
      (fun (f : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X) ↦ f.hom.2) Z)
    ((fun (f : CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag T) X) ↦ f.hom.2) Y)
have this : Eq.{v₁ + 1} (α :=
  (Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left).2 ⟶
    (Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right).2)
  ((fun
        (x :
          Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left ⟶
            Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right) ↦
      x.2)
    (Functor.map (Functor.diag T) m.left ≫ Z.hom))
  ((fun
        (x :
          Functor.obj.{v₁, v₁, u₁, u₁} (Functor.diag T) Y.left ⟶
            Functor.obj.{0, v₁, 0, u₁} (Functor.fromPUnit X) Z.right) ↦
      x.2)
    (Y.hom ≫ Functor.map (Functor.fromPUnit X) m.right))
Tactic: have := congrArg (·.2) m.w