awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MorphismProperty (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : P.ContainsIdentities
Y : P.Under ⊤ X
a : Under.mk (P := P) ⊤ (𝟙 X) ⋯ ⟶ Y
⊢ a = Under.homMk (P := P) (Q := ⊤) Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom ⋯ ⋯
have h : a.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).right =
  CommaMorphism.right
    (Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
      (Under.homMk (P := P) (Q := ⊤) Y.toComma (P := P) (Q := ⊤) (W := ⊤).hom sorry sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MorphismProperty (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPushouts.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderCobaseChange
inst_4 : P.HasOfPrecompProperty P
⊢ CreatesColimitsOfShape (C := P.Under ⊤ X) WalkingSpan (Under.forget P ⊤ X)
have inst : HasColimitsOfShape WalkingSpan (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
Tactic: apply +allowSynthFailures forgetCreatesColimitsOfShapeOfClosed
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MorphismProperty (goal)
Goal:
T : Type u_1
inst_1 : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_2 : HasPushouts.{v_1, u_1} T
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.HasOfPrecompProperty P
inst : HasColimitsOfShape WalkingSpan (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
⊢ CreatesColimitsOfShape (C := P.Under ⊤ X) WalkingSpan (Under.forget P ⊤ X)
have inst₁ : ObjectProperty.IsClosedUnderColimitsOfShape (C := Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
  (commaObj (Functor.fromPUnit X) (𝟭 T) P) WalkingSpan
Tactic: apply +allowSynthFailures forgetCreatesColimitsOfShapeOfClosed
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MorphismProperty (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : HasPushouts.{v_1, u_1} T
inst_2 : P.IsStableUnderComposition
inst_3 : P.IsStableUnderCobaseChange
inst_4 : P.HasOfPrecompProperty P
⊢ HasPushouts (P.Under ⊤ X)
have inst : HasColimitsOfShape WalkingSpan (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
Tactic: apply +allowSynthFailures hasColimitsOfShape_of_closedUnderColimitsOfShape
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.MorphismProperty (goal)
Goal:
T : Type u_1
inst_1 : Category.{v_1, u_1} T
P : MorphismProperty.{v_1, u_1} T
X : T
inst_2 : HasPushouts.{v_1, u_1} T
inst_3 : P.IsStableUnderComposition
inst_4 : P.IsStableUnderCobaseChange
inst_5 : P.HasOfPrecompProperty P
inst : HasColimitsOfShape WalkingSpan (Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
⊢ HasPushouts (P.Under ⊤ X)
have inst₁ : ObjectProperty.IsClosedUnderColimitsOfShape (C := Comma.{0, v_1, v_1, 0, u_1, u_1} (Functor.fromPUnit X) (𝟭 T))
  (commaObj (Functor.fromPUnit X) (𝟭 T) P) WalkingSpan
Tactic: apply +allowSynthFailures hasColimitsOfShape_of_closedUnderColimitsOfShape
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.leftOp
m : s.pt ⟶ (coneLeftOpOfCocone c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneLeftOpOfCocone c).π.app j = s.π.app j
⊢ m = Quiver.Hom.unop (hc.desc (coconeOfConeLeftOp s))
have refine : ∀ (j : J),
  (c.ι.app j ≫ m.op).unop =
    Quiver.Hom.unop (c.ι.app j ≫ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeOfConeLeftOp s))))
Tactic: refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.leftOp
m : (coconeLeftOpOfCone c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeLeftOpOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.unop (hc.lift (coneOfCoconeLeftOp s))
have refine : ∀ (j : J),
  Eq (α := unop (F.obj j) ⟶ unop (op s.pt)) (Quiver.Hom.unop (m.op ≫ c.π.app j))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (hc.lift (coneOfCoconeLeftOp s))) ≫ c.π.app j))
Tactic: refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F
hc : IsColimit c
s : Cone F.rightOp
m : s.pt ⟶ (coneRightOpOfCocone c).pt
w : ∀ (j : J), m ≫ (coneRightOpOfCocone c).π.app j = s.π.app j
⊢ m = Quiver.Hom.op (hc.desc (coconeOfConeRightOp s))
have refine : ∀ (j : Jᵒᵖ),
  (c.ι.app j ≫ m.unop).op =
    Quiver.Hom.op (c.ι.app j ≫ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeOfConeRightOp s))))
Tactic: refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cone F
hc : IsLimit c
s : Cocone F.rightOp
m : (coconeRightOpOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeRightOpOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.op (hc.lift (coneOfCoconeRightOp s))
have refine : ∀ (j : Jᵒᵖ),
  (m.unop ≫ c.π.app j).op =
    Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (hc.lift (coneOfCoconeRightOp s))) ≫ c.π.app j)
