awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
        (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
      (prod.lift s.fst (s.snd ≫ prod.snd))
      (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)) =
    s.snd
have refine_2 : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} B X)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
        (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) sorry))
      (prod.lift s.fst (s.snd ≫ prod.snd))
      (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) sorry)))
    prod.fst =
  s.snd ≫ prod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
refine_2 :
  CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} B X)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
          (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
        (prod.lift s.fst (s.snd ≫ prod.snd))
        (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)))
      prod.fst =
    s.snd ≫ prod.fst
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
        (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯))
      (prod.lift s.fst (s.snd ≫ prod.snd))
      (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)) =
    s.snd
have refine_2₁ : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} B X)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan (Y := Limits.prod.{v₁, u₁} B X) f prod.fst)
        (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) sorry))
      (prod.lift s.fst (s.snd ≫ prod.snd))
      (PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) sorry)))
    prod.snd =
  s.snd ≫ prod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
m : s.pt ⟶ Limits.prod.{v₁, u₁} A X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
⊢ m = prod.lift s.fst (s.snd ≫ prod.snd)
have refine_3 : m ≫ prod.fst = CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A X) (prod.lift s.fst (s.snd ≫ prod.snd)) prod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryProduct.{v₁, u₁} A X
inst_2 : HasBinaryProduct.{v₁, u₁} B X
s : PullbackCone (Y := Limits.prod.{v₁, u₁} B X) f prod.fst
m : s.pt ⟶ Limits.prod.{v₁, u₁} A X
h₁ : m ≫ prod.fst = s.fst
h₂ : m ≫ prod.map f (𝟙 X) = s.snd
refine_3 :
  m ≫ prod.fst = CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A X) (prod.lift s.fst (s.snd ≫ prod.snd)) prod.fst
