awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
inst_3 : HasBinaryCoproduct.{v₁, u₁} X Y
h :
  X = Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } →
    Eq.{v₁ + 1} (α := 0 ⟶ X) 0
      (IsInitial.to HasZeroObject.zeroIsInitial
        (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
⊢ IsPushout.{v₁, u₁} (C := C) (Z := 0) (X := X) (Y := Y) (P := coprod.{v₁, u₁} X Y) 0 0 coprod.inl coprod.inr
have h₁ : Y = Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } →
  Eq.{v₁ + 1} (α := 0 ⟶ Y) 0
    (IsInitial.to HasZeroObject.zeroIsInitial
      (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
Tactic: convert! @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X : C
s : Cocone.{0, v₁, 0, u₁} (span (Y := 0) 0 (𝟙 X))
⊢ ∀ (j : WalkingSpan),
    CategoryStruct.comp (Y :=
        Functor.obj.{0, v₁, 0, u₁}
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt.{0, v₁, 0, u₁} (F := span (Y := 0) 0 (𝟙 X)) (PushoutCocone.mk (W := 0) 0 0 ⋯)))
          j)
        (NatTrans.app (Cocone.ι (PushoutCocone.mk (W := 0) 0 0 ⋯)) j) 0 =
      s.ι.app j
have c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
Tactic: have c :=
              @PushoutCocone.coequalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _)
                (by simp [eq_iff_true_of_subsingleton]) (by simpa using PushoutCocone.condition s)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPushout (Z := 0) 0 0 b.inl b.inr