Tactic: refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cocone F
hc : IsColimit c
s : Cone F.unop
m : s.pt ⟶ (coneUnopOfCocone c).pt
w : ∀ (j : J), m ≫ (coneUnopOfCocone c).π.app j = s.π.app j
⊢ m = Quiver.Hom.unop (hc.desc (coconeOfConeUnop s))
have refine : ∀ (j : Jᵒᵖ),
  (c.ι.app j ≫ m.op).unop = Quiver.Hom.unop (c.ι.app j ≫ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeOfConeUnop s))))
Tactic: refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cone F
hc : IsLimit c
s : Cocone F.unop
m : (coconeUnopOfCone c).pt ⟶ s.pt
w : ∀ (j : J), (coconeUnopOfCone c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.unop (hc.lift (coneOfCoconeUnop s))
have refine : ∀ (j : Jᵒᵖ),
  Eq (α := unop (F.obj j) ⟶ unop (op s.pt)) (Quiver.Hom.unop (m.op ≫ c.π.app j))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (hc.lift (coneOfCoconeUnop s))) ≫ c.π.app j))
Tactic: refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cocone F.leftOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeLeftOp c).pt
w : ∀ (j : J), m ≫ (coneOfCoconeLeftOp c).π.app j = s.π.app j
⊢ m = Quiver.Hom.op (hc.desc (coconeLeftOpOfCone s))
have refine : ∀ (j : Jᵒᵖ),
  (c.ι.app j ≫ m.unop).op = Quiver.Hom.op (c.ι.app j ≫ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeLeftOpOfCone s))))
Tactic: refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
c : Cone F.leftOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeLeftOp c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfConeLeftOp c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.op (hc.lift (coneLeftOpOfCocone s))
have refine : ∀ (j : Jᵒᵖ),
  (m.unop ≫ c.π.app j).op = Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (hc.lift (coneLeftOpOfCocone s))) ≫ c.π.app j)
Tactic: refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cocone F.rightOp
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeRightOp c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeRightOp c).π.app j = s.π.app j
⊢ m = Quiver.Hom.unop (hc.desc (coconeRightOpOfCone s))
have refine : ∀ (j : J),
  (c.ι.app j ≫ m.op).unop =
    Quiver.Hom.unop (c.ι.app j ≫ Quiver.Hom.op (Quiver.Hom.unop (hc.desc (coconeRightOpOfCone s))))
Tactic: refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeRightOp c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeRightOp c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.unop (hc.lift (coneRightOpOfCocone s))
have refine : ∀ (j : J),
  Eq (α := unop (F.rightOp.obj j) ⟶ unop (op s.pt)) (Quiver.Hom.unop (m.op ≫ c.π.app j))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (hc.lift (coneRightOpOfCocone s))) ≫ c.π.app j))
Tactic: refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cocone F.unop
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeUnop c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeUnop c).π.app j = s.π.app j
⊢ m = Quiver.Hom.op (hc.desc (coconeUnopOfCone s))
have refine : ∀ (j : J),
  (c.ι.app j ≫ m.unop).op = Quiver.Hom.op (c.ι.app j ≫ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeUnopOfCone s))))