⊢ m = prod.lift s.fst (s.snd ≫ prod.snd)
have refine_3₁ : m ≫ prod.snd = CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} A X) (prod.lift s.fst (s.snd ≫ prod.snd)) prod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryFan.{v₁, u₁} X Y
hc : IsLimit c
T : C
hT : IsTerminal.{v₁, u₁} T
s :
  PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
    Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
    (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
m :
  s.pt ⟶
    Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
⊢ m =
    (fun
          (s :
            PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
        BinaryFan.IsLimit.lift hc s.fst s.snd)
      s
have h₃ : m ≫ c.fst =
  (fun
          (s :
            PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
        BinaryFan.IsLimit.lift hc s.fst s.snd)
      s ≫
    c.fst
Tactic: apply BinaryFan.IsLimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryFan.{v₁, u₁} X Y
hc : IsLimit c
T : C
hT : IsTerminal.{v₁, u₁} T
s :
  PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
    Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
    (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
m :
  s.pt ⟶
    Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := WalkingPair.left : Discrete WalkingPair }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
h₃ :
  m ≫ c.fst =
    (fun
            (s :
              PullbackCone (X :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
                (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
                (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
          BinaryFan.IsLimit.lift hc s.fst s.snd)
        s ≫
      c.fst
⊢ m =
    (fun
          (s :
            PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
        BinaryFan.IsLimit.lift hc s.fst s.snd)
      s
have h₄ : m ≫ c.snd =
  (fun
          (s :
            PullbackCone (X := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
              (hT.from (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))) ↦
        BinaryFan.IsLimit.lift hc s.fst s.snd)
      s ≫
    c.snd
Tactic: apply BinaryFan.IsLimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
⊢ IsPullback t sndsndfgr sndfi rZ
have refine : IsPullback (t ≫ fstfi) sndsndfgr f (rZ ≫ i)
Tactic: refine .of_right ?_ ht₂ hfi
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
i : Z ⟶ S
Pfg : C
fstfg : Pfg ⟶ X
sndfg : Pfg ⟶ Y
hfg : IsPullback fstfg sndfg f g
Pfi : C
fstfi : Pfi ⟶ X
sndfi : Pfi ⟶ Z
hfi : IsPullback fstfi sndfi f i
R : C
rY : R ⟶ Y
rZ : R ⟶ Z
hrw : rY ≫ g = rZ ≫ i
Psndfgr : C
fstsndfgr : Psndfgr ⟶ Pfg
sndsndfgr : Psndfgr ⟶ R
hsndfgr : IsPullback fstsndfgr sndsndfgr sndfg rY
t : Psndfgr ⟶ Pfi
ht₁ : t ≫ fstfi = fstsndfgr ≫ fstfg
ht₂ : t ≫ sndfi = sndsndfgr ≫ rZ
⊢ IsPullback (t ≫ fstfi) sndsndfgr f (rZ ≫ i)
have rw : IsPullback (fstsndfgr ≫ fstfg) sndsndfgr f (rY ≫ g)
Tactic: rw [← hrw, ht₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
⊢ f' ≫ inl' = g' ≫ inr'
have rw : e₁.hom ≫ f' ≫ inl' = e₁.hom ≫ g' ≫ inr'
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commf, ← comminl,
      ← reassoc_of% commg, ← comminr, h.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
rw : e₁.hom ≫ f' ≫ inl' = e₁.hom ≫ g' ≫ inr'
⊢ f' ≫ inl' = g' ≫ inr'
have rw₁ : f ≫ e₂.hom ≫ inl' = e₁.hom ≫ g' ≫ inr'
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commf, ← comminl,
      ← reassoc_of% commg, ← comminr, h.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
rw : e₁.hom ≫ f' ≫ inl' = e₁.hom ≫ g' ≫ inr'
rw₁ : f ≫ e₂.hom ≫ inl' = e₁.hom ≫ g' ≫ inr'
⊢ f' ≫ inl' = g' ≫ inr'
have rw₂ : f ≫ inl ≫ e₄.hom = e₁.hom ≫ g' ≫ inr'
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commf, ← comminl,
      ← reassoc_of% commg, ← comminr, h.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
rw : e₁.hom ≫ f' ≫ inl' = e₁.hom ≫ g' ≫ inr'
rw₁ : f ≫ e₂.hom ≫ inl' = e₁.hom ≫ g' ≫ inr'
rw₂ : f ≫ inl ≫ e₄.hom = e₁.hom ≫ g' ≫ inr'
⊢ f' ≫ inl' = g' ≫ inr'
have rw₃ : f ≫ inl ≫ e₄.hom = g ≫ e₃.hom ≫ inr'
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commf, ← comminl,
      ← reassoc_of% commg, ← comminr, h.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
rw : e₁.hom ≫ f' ≫ inl' = e₁.hom ≫ g' ≫ inr'
rw₁ : f ≫ e₂.hom ≫ inl' = e₁.hom ≫ g' ≫ inr'
rw₂ : f ≫ inl ≫ e₄.hom = e₁.hom ≫ g' ≫ inr'
rw₃ : f ≫ inl ≫ e₄.hom = g ≫ e₃.hom ≫ inr'
⊢ f' ≫ inl' = g' ≫ inr'
have rw₄ : f ≫ inl ≫ e₄.hom = g ≫ inr ≫ e₄.hom
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commf, ← comminl,
      ← reassoc_of% commg, ← comminr, h.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z ≅ Z'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : P ≅ P'
commf : f ≫ e₂.hom = e₁.hom ≫ f'
commg : g ≫ e₃.hom = e₁.hom ≫ g'
comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'
comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'
rw : e₁.hom ≫ f' ≫ inl' = e₁.hom ≫ g' ≫ inr'
rw₁ : f ≫ e₂.hom ≫ inl' = e₁.hom ≫ g' ≫ inr'
rw₂ : f ≫ inl ≫ e₄.hom = e₁.hom ≫ g' ≫ inr'
rw₃ : f ≫ inl ≫ e₄.hom = g ≫ e₃.hom ≫ inr'
rw₄ : f ≫ inl ≫ e₄.hom = g ≫ inr ≫ e₄.hom
⊢ f' ≫ inl' = g' ≫ inr'
have rw₅ : g ≫ inr ≫ e₄.hom = g ≫ inr ≫ e₄.hom
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commf, ← comminl,
      ← reassoc_of% commg, ← comminr, h.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
⊢ IsPushout f' g' inl' inr'
have commf₁ : f ≫ e₂.symm.hom = e₁.symm.hom ≫ f'
Tactic: apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
commf₁ : f ≫ e₂.symm.hom = e₁.symm.hom ≫ f'
⊢ IsPushout f' g' inl' inr'
have commg₁ : g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'
Tactic: apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
commf₁ : f ≫ e₂.symm.hom = e₁.symm.hom ≫ f'
commg₁ : g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'
⊢ IsPushout f' g' inl' inr'
have comminl₁ : inl ≫ e₄.symm.hom = e₂.symm.hom ≫ inl'
Tactic: apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
Z' X' Y' P' : C
f' : Z' ⟶ X'
g' : Z' ⟶ Y'
inl' : X' ⟶ P'
inr' : Y' ⟶ P'
e₁ : Z' ≅ Z
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : P' ≅ P
commf : e₁.hom ≫ f = f' ≫ e₂.hom
commg : e₁.hom ≫ g = g' ≫ e₃.hom
comminl : e₂.hom ≫ inl = inl' ≫ e₄.hom
comminr : e₃.hom ≫ inr = inr' ≫ e₄.hom
commf₁ : f ≫ e₂.symm.hom = e₁.symm.hom ≫ f'
commg₁ : g ≫ e₃.symm.hom = e₁.symm.hom ≫ g'
comminl₁ : inl ≫ e₄.symm.hom = e₂.symm.hom ≫ inl'
⊢ IsPushout f' g' inl' inr'
have comminr₁ : inr ≫ e₄.symm.hom = e₃.symm.hom ≫ inr'
Tactic: apply h.of_iso e₁.symm e₂.symm e₃.symm e₄.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst_1 : 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 : Epi g
⊢ Epi inl
have left_cancellation : ∀ {Z : C} (g h : P ⟶ Z), inl ≫ g = inl ≫ h → g = h
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (hypothesis)
Goal:
C : Type u₁
inst_1 : 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 : IsIso g
⊢ IsIso inl
have this : HasPushout f g
Tactic: have := h.hasPushout
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst_1 : 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 : IsIso g
this : HasPushout f g
⊢ IsIso inl
have rw : IsIso (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g) (Iso.inv h.isoPushout))
Tactic: rw [← h.inl_isoPushout_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₂ ⟶ X₃₂
v₂₁ : X₂₁ ⟶ X₃₁
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ h₁₁ ≫ v₁₃ = v₁₁ ≫ v₂₁ ≫ h₃₁
have rw : (v₁₁ ≫ v₂₁) ≫ h₃₁ = v₁₁ ≫ v₂₁ ≫ h₃₁
Tactic: rw [s.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₂₁ : X₂₁ ⟶ X₂₂
h₃₁ : X₃₁ ⟶ X₃₂
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₂ ⟶ X₃₂
v₂₁ : X₂₁ ⟶ X₃₁
s : IsPushout h₁₁ (v₁₁ ≫ v₂₁) v₁₃ h₃₁
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
rw : (v₁₁ ≫ v₂₁) ≫ h₃₁ = v₁₁ ≫ v₂₁ ≫ h₃₁
⊢ h₁₁ ≫ v₁₃ = v₁₁ ≫ v₂₁ ≫ h₃₁
have rw₁ : v₁₁ ≫ v₂₁ ≫ h₃₁ = v₁₁ ≫ v₂₁ ≫ h₃₁
Tactic: rw [s.w, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₃ : X₂₁ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
⊢ h₁₁ ≫ h₁₂ ≫ v₁₃ = v₁₁ ≫ h₂₃
have rw : (h₁₁ ≫ h₁₂) ≫ v₁₃ = v₁₁ ≫ h₂₃
Tactic: rw [← Category.assoc, s.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C
h₁₁ : X₁₁ ⟶ X₁₂
h₁₂ : X₁₂ ⟶ X₁₃
h₂₁ : X₂₁ ⟶ X₂₂
h₂₃ : X₂₁ ⟶ X₂₃
v₁₁ : X₁₁ ⟶ X₂₁
v₁₂ : X₁₂ ⟶ X₂₂
v₁₃ : X₁₃ ⟶ X₂₃
s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ h₂₃
t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁
rw : (h₁₁ ≫ h₁₂) ≫ v₁₃ = v₁₁ ≫ h₂₃
⊢ h₁₁ ≫ h₁₂ ≫ v₁₃ = v₁₁ ≫ h₂₃
have rw₁ : v₁₁ ≫ h₂₃ = v₁₁ ≫ h₂₃
Tactic: rw [← Category.assoc, s.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
inst_1 : Epi f
inst_2 : IsIso inr
sq : CommSq f g inl inr
⊢ IsColimit sq.cocone
have _ : ∀ (s : PushoutCocone f g), inl ≫ (fun (s : PushoutCocone f g) ↦ inv inr ≫ s.inr) s = s.inl
Tactic: refine
        PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => ?_)
          (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
⊢ { l :
    Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
      s.pt //
    PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ l = s.inl ∧
      PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ l = s.inr ∧
        ∀
          {m :
            Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
                (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
              s.pt},
          PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m =
              s.inl →
            PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m =
                s.inr →
              m = l }
have refine_1 : CategoryStruct.comp (Y :=
    Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
      (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry))
    (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry))
    (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
  s.inl
Tactic: refine ⟨coprod.desc s.inr (coprod.inr ≫ s.inl), ?_, ?_, ?_⟩