have h₁ : Eq.{v₁ + 1} (α := 0 ⟶ X) 0 (IsInitial.to HasZeroObject.zeroIsInitial X)
Tactic: convert! IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
h₁ : Eq.{v₁ + 1} (α := 0 ⟶ X) 0 (IsInitial.to HasZeroObject.zeroIsInitial X)
⊢ IsPushout (Z := 0) 0 0 b.inl b.inr
have h₂ : Eq.{v₁ + 1} (α := 0 ⟶ Y) 0 (IsInitial.to HasZeroObject.zeroIsInitial Y)
Tactic: convert! IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPushout (Y := 0) b.inl 0 b.snd 0
have h₁ : IsPushout (X := 0) 0 b.inl 0 b.snd
Tactic: apply flip
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPushout (X := 0) 0 b.inl 0 b.snd
have h₁ : IsPushout (Z := 0) (X := 0) (CategoryStruct.comp (Y := X) 0 0) 0 0 (b.inr ≫ b.snd)
Tactic: refine of_left ?_ (by simp) (of_isBilimit h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPushout (Y := 0) b.inr 0 b.fst 0
have refine : IsPushout (Z := 0) (Y := 0) 0 (CategoryStruct.comp (Y := Y) 0 0) (b.inl ≫ b.fst) 0
Tactic: refine of_top ?_ (by simp) (of_isBilimit h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPushout (P := 0) b.fst b.snd 0 0
have refine : IsPushout (Y := 0) (P := 0) (b.inl ≫ b.fst) 0 0 (CategoryStruct.comp (Y := Y) 0 0)
Tactic: refine IsPushout.of_left ?_ (by simp) (IsPushout.inl_snd' h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : HasPullback f g
⊢ CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g) = fst
have dsimp : CategoryStruct.comp (Y := pullback f g)
    (Iso.inv (limit.isoLimitCone { cone := PullbackCone.mk fst snd sorry, isLimit := h.isLimit : LimitCone (cospan f g) }))
    (pullback.fst f g) =
  fst
Tactic: dsimp [isoPullback, cone, CommSq.cone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : HasPullback f g
⊢ CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.snd f g) = snd
have dsimp : CategoryStruct.comp (Y := pullback f g)
    (Iso.inv (limit.isoLimitCone { cone := PullbackCone.mk fst snd sorry, isLimit := h.isLimit : LimitCone (cospan f g) }))
    (pullback.snd f g) =
  snd
Tactic: dsimp [isoPullback, cone, CommSq.cone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst_1 : HasPushout f g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (Iso.inv h.isoPushout) = inl
have dsimp : CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
    (Iso.hom
      (colimit.isoColimitCocone
        { cocone := PushoutCocone.mk inl inr sorry, isColimit := h.isColimit : ColimitCocone (span f g) })) =
  inl
Tactic: dsimp [isoPushout, cocone, CommSq.cocone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst_1 : HasPushout f g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (Iso.inv h.isoPushout) = inr
have dsimp : CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
    (Iso.hom
      (colimit.isoColimitCocone
        { cocone := PushoutCocone.mk inl inr sorry, isColimit := h.isColimit : ColimitCocone (span f g) })) =
  inr
Tactic: dsimp [isoPushout, cocone, CommSq.cocone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasKernel t
inst_3 : HasKernel b
sq : IsPullback t l r b
⊢ CategoryStruct.comp (Y := kernel b) (kernel.map t b l r ⋯) (kernel.lift t (sq.lift 0 (kernel.ι b) ⋯) ⋯) = 𝟙 (kernel t)
have h : CategoryStruct.comp (Y := equalizer t 0)
    (CategoryStruct.comp (Y := kernel b) (kernel.map t b l r sorry) (kernel.lift t (sq.lift 0 (kernel.ι b) sorry) sorry))
    (equalizer.ι t 0) =
  𝟙 (kernel t) ≫ equalizer.ι t 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
inst_2 : HasCokernel t
inst_3 : HasCokernel b
sq : IsPushout t l r b
⊢ CategoryStruct.comp (Y := cokernel t) (cokernel.desc b (sq.desc (cokernel.π t) 0 ⋯) ⋯) (cokernel.map t b l r ⋯) =
    𝟙 (cokernel b)
have h : CategoryStruct.comp (Y := coequalizer b 0) (coequalizer.π b 0)
    (CategoryStruct.comp (Y := cokernel t) (cokernel.desc b (sq.desc (cokernel.π t) 0 sorry) sorry) (cokernel.map t b l r sorry)) =
  coequalizer.π b 0 ≫ 𝟙 (cokernel b)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ IsIso (X := pullback f g) (pullback.snd f g)
have refine : pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) sorry = 𝟙 (pullback f g)
Tactic: refine ⟨⟨pullback.lift (g ≫ inv f) (𝟙 _) (by simp), ?_, by simp⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯ = 𝟙 (pullback f g)
have h₀ : CategoryStruct.comp (Y := pullback f g) (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) sorry) (pullback.fst f g) =
  𝟙 (pullback f g) ≫ pullback.fst f g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
h₀ :
  CategoryStruct.comp (Y := pullback f g) (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯) (pullback.fst f g) =
    𝟙 (pullback f g) ≫ pullback.fst f g
⊢ pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) ⋯ = 𝟙 (pullback f g)
have h₁ : CategoryStruct.comp (Y := pullback f g) (pullback.snd f g ≫ pullback.lift (g ≫ inv f) (𝟙 Y) sorry) (pullback.snd f g) =
  𝟙 (pullback f g) ≫ pullback.snd f g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
⊢ CategoryStruct.comp (Y := pullback f g) (inv (pullback.snd f g)) (pullback.fst f g) = g ≫ inv f
have rw : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.snd f g ≫ g ≫ inv f)
Tactic: rw [IsIso.inv_comp_eq, ← pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
rw : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.snd f g ≫ g ≫ inv f)
⊢ CategoryStruct.comp (Y := pullback f g) (inv (pullback.snd f g)) (pullback.fst f g) = g ≫ inv f
have rw₁ : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.fst f g ≫ f ≫ inv f)
Tactic: rw [IsIso.inv_comp_eq, ← pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
rw : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.snd f g ≫ g ≫ inv f)
rw₁ : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.fst f g ≫ f ≫ inv f)
⊢ CategoryStruct.comp (Y := pullback f g) (inv (pullback.snd f g)) (pullback.fst f g) = g ≫ inv f
have rw₂ : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.fst f g ≫ 𝟙 X)
Tactic: rw [IsIso.inv_comp_eq, ← pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso f
rw : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.snd f g ≫ g ≫ inv f)
rw₁ : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.fst f g ≫ f ≫ inv f)
rw₂ : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.fst f g ≫ 𝟙 X)
⊢ CategoryStruct.comp (Y := pullback f g) (inv (pullback.snd f g)) (pullback.fst f g) = g ≫ inv f
have rw₃ : Eq (α := pullback f g ⟶ X) (pullback.fst f g) (pullback.fst f g)
Tactic: rw [IsIso.inv_comp_eq, ← pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ IsIso (X := pullback f g) (pullback.fst f g)
have refine : pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) sorry = 𝟙 (pullback f g)
Tactic: refine ⟨⟨pullback.lift (𝟙 _) (f ≫ inv g) (by simp), ?_, by simp⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯ = 𝟙 (pullback f g)
have h₀ : CategoryStruct.comp (Y := pullback f g) (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) sorry) (pullback.fst f g) =
  𝟙 (pullback f g) ≫ pullback.fst f g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
