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
X : T
U V : Over.{v₁, u₁} X
f g : U ⟶ V
left : U.left ⟶ V.left
b : U.right ⟶ V.right
w : Functor.map (𝟭 T) left ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) b
h : Hom.left { left := left, right := b, w := w : CommaMorphism U V } = Hom.left g
⊢ { left := left, right := b, w := w : CommaMorphism U V } = g
have let : ∀ (left_1 : U.left ⟶ V.left) (e : U.right ⟶ V.right)
  (w_1 : Functor.map (𝟭 T) left_1 ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) e)
  (h :
    Hom.left { left := left, right := b, w := w : CommaMorphism U V } =
      Hom.left { left := left_1, right := e, w := w_1 }),
  { left := left, right := b, w := w : CommaMorphism U V } = { left := left_1, right := e, w := w_1 }
Tactic: let ⟨_,e,_⟩ := g
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Over.{v₁, u₁} X
f g : U ⟶ V
left : U.left ⟶ V.left
b : U.right ⟶ V.right
w : Functor.map (𝟭 T) left ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) b
left_1 : U.left ⟶ V.left
e : U.right ⟶ V.right
w_1 : Functor.map (𝟭 T) left_1 ≫ V.hom = U.hom ≫ Functor.map (Functor.fromPUnit X) e
h :
  Hom.left { left := left, right := b, w := w : CommaMorphism U V } = Hom.left { left := left_1, right := e, w := w_1 }