Tactic: refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
c : Cone F.unop
hc : IsLimit c
s : Cocone F
m : (coconeOfConeUnop c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeUnop c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.op (hc.lift (coneUnopOfCocone s))
have refine : ∀ (j : J),
  (m.unop ≫ c.π.app j).op = Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (hc.lift (coneUnopOfCocone s))) ≫ c.π.app j)
Tactic: refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ ↔ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C
have refine : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ → HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C
have this : HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ Cᵒᵖ
Tactic: have : HasLimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasLimitsOfShape_of_equivalence (opOpEquivalence J).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ ↔ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C
have refine : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ → HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C
have this : HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ Cᵒᵖ
Tactic: have : HasColimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ ↔ HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C
have refine : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C → HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ
Tactic: refine ⟨fun _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ
have this : HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ C
Tactic: have : HasColimitsOfShape Jᵒᵖᵒᵖ C := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ ↔ HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C
have refine : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C → HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ
Tactic: refine ⟨fun _ ↦ hasLimitsOfShape_of_hasColimitsOfShape_op, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ
have this : HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ C
Tactic: have : HasLimitsOfShape Jᵒᵖᵒᵖ C := hasLimitsOfShape_of_equivalence (opOpEquivalence J).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasWidePullbacks.{w, v₁, u₁} C
ι : Type w
⊢ HasColimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι) Cᵒᵖ
have rw : HasLimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι)ᵒᵖ C
Tactic: rw [hasColimitsOfShape_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasWidePushouts.{w, v₁, u₁} C
ι : Type w
⊢ HasLimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι) Cᵒᵖ
have rw : HasColimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι)ᵒᵖ C
Tactic: rw [hasLimitsOfShape_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasWidePullbacks.{w, v₁, u₁} Cᵒᵖ ↔ HasWidePushouts.{w, v₁, u₁} C
have refine : ∀ (h : HasWidePullbacks.{w, v₁, u₁} Cᵒᵖ) (ι : Type w), HasColimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι) C
Tactic: refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasWidePullbacks.{w, v₁, u₁} Cᵒᵖ
ι : Type w
⊢ HasColimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι) C
have rw : HasLimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι)ᵒᵖ Cᵒᵖ
Tactic: rw [← hasLimitsOfShape_opposite_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasWidePushouts.{w, v₁, u₁} Cᵒᵖ ↔ HasWidePullbacks.{w, v₁, u₁} C
have refine : ∀ (h : HasWidePushouts.{w, v₁, u₁} Cᵒᵖ) (ι : Type w), HasLimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι) C
Tactic: refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasWidePushouts.{w, v₁, u₁} Cᵒᵖ
ι : Type w
⊢ HasLimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι) C
have rw : HasColimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι)ᵒᵖ Cᵒᵖ
Tactic: rw [← hasColimitsOfShape_opposite_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasFiniteWidePullbacks.{v₁, u₁} C
⊢ HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ
have refine : ∀ (J : Type), Finite J → HasColimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J) Cᵒᵖ
Tactic: refine ⟨fun J _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : Type u₂
inst_1 : Category.{v₂, u₂} J_1
inst_2 : HasFiniteWidePullbacks.{v₁, u₁} C
J : Type
h : Finite J
⊢ HasColimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J) Cᵒᵖ
have rw : HasLimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J)ᵒᵖ C
Tactic: rw [hasColimitsOfShape_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasFiniteWidePushouts.{v₁, u₁} C
⊢ HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ
have refine : ∀ (J : Type), Finite J → HasLimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J) Cᵒᵖ
Tactic: refine ⟨fun J _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : Type u₂
inst_1 : Category.{v₂, u₂} J_1
inst_2 : HasFiniteWidePushouts.{v₁, u₁} C
J : Type
h : Finite J
⊢ HasLimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J) Cᵒᵖ
have rw : HasColimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J)ᵒᵖ C
Tactic: rw [hasLimitsOfShape_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ ↔ HasFiniteWidePushouts.{v₁, u₁} C
have refine : ∀ (h : HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ) (J : Type),
  Finite J → HasColimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J) C
