awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
refine_1 :
  ∀ (k : J),
    (l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst) ≫
        ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }).π.app k =
      s.fst ≫ ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α }).π.app k
⊢ { l : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }
have refine_2 : l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) sorry).snd = s.snd
Tactic: refine ⟨l, hcⱼ.hom_ext fun k ↦ ?_, ?_, fun {m} hm₁ hm₂ ↦ hcᵢ.hom_ext
    fun k ↦ ((H k f).hom_ext ?_ ?_).trans (hcᵢ.fac ⟨_, _⟩ k).symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
refine_1 :
  ∀ (k : J),
    (l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst) ≫
        ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }).π.app k =
      s.fst ≫ ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α }).π.app k
refine_2 : l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd
⊢ { l : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt //
    l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt},
          m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd → m = l }
have refine_3 : ∀ {m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) sorry).pt}
  (hm₁ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) sorry).fst = s.fst)
  (hm₂ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) sorry).snd = s.snd) (k : J),
  (m ≫ ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }).π.app k) ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).left.map f =
    app
        (Cone.π
          { pt := s.1,
            π := { app := fun (k : J) ↦ sorry.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd sorry, naturality := sorry } })
        k ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).left.map f
Tactic: refine ⟨l, hcⱼ.hom_ext fun k ↦ ?_, ?_, fun {m} hm₁ hm₂ ↦ hcᵢ.hom_ext
    fun k ↦ ((H k f).hom_ext ?_ ?_).trans (hcᵢ.fac ⟨_, _⟩ k).symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
⊢ l ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd
have refine_2 : l ≫ G.hom.app i = s.snd
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
⊢ l ≫ G.hom.app i = s.snd
have refine_2 : ∀ (k : J), l ≫ G.hom.app i = s.snd
Tactic: obtain ⟨k⟩ : Nonempty J := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
k : J
⊢ l ≫ G.hom.app i = s.snd
have refine_2 : l ≫ (Over.Hom.left (α.app k)).app i ≫ (c.obj k).hom.app i = s.snd
Tactic: rw [show G.hom.app i = (α.app k).left.app i ≫ (c.obj k).hom.app i by simp [← comp_app]]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J_1 : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J_1
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
J : Type u_1
inst_5 : Category.{v_1, u_1} J
hJ : IsConnected.{v_1, u_1} J
G : Over F
h : limitsOfShape (fun (f : Over F) ↦ Equifibered f.hom) J G
i j : C
f : i ⟶ j
c : J ⥤ Over F
α : obj (const J) G ⟶ c
hc : IsLimit { pt := G, π := α : Cone c }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj j).hom
s : PullbackCone (G.hom.app j) (F.map f)
hcᵢ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) i) hc
hcⱼ : IsLimit ((Over.forget F ⋙ obj (evaluation C D) j).mapCone { pt := G, π := α : Cone c }) :=
  isLimitOfPreserves (Over.forget F ⋙ obj (evaluation C D) j) hc
l : s.pt ⟶ G.left.obj i :=
  hcᵢ.lift
    { pt := s.1,
      π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } }
m : s.pt ⟶ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).pt
hm₁ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).fst = s.fst
hm₂ : m ≫ (PullbackCone.mk (G.left.map f) (G.hom.app i) ⋯).snd = s.snd
k : J
⊢ (m ≫ ((Over.forget F ⋙ obj (evaluation C D) i).mapCone { pt := G, π := α : Cone c }).π.app k) ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).left.map f =
    app
        (Cone.π
          { pt := s.1,
            π := { app := fun (k : J) ↦ ⋯.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd ⋯, naturality := ⋯ } })
        k ≫
      ({ diag := c, π := α, isLimit := hc : LimitPresentation J G }.diag.obj k).left.map f
have refine_3 : (m ≫ (Over.Hom.left (α.app k)).app i) ≫ (c.obj k).left.map f =
  sorry.lift (s.fst ≫ (Over.Hom.left (α.app k)).app j) s.snd sorry ≫ (c.obj k).left.map f