⊢ { left := left, right := b, w := w : CommaMorphism U V } = { left := left_1, right := e, w := w_1 }
have e_right : b = e
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V W : Over.{v₁, u₁} X
f : U.left ⟶ V.left
g : V.left ⟶ W.left
w_f : f ≫ V.hom = U.hom
w_g : g ≫ W.hom = V.hom
⊢ homMk (f ≫ g) ⋯ = homMk f w_f ≫ homMk g w_g
have h : Hom.left (homMk (f ≫ g) sorry) = Hom.left (homMk f w_f ≫ homMk g w_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_1 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
h : f = g
⊢ f.left = g.left
have rw : g.left = g.left
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
f g : Over.{v₁, u₁} X
h : f = g
⊢ Hom.left (eqToHom h) = eqToHom ⋯
have subst : Hom.left (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
Y : T
x : Over.{v₁, u₁} Y
⊢ Functor.obj (map (𝟙 Y)) x = Functor.obj (𝟭 (Over.{v₁, u₁} Y)) x
have simp : { left := x.left, right := x.right, hom := x.hom : Comma.{v₁, 0, v₁, u₁, 0, u₁} (𝟭 T) (Functor.fromPUnit Y) } = x
Tactic: simp [map, Comma.mapRight]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
Y : T
x : Over.{v₁, u₁} Y
⊢ NatTrans.app (Iso.hom (mapId Y)) x = eqToHom ⋯
have h : Hom.left (NatTrans.app (Iso.hom (mapId Y)) x) = Hom.left (eqToHom sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
x : Over.{v₁, u₁} X
⊢ (mapComp f g).hom.app x = eqToHom ⋯
have h : Hom.left ((mapComp f g).hom.app x) = Hom.left (eqToHom sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
Y : Over.{v₁, u₁} X
⊢ Hom.left (Limits.IsTerminal.from mkIdTerminal Y) = Y.hom
have rw : Hom.left (homMk Y.hom sorry) = Y.hom
Tactic: rw [mkIdTerminal.hom_ext (mkIdTerminal.from 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
⊢ Mono (Hom.left k)
have refine : ∀ {Y : T} (l m : Y ⟶ f.left) (a : l ≫ Hom.left k = m ≫ Hom.left k), 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ l ≫ f.hom = (mk (m ≫ f.hom)).hom
have dsimp : l ≫ f.hom = m ≫ f.hom
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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ l ≫ f.hom = m ≫ f.hom
have rw : l ≫ Hom.left k ≫ g.hom = m ≫ Hom.left k ≫ g.hom
Tactic: rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
rw : l ≫ Hom.left k ≫ g.hom = m ≫ Hom.left k ≫ g.hom
⊢ l ≫ f.hom = m ≫ f.hom
have rw₁ : (l ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom
Tactic: rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
rw : l ≫ Hom.left k ≫ g.hom = m ≫ Hom.left k ≫ g.hom
rw₁ : (l ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom
⊢ l ≫ f.hom = m ≫ f.hom
have rw₂ : (m ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom
Tactic: rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
rw : l ≫ Hom.left k ≫ g.hom = m ≫ Hom.left k ≫ g.hom
rw₁ : (l ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom
rw₂ : (m ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom
⊢ l ≫ f.hom = m ≫ f.hom
have rw₃ : m ≫ Hom.left k ≫ g.hom = m ≫ Hom.left k ≫ g.hom
Tactic: rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
l' : mk (m ≫ f.hom) ⟶ f := homMk l ⋯
⊢ l = m
have suffices : l' = homMk m sorry
Tactic: suffices l' = (homMk m : mk (m ≫ f.hom) ⟶ f) by apply congrArg CommaMorphism.left 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
l' : mk (m ≫ f.hom) ⟶ f := homMk l ⋯
⊢ l' = homMk m ⋯
have rw : l' ≫ k = homMk m sorry ≫ k
Tactic: rw [← cancel_mono 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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g_1
f g : Over.{v₁, u₁} X
k : f ⟶ g
inst_2 : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
l' : mk (m ≫ f.hom) ⟶ f := homMk l ⋯
⊢ l' ≫ k = homMk m ⋯ ≫ k
have h : Hom.left (l' ≫ k) = Hom.left (homMk m sorry ≫ k)
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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g
f : Over.{v₁, u₁} X
X_1 Y : Over f
κ : X_1 ⟶ Y
⊢ Hom.left (Hom.left κ) ≫ (mk (Hom.left Y.hom)).hom = (mk (Hom.left X_1.hom)).hom
have dsimp : Hom.left (Hom.left κ) ≫ Hom.left Y.hom = Hom.left X_1.hom
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 : Over.{v₁, u₁} X
φ : f_1 ⟶ g
f : Over.{v₁, u₁} X
X_1 Y : Over f
κ : X_1 ⟶ Y
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y.hom = Hom.left X_1.hom
have rw : Hom.left (Hom.left κ) ≫ Hom.left Y.hom = Hom.left (Hom.left κ ≫ Y.hom)
Tactic: rw [← 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
f_1 g : Over.{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 : Over.{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 : Over.{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 : Over.{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).left ⟶ (Functor.obj (post F ⋙ post G) Y).left)
  (Hom.left
    (Functor.map (post (F ⋙ G)) f ≫
      Iso.hom
        ((fun (X_2 : Over.{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.left
    (Iso.hom
        ((fun (X_2 : Over.{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 : Over.{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 : Over.{v₁, u₁} X
f : X_1 ⟶ Y
⊢ Eq (α := (Functor.obj (post (F ⋙ G)) X_1).left ⟶ (Functor.obj (post F ⋙ post G) Y).left)
    (Hom.left
      (Functor.map (post (F ⋙ G)) f ≫
        Iso.hom
          ((fun (X_2 : Over.{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.left
      (Iso.hom
          ((fun (X_2 : Over.{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.left (Functor.map (post (F ⋙ G)) f) ≫ 𝟙 (Functor.obj (post (F ⋙ G)) Y).left =
  𝟙 (Functor.obj (post (F ⋙ G)) X_1).left ≫ Hom.left (Functor.map (post F ⋙ post G) f)
Tactic: dsimp only [Iso.refl_hom, Over.comp_left, Over.id_left]
-- 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 : 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)
⊢ f = g
have h₁ : Hom.left f = Hom.left 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 : 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 ⟶ B), Functor.map (post F) a = f
have obtain : ∀ (a : A.left ⟶ B.left) (ha : F.map a = Hom.left f), ∃ (a : A ⟶ B), Functor.map (post F) a = f
Tactic: obtain ⟨a, ha⟩ := F.map_surjective f.left
-- 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 : 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)
⊢ Functor.essImage (post F) B
have obtain : ∀ (A' : T) (e : F.obj A' ≅ B.left), Functor.essImage (post F) B
Tactic: obtain ⟨A', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.left
-- 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 : 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
⊢ Functor.essImage (post F) B
have obtain : ∀ (f : A' ⟶ X) (hf : F.map f = e.hom ≫ B.hom), Functor.essImage (post F) B
Tactic: obtain ⟨f, hf⟩ := F.map_surjective (e.hom ≫ B.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 : 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 ⟶
      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)
have 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) sorry))
  (Hom.left (homMk (a.counit.app x.left) sorry ≫ Functor.map (𝟭 (Over.{v₂, u₂} (Functor.obj.{v₂, v₂, u₂, u₂} (𝟭 D) Y))) 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 : 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)
⊢ (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)
have 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) sorry, naturality := sorry :
            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) sorry,
          naturality := sorry }
        ((post F ⋙ map (a.counit.app Y)).obj A)) =
  Hom.left (𝟙 ((post F ⋙ map (a.counit.app Y)).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 : 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
⊢ homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯ ≫ (liftCone D s c p hp).π.app j = t.π.app j
have h : Hom.left (homMk (hc.lift (Functor.mapCone (forget X) t)) sorry ≫ (liftCone D s c p hp).π.app j) = Hom.left (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 : 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
⊢ x = homMk (hc.lift (Functor.mapCone (forget X) t)) ⋯
have h : Hom.left x = Hom.left (homMk (hc.lift (Functor.mapCone (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 : 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)) ⋯)
have h : ∀ (j : J), Hom.left x ≫ c.π.app j = Hom.left (homMk (hc.lift (Functor.mapCone (forget X) t)) sorry) ≫ c.π.app j
Tactic: refine hc.hom_ext (fun j ↦ ?_)
-- 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
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 X_1.hom)).hom
have 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
Tactic: rw [← CostructuredArrow.w f]
-- 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
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
⊢ (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 ⋯))
have h : Over.Hom.left ((toOver F X).map (homMk f.left sorry) ≫ hom (mk (Y := mk (Y_1.hom ≫ Y.hom)) (Over.homMk Y_1.hom sorry))) =
  Over.Hom.left (hom (mk (Y := mk (X_1.hom ≫ Y.hom)) (Over.homMk X_1.hom sorry)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
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
⊢ f = g
have 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
Tactic: let ⟨_,b,_⟩ := f
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Under.{v₁, u₁} X
f g : U ⟶ V
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
have let : ∀ (left_1 : U.left ⟶ V.left) (e : U.right ⟶ V.right)
  (w_1 : Functor.map (Functor.fromPUnit X) left_1 ≫ V.hom = U.hom ≫ Functor.map (𝟭 T) e)
  (h :
    Hom.right { left := left, right := b, w := w : CommaMorphism U V } =
      Hom.right { left := left_1, right := e, w := w_1 }),
  { left := left, right := b, w := w : CommaMorphism U V } = { left := left_1, right := e, w := w_1 }
Tactic: let ⟨_,e,_⟩ := g
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X : T
U V : Under.{v₁, u₁} X
f g : U ⟶ V
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
left_1 : U.left ⟶ V.left
e : U.right ⟶ V.right
w_1 : Functor.map (Functor.fromPUnit X) left_1 ≫ V.hom = U.hom ≫ Functor.map (𝟭 T) e
h :
  Hom.right { left := left, right := b, w := w : CommaMorphism U V } =
    Hom.right { left := left_1, right := e, w := w_1 }
⊢ { left := left, right := b, w := w : CommaMorphism U V } = { left := left_1, right := e, w := w_1 }
have e_left : left = left_1
Tactic: congr
-- 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
h : f = g
⊢ f.right = g.right
have rw : g.right = g.right
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
f g : Under.{v₁, u₁} X
h : f = g
⊢ Hom.right (eqToHom h) = eqToHom ⋯
have subst : Hom.right (eqToHom sorry) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
Y : T
x : Under.{v₁, u₁} Y
⊢ Functor.obj (map (𝟙 Y)) x = Functor.obj (𝟭 (Under.{v₁, u₁} Y)) x
have simp : { left := x.left, right := x.right, hom := x.hom : Comma.{0, v₁, v₁, 0, u₁, u₁} (Functor.fromPUnit Y) (𝟭 T) } = x
Tactic: simp [map, Comma.mapLeft]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
Y : T
x : Under.{v₁, u₁} Y
⊢ NatTrans.app (Iso.hom (mapId Y)) x = eqToHom ⋯
have h : Hom.right (NatTrans.app (Iso.hom (mapId Y)) x) = Hom.right (eqToHom sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ map (f ≫ g) = map g ⋙ map f
have h_obj : ∀ (X_1 : Under.{v₁, u₁} Z), (map (f ≫ g)).obj X_1 = (map g ⋙ map f).obj X_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
h_obj : ∀ (X_1 : Under.{v₁, u₁} Z), (map (f ≫ g)).obj X_1 = (map g ⋙ map f).obj X_1
⊢ map (f ≫ g) = map g ⋙ map f
have h_map : autoParam
  (∀ (X_1 Y_1 : Under.{v₁, u₁} Z) (f_1 : X_1 ⟶ Y_1),
    (map (f ≫ g)).map f_1 = eqToHom sorry ≫ (map g ⋙ map f).map f_1 ≫ eqToHom sorry)
  Functor.ext._auto_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.Over.Basic (goal)
Goal:
T : Type u₁
inst : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under.{v₁, u₁} Z
k : U ⟶ V
⊢ (map (f ≫ g)).map k = eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯
have h_map : Hom.right ((map (f ≫ g)).map k) = Hom.right (eqToHom sorry ≫ (map g ⋙ map f).map k ≫ eqToHom sorry)
Tactic: ext