Tactic: refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ
J : Type
h_1 : Finite J
⊢ HasColimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J) C
have rw : HasLimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J)ᵒᵖ Cᵒᵖ
Tactic: rw [← hasLimitsOfShape_opposite_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ ↔ HasFiniteWidePullbacks.{v₁, u₁} C
have refine : ∀ (h : HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ) (J : Type),
  Finite J → HasLimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J) C
Tactic: refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Opposites (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ
J : Type
h_1 : Finite J
⊢ HasLimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J) C
have rw : HasColimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J)ᵒᵖ Cᵒᵖ
Tactic: rw [← hasColimitsOfShape_opposite_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Pi (goal)
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j ⟶ F.obj j')
    (Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f ≫ fun (i : I) ↦ (c i).π.app j')
    ((fun (i : I) ↦ (c i).π.app j) ≫ F.map f)
have h : ∀ (i : I),
  Eq (α := Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
    ((Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f ≫ fun (i : I) ↦ (c i).π.app j') i :
      Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
    (((fun (i : I) ↦ (c i).π.app j) ≫ F.map f) i :
      Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Pi (goal)
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
⊢ Eq (α := F.obj j ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j')
    (F.map f ≫ fun (i : I) ↦ (c i).ι.app j')
    ((fun (i : I) ↦ (c i).ι.app j) ≫ Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f)
have h : ∀ (i : I),
  Eq (α := F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
    ((F.map f ≫ fun (i : I) ↦ (c i).ι.app j') i :
      F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
    (((fun (i : I) ↦ (c i).ι.app j) ≫ Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f) i :
      F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Pi (goal)
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
j : J
⊢ (fun (i : I) ↦ (P i).lift (coneCompEval (C := C) s i)) ≫ (coneOfConeCompEval (C := C) c).π.app j = s.π.app j
have h : ∀ (i : I),
  ((fun (i : I) ↦ (P i).lift (coneCompEval (C := C) s i)) ≫ (coneOfConeCompEval (C := C) c).π.app j) i = s.π.app j i
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Pi (goal)
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
m : s.pt ⟶ (coneOfConeCompEval (C := C) c).pt
w : ∀ (j : J), m ≫ (coneOfConeCompEval (C := C) c).π.app j = s.π.app j
⊢ m = fun (i : I) ↦ (P i).lift (coneCompEval (C := C) s i)
have h : ∀ (i : I), m i = (P i).lift (coneCompEval (C := C) s i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Pi (goal)
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
j : J
⊢ ((coconeOfCoconeCompEval (C := C) c).ι.app j ≫ fun (i : I) ↦ (P i).desc (coconeCompEval (C := C) s i)) = s.ι.app j
have h : ∀ (i : I),
  ((coconeOfCoconeCompEval (C := C) c).ι.app j ≫ fun (i : I) ↦ (P i).desc (coconeCompEval (C := C) s i)) i = s.ι.app j i
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Pi (goal)
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
m : (coconeOfCoconeCompEval (C := C) c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeCompEval (C := C) c).ι.app j ≫ m = s.ι.app j
⊢ m = fun (i : I) ↦ (P i).desc (coconeCompEval (C := C) s i)
have h : ∀ (i : I), m i = (P i).desc (coconeCompEval (C := C) s i)
Tactic: funext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preorder (goal)
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cone F
x : C
⊢ x ∈ Set.range F.obj → c.pt ≤ x
have this : ∀ (i : J) (p : F.obj i = x), c.pt ≤ x
Tactic: ⟨i, p⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preorder (goal)
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cone F
x : C
i : J
p : F.obj i = x
⊢ c.pt ≤ x
have rw : c.pt ≤ F.obj i
Tactic: rw [← p]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preorder (goal)
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cocone F
x : C
⊢ x ∈ Set.range F.obj → x ≤ c.pt
have this : ∀ (i : J) (p : F.obj i = x), x ≤ c.pt
Tactic: ⟨i, p⟩