h₀ :
  CategoryStruct.comp (Y := pullback f g) (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯) (pullback.fst f g) =
    𝟙 (pullback f g) ≫ pullback.fst f g
⊢ pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) ⋯ = 𝟙 (pullback f g)
have h₁ : CategoryStruct.comp (Y := pullback f g) (pullback.fst f g ≫ pullback.lift (𝟙 X) (f ≫ inv g) sorry) (pullback.snd f g) =
  𝟙 (pullback f g) ≫ pullback.snd f g
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
⊢ CategoryStruct.comp (Y := pullback f g) (inv (pullback.fst f g)) (pullback.snd f g) = f ≫ inv g
have rw : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.fst f g ≫ f ≫ inv g)
Tactic: rw [IsIso.inv_comp_eq, pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
rw : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.fst f g ≫ f ≫ inv g)
⊢ CategoryStruct.comp (Y := pullback f g) (inv (pullback.fst f g)) (pullback.snd f g) = f ≫ inv g
have rw₁ : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.snd f g ≫ g ≫ inv g)
Tactic: rw [IsIso.inv_comp_eq, pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
rw : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.fst f g ≫ f ≫ inv g)
rw₁ : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.snd f g ≫ g ≫ inv g)
⊢ CategoryStruct.comp (Y := pullback f g) (inv (pullback.fst f g)) (pullback.snd f g) = f ≫ inv g
have rw₂ : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.snd f g ≫ 𝟙 Y)
Tactic: rw [IsIso.inv_comp_eq, pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso g
rw : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.fst f g ≫ f ≫ inv g)
rw₁ : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.snd f g ≫ g ≫ inv g)
rw₂ : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.snd f g ≫ 𝟙 Y)
⊢ CategoryStruct.comp (Y := pullback f g) (inv (pullback.fst f g)) (pullback.snd f g) = f ≫ inv g
have rw₃ : Eq (α := pullback f g ⟶ Y) (pullback.snd f g) (pullback.snd f g)
Tactic: rw [IsIso.inv_comp_eq, pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso f
⊢ IsIso (Y := pushout f g) (pushout.inr f g)
have refine : pushout.desc (inv f ≫ g) (𝟙 Z) sorry ≫ pushout.inr f g = 𝟙 (pushout f g)
Tactic: refine ⟨⟨pushout.desc (inv f ≫ g) (𝟙 _) (by simp), by simp, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso f
⊢ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = 𝟙 (pushout f g)
have h₀ : CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.desc (inv f ≫ g) (𝟙 Z) sorry ≫ pushout.inr f g) =
  pushout.inl f g ≫ 𝟙 (pushout f g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso f
h₀ :
  CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g) =
    pushout.inl f g ≫ 𝟙 (pushout f g)