Tactic: dsimp at *
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
X Y : Under F
e : X ≅ Y
⊢ Coequifibered X.hom → Coequifibered Y.hom
have rw : Coequifibered X.hom → Coequifibered X.hom
Tactic: rw [← Under.w e.hom, Coequifibered.cancel_right_of_respectsIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (hypothesis)
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
⊢ IsClosedUnderColimitsOfShape (C := Under F) (fun (f : Under F) ↦ Coequifibered f.hom) J
have this : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
Tactic: have : IsClosedUnderIsomorphisms fun f : Under F ↦ f.hom.Coequifibered :=
    ⟨fun {X Y} e ↦ by rw [← Under.w e.hom, Coequifibered.cancel_right_of_respectsIso]; simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (hypothesis)
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
⊢ IsClosedUnderColimitsOfShape (C := Under F) (fun (f : Under F) ↦ Coequifibered f.hom) J
have this₁ : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ
Tactic: have (a b : Cᵒᵖ) : HasCoproductsOfShape (a ⟶ b) Dᵒᵖ :=
    hasColimitsOfShape_of_equivalence (Discrete.equivalence Quiver.Hom.opEquiv)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this_1 : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ IsClosedUnderColimitsOfShape (C := Under F) (fun (f : Under F) ↦ Coequifibered f.hom) J
have rw : (inverseImage (ObjectProperty.op fun (f : Under F) ↦ Coequifibered f.hom) e.functor).IsClosedUnderLimitsOfShape Jᵒᵖ
Tactic: rw [isClosedUnderColimitsOfShape_iff_op, ← isClosedUnderLimitsOfShape_inverseImage_iff _ _ e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this_1 : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
⊢ (inverseImage (ObjectProperty.op fun (f : Under F) ↦ Coequifibered f.hom) e.functor).IsClosedUnderLimitsOfShape Jᵒᵖ
have h : ∀ (f : Over F.op),
  inverseImage (ObjectProperty.op fun (f : Under F) ↦ Coequifibered f.hom) e.functor f ↔ Equifibered f.hom
Tactic: convert!
    (inferInstance : IsClosedUnderLimitsOfShape (fun f : Over F.op ↦ f.hom.Equifibered) Jᵒᵖ) with f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits (goal)
Goal:
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_3} C
inst_2 : Category.{v_3, u_2} K
inst_3 : Category.{v_4, u_4} D
F : Functor.{v_2, v_4, u_3, u_4} C D
inst_4 : ∀ (a b : C), HasProductsOfShape.{v_2, u_4, v_4} (a ⟶ b) D
this_1 : IsClosedUnderIsomorphisms (C := Under F) fun (f : Under F) ↦ Coequifibered f.hom
this : ∀ (a b : Cᵒᵖ), HasCoproductsOfShape.{v_2, u_4, v_4} (a ⟶ b) Dᵒᵖ
e : Over F.op ≌ (Under F)ᵒᵖ := (postEquiv (Opposite.op F) (opUnopEquiv C D)).symm.trans (opEquivOpUnder F)
f : Over F.op
⊢ inverseImage (ObjectProperty.op fun (f : Under F) ↦ Coequifibered f.hom) e.functor f ↔ Equifibered f.hom
have h : Coequifibered.{v_2, u_3, v_4, u_4} (J := C) (C := D) (X := F.op.unop) (Y := f.left.unop)
    { app := fun (X : C) ↦ Quiver.Hom.unop (f.hom.app (Opposite.op X)), naturality := sorry } ↔
  Coequifibered (NatTrans.unop f.hom)
Tactic: simp [e, MorphismProperty.cancel_left_of_respectsIso, ← coequifibered_unop_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
⊢ lift (fst f g) (snd f g) ⋯ = 𝟙 (pullback f g)
have h₀ : CategoryStruct.comp (Y := pullback f g) (lift (fst f g) (snd f g) sorry) (fst f g) = 𝟙 (pullback f g) ≫ fst f g
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullback f g
h₀ : CategoryStruct.comp (Y := pullback f g) (lift (fst f g) (snd f g) ⋯) (fst f g) = 𝟙 (pullback f g) ≫ fst f g
⊢ lift (fst f g) (snd f g) ⋯ = 𝟙 (pullback f g)
have h₁ : CategoryStruct.comp (Y := pullback f g) (lift (fst f g) (snd f g) sorry) (snd f g) = 𝟙 (pullback f g) ≫ snd f g
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
⊢ desc (inl f g) (inr f g) ⋯ = 𝟙 (pushout f g)
have h₀ : CategoryStruct.comp (Y := pushout f g) (inl f g) (desc (inl f g) (inr f g) sorry) = inl f g ≫ 𝟙 (pushout f g)
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : HasPushout f g
h₀ : CategoryStruct.comp (Y := pushout f g) (inl f g) (desc (inl f g) (inr f g) ⋯) = inl f g ≫ 𝟙 (pushout f g)
⊢ desc (inl f g) (inr f g) ⋯ = 𝟙 (pushout f g)
have h₁ : CategoryStruct.comp (Y := pushout f g) (inr f g) (desc (inl f g) (inr f g) sorry) = inr f g ≫ 𝟙 (pushout f g)
Tactic: apply hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ f ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ f''
have rw : i₁ ≫ f' ≫ j₃ = (i₁ ≫ j₁) ≫ f''
Tactic: rw [reassoc_of% e₁, e₃, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
rw : i₁ ≫ f' ≫ j₃ = (i₁ ≫ j₁) ≫ f''
⊢ f ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ f''
have rw₁ : i₁ ≫ j₁ ≫ f'' = (i₁ ≫ j₁) ≫ f''
Tactic: rw [reassoc_of% e₁, e₃, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
rw : i₁ ≫ f' ≫ j₃ = (i₁ ≫ j₁) ≫ f''
rw₁ : i₁ ≫ j₁ ≫ f'' = (i₁ ≫ j₁) ≫ f''
⊢ f ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ f''
have rw₂ : i₁ ≫ j₁ ≫ f'' = i₁ ≫ j₁ ≫ f''
Tactic: rw [reassoc_of% e₁, e₃, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₂ ≫ j₂) ≫ g''
have rw : i₂ ≫ g' ≫ j₃ = (i₂ ≫ j₂) ≫ g''
Tactic: rw [reassoc_of% e₂, e₄, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
rw : i₂ ≫ g' ≫ j₃ = (i₂ ≫ j₂) ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₂ ≫ j₂) ≫ g''
have rw₁ : i₂ ≫ j₂ ≫ g'' = (i₂ ≫ j₂) ≫ g''
Tactic: rw [reassoc_of% e₂, e₄, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
rw : i₂ ≫ g' ≫ j₃ = (i₂ ≫ j₂) ≫ g''
rw₁ : i₂ ≫ j₂ ≫ g'' = (i₂ ≫ j₂) ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₂ ≫ j₂) ≫ g''
have rw₂ : i₂ ≫ j₂ ≫ g'' = i₂ ≫ j₂ ≫ g''
Tactic: rw [reassoc_of% e₂, e₄, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst_1 : HasPullback f g
inst_2 : HasPullback f' g'
inst_3 : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ Eq (α := pullback f g ⟶ pullback f'' g'')
    (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
    (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯)
have h₀ : Eq (α := pullback f g ⟶ X'')
  (CategoryStruct.comp (Y := pullback f'' g'')
    (CategoryStruct.comp (Y := pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄))
    (fst f'' g''))
  (CategoryStruct.comp (Y := pullback f'' g'') (map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) sorry sorry) (fst f'' g''))
Tactic: ext