⊢ pushout.desc (inv f ≫ g) (𝟙 Z) ⋯ ≫ pushout.inr f g = 𝟙 (pushout f g)
have h₁ : CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (pushout.desc (inv f ≫ g) (𝟙 Z) sorry ≫ pushout.inr f g) =
  pushout.inr f g ≫ 𝟙 (pushout f g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso f
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = inv f ≫ g
have rw : f ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = g
Tactic: rw [IsIso.eq_inv_comp, pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso f
rw : f ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = inv f ≫ g
have rw₁ : g ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inr f g)) = g
Tactic: rw [IsIso.eq_inv_comp, pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso f
rw : f ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = g
rw₁ : g ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inr f g)) = g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = inv f ≫ g
have rw₂ : g ≫ 𝟙 Z = g
Tactic: rw [IsIso.eq_inv_comp, pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso f
rw : f ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = g
rw₁ : g ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inr f g)) = g
rw₂ : g ≫ 𝟙 Z = g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inr f g)) = inv f ≫ g
have rw₃ : g = g
Tactic: rw [IsIso.eq_inv_comp, pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ IsIso (Y := pushout f g) (pushout.inl f g)
have refine : pushout.desc (𝟙 Y) (inv g ≫ f) sorry ≫ pushout.inl f g = 𝟙 (pushout f g)
Tactic: refine ⟨⟨pushout.desc (𝟙 _) (inv g ≫ f) (by simp), by simp, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = 𝟙 (pushout f g)
have h₀ : CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.desc (𝟙 Y) (inv g ≫ f) sorry ≫ pushout.inl f g) =
  pushout.inl f g ≫ 𝟙 (pushout f g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
h₀ :
  CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g) =
    pushout.inl f g ≫ 𝟙 (pushout f g)
⊢ pushout.desc (𝟙 Y) (inv g ≫ f) ⋯ ≫ pushout.inl f g = 𝟙 (pushout f g)
have h₁ : CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (pushout.desc (𝟙 Y) (inv g ≫ f) sorry ≫ pushout.inl f g) =
  pushout.inr f g ≫ 𝟙 (pushout f g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = inv g ≫ f
have rw : g ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = f
Tactic: rw [IsIso.eq_inv_comp, ← pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
rw : g ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = f
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = inv g ≫ f
have rw₁ : f ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inl f g)) = f
Tactic: rw [IsIso.eq_inv_comp, ← pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
rw : g ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = f
rw₁ : f ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inl f g)) = f
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = inv g ≫ f
have rw₂ : f ≫ 𝟙 Y = f
Tactic: rw [IsIso.eq_inv_comp, ← pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_1 : IsIso g
rw : g ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = f
rw₁ : f ≫ CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (inv (pushout.inl f g)) = f
rw₂ : f ≫ 𝟙 Y = f
⊢ CategoryStruct.comp (Y := pushout f g) (pushout.inr f g) (inv (pushout.inl f g)) = inv g ≫ f
have rw₃ : f = f
Tactic: rw [IsIso.eq_inv_comp, ← pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono f
⊢ Mono t.snd
have refine : ∀ {W : C} (h k : W ⟶ t.pt) (i : h ≫ t.snd = k ≫ t.snd), h ≫ t.fst = k ≫ t.fst
Tactic: refine ⟨fun {W} h k i => IsLimit.hom_ext ht ?_ i⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ h ≫ t.fst = k ≫ t.fst
have rw : h ≫ t.snd ≫ g = k ≫ t.snd ≫ g
Tactic: rw [← cancel_mono f, Category.assoc, Category.assoc, condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono g
⊢ Mono t.fst
have refine : ∀ {W : C} (h k : W ⟶ t.pt) (i : h ≫ t.fst = k ≫ t.fst), h ≫ t.snd = k ≫ t.snd
Tactic: refine ⟨fun {W} h k i => IsLimit.hom_ext ht i ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst_1 : Mono g
W : C
h k : W ⟶ t.pt
i : h ≫ t.fst = k ≫ t.fst
⊢ h ≫ t.snd = k ≫ t.snd
have rw : h ≫ t.fst ≫ f = k ≫ t.fst ≫ f
Tactic: rw [← cancel_mono g, Category.assoc, Category.assoc, ← condition]