awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
create : (t₁.inr ≫ t₂.inl) ≫ l = t₁.inr ≫ s.inl
create₁ : («i₂» ≫ t₂.inl) ≫ l = «i₂» ≫ s.inl
⊢ t₁.inr ≫ t₂.inl ≫ l = t₁.inr ≫ s.inl
have create₂ : (f₂ ≫ t₂.inr) ≫ l = «i₂» ≫ s.inl
Tactic: rw [← Category.assoc, ← hi₂, t₂.condition, s.condition, Category.assoc, hl']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
create : (t₁.inr ≫ t₂.inl) ≫ l = t₁.inr ≫ s.inl
create₁ : («i₂» ≫ t₂.inl) ≫ l = «i₂» ≫ s.inl
create₂ : (f₂ ≫ t₂.inr) ≫ l = «i₂» ≫ s.inl
⊢ t₁.inr ≫ t₂.inl ≫ l = t₁.inr ≫ s.inl
have create₃ : (f₂ ≫ t₂.inr) ≫ l = f₂ ≫ s.inr
Tactic: rw [← Category.assoc, ← hi₂, t₂.condition, s.condition, Category.assoc, hl']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
create : (t₁.inr ≫ t₂.inl) ≫ l = t₁.inr ≫ s.inl
create₁ : («i₂» ≫ t₂.inl) ≫ l = «i₂» ≫ s.inl
create₂ : (f₂ ≫ t₂.inr) ≫ l = «i₂» ≫ s.inl
create₃ : (f₂ ≫ t₂.inr) ≫ l = f₂ ≫ s.inr
⊢ t₁.inr ≫ t₂.inl ≫ l = t₁.inr ≫ s.inl
have create₄ : f₂ ≫ t₂.inr ≫ l = f₂ ≫ s.inr
Tactic: rw [← Category.assoc, ← hi₂, t₂.condition, s.condition, Category.assoc, hl']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl' : t₂.inr ≫ l = s.inr
hl : t₁.inl ≫ t₂.inl ≫ l = t₁.inl ≫ s.inl
create : (t₁.inr ≫ t₂.inl) ≫ l = t₁.inr ≫ s.inl
create₁ : («i₂» ≫ t₂.inl) ≫ l = «i₂» ≫ s.inl
create₂ : (f₂ ≫ t₂.inr) ≫ l = «i₂» ≫ s.inl
create₃ : (f₂ ≫ t₂.inr) ≫ l = f₂ ≫ s.inr
create₄ : f₂ ≫ t₂.inr ≫ l = f₂ ≫ s.inr
⊢ t₁.inr ≫ t₂.inl ≫ l = t₁.inr ≫ s.inl
have create₅ : f₂ ≫ s.inr = f₂ ≫ s.inr
Tactic: rw [← Category.assoc, ← hi₂, t₂.condition, s.condition, Category.assoc, hl']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
⊢ m = l
have create : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = (t₁.pasteHoriz t₂ hi₂).inl ≫ l
Tactic: apply PushoutCocone.IsColimit.hom_ext H'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ : C
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
i₁ : X₁ ⟶ Y₁
t₁ : PushoutCocone i₁ f₁
i₂ : X₂ ⟶ t₁.pt
t₂ : PushoutCocone «i₂» f₂
hi₂ : «i₂» = t₁.inr
H : IsColimit t₁
H' : IsColimit (t₁.pasteHoriz t₂ hi₂)
s : PushoutCocone «i₂» f₂
l : (t₁.pasteHoriz t₂ hi₂).pt ⟶ s.pt
hl : (t₁.pasteHoriz t₂ hi₂).inl ≫ l = t₁.inl ≫ s.inl
hl' : (t₁.pasteHoriz t₂ hi₂).inr ≫ l = s.inr
m : t₂.pt ⟶ s.pt
hm₁ : t₂.inl ≫ m = s.inl
hm₂ : t₂.inr ≫ m = s.inr
create : (t₁.pasteHoriz t₂ hi₂).inl ≫ m = (t₁.pasteHoriz t₂ hi₂).inl ≫ l
⊢ m = l
have create₁ : (t₁.pasteHoriz t₂ hi₂).inr ≫ m = (t₁.pasteHoriz t₂ hi₂).inr ≫ l
Tactic: apply PushoutCocone.IsColimit.hom_ext H'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁_1 : PushoutCocone g₂ i₃
i₂_1 : Y₂ ⟶ t₁_1.pt
t₂_1 : PushoutCocone g₁ i₂_1
hi₂_1 : i₂_1 = t₁_1.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
⊢ (g₂ ≫ g₁) ≫ t₂.inl = i₃ ≫ t₁.inr ≫ t₂.inr
have rw : (g₂ ≫ g₁) ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
Tactic: rw [← reassoc_of% t₁.condition, Category.assoc, t₂.condition, ← hi₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁_1 : PushoutCocone g₂ i₃
i₂_1 : Y₂ ⟶ t₁_1.pt
t₂_1 : PushoutCocone g₁ i₂_1
hi₂_1 : i₂_1 = t₁_1.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
rw : (g₂ ≫ g₁) ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
⊢ (g₂ ≫ g₁) ≫ t₂.inl = i₃ ≫ t₁.inr ≫ t₂.inr
have rw₁ : g₂ ≫ g₁ ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
Tactic: rw [← reassoc_of% t₁.condition, Category.assoc, t₂.condition, ← hi₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁_1 : PushoutCocone g₂ i₃
i₂_1 : Y₂ ⟶ t₁_1.pt
t₂_1 : PushoutCocone g₁ i₂_1
hi₂_1 : i₂_1 = t₁_1.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
rw : (g₂ ≫ g₁) ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
rw₁ : g₂ ≫ g₁ ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
⊢ (g₂ ≫ g₁) ≫ t₂.inl = i₃ ≫ t₁.inr ≫ t₂.inr
have rw₂ : g₂ ≫ i₂ ≫ t₂.inr = g₂ ≫ t₁.inl ≫ t₂.inr
Tactic: rw [← reassoc_of% t₁.condition, Category.assoc, t₂.condition, ← hi₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁_1 : PushoutCocone g₂ i₃
i₂_1 : Y₂ ⟶ t₁_1.pt
t₂_1 : PushoutCocone g₁ i₂_1
hi₂_1 : i₂_1 = t₁_1.inl
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ i₂
hi₂ : i₂ = t₁.inl
rw : (g₂ ≫ g₁) ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
rw₁ : g₂ ≫ g₁ ≫ t₂.inl = g₂ ≫ t₁.inl ≫ t₂.inr
rw₂ : g₂ ≫ i₂ ≫ t₂.inr = g₂ ≫ t₁.inl ≫ t₂.inr
⊢ (g₂ ≫ g₁) ≫ t₂.inl = i₃ ≫ t₁.inr ≫ t₂.inr
have rw₃ : g₂ ≫ i₂ ≫ t₂.inr = g₂ ≫ i₂ ≫ t₂.inr
Tactic: rw [← reassoc_of% t₁.condition, Category.assoc, t₂.condition, ← hi₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Y₃ Y₂ Y₁ X₃ : C
g₂ : Y₃ ⟶ Y₂
g₁ : Y₂ ⟶ Y₁
i₃ : Y₃ ⟶ X₃
t₁ : PushoutCocone g₂ i₃
i₂ : Y₂ ⟶ t₁.pt
t₂ : PushoutCocone g₁ «i₂»
hi₂ : «i₂» = t₁.inl
H₁ : IsColimit t₁
H₂ : IsColimit t₂
⊢ IsColimit (t₁.pasteVert t₂ hi₂)
have apply : IsColimit (t₁.flip.pasteHoriz («i₂» := «i₂») t₂.flip hi₂)
Tactic: apply PushoutCocone.isColimitOfFlip <| IsColimit.ofIsoColimit _ (t₁.pasteVertFlip t₂ hi₂).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst_1 : HasPullback f g
inst_2 : HasPullback (Y := pullback f g) f' (pullback.fst f g)
⊢ Eq (α := pullback (f' ≫ f) g ⟶ X)
    (CategoryStruct.comp (Y := pullback (Y := pullback f g) f' (pullback.fst f g))
        (Iso.inv (pullbackRightPullbackFstIso f g f')) (pullback.snd f' (pullback.fst f g) ≫ pullback.fst f g) :
      pullback (f' ≫ f) g ⟶ X)
    (pullback.fst (f' ≫ f) g ≫ f' : pullback (f' ≫ f) g ⟶ X)
have rw : Eq (α := pullback (f' ≫ f) g ⟶ X)
  (CategoryStruct.comp (Y := pullback (Y := pullback f g) f' (pullback.fst f g))
      (Iso.inv (pullbackRightPullbackFstIso f g f')) (pullback.fst f' (pullback.fst f g) ≫ f') :
    pullback (f' ≫ f) g ⟶ X)
  (pullback.fst (f' ≫ f) g ≫ f' : pullback (f' ≫ f) g ⟶ X)
Tactic: rw [← pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
g' : W ⟶ Y
inst_1 : HasPullback f g
inst_2 : HasPullback (X := pullback f g) (pullback.snd f g) g'
⊢ Eq (α := pullback f (g' ≫ g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (pullback.snd f g) g')
        (Iso.inv (pullbackLeftPullbackSndIso f g g')) (pullback.fst (pullback.snd f g) g' ≫ pullback.snd f g) :
      pullback f (g' ≫ g) ⟶ Y)
    (pullback.snd f (g' ≫ g) ≫ g' : pullback f (g' ≫ g) ⟶ Y)
have rw : Eq (α := pullback f (g' ≫ g) ⟶ Y)
  (CategoryStruct.comp (Y := pullback (X := pullback f g) (pullback.snd f g) g')
      (Iso.inv (pullbackLeftPullbackSndIso f g g')) (pullback.snd (pullback.snd f g) g' ≫ g') :
    pullback f (g' ≫ g) ⟶ Y)
  (pullback.snd f (g' ≫ g) ≫ g' : pullback f (g' ≫ g) ⟶ Y)
Tactic: rw [pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
⊢ Eq (α := Y ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
        (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inl (pushout.inr f g) g')
          (Iso.hom (pushoutLeftPushoutInrIso f g g'))) :
      Y ⟶ pushout f (g ≫ g'))
    (pushout.inl f (g ≫ g') : Y ⟶ pushout f (g ≫ g'))
have rw : Eq (α := Y ⟶ pushout f (g ≫ g'))
  (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g')
      (pushout.inl f g ≫ pushout.inl (pushout.inr f g) g') (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
    Y ⟶ pushout f (g ≫ g'))
  (pushout.inl f (g ≫ g') : Y ⟶ pushout f (g ≫ g'))
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
⊢ Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
        (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inl (pushout.inr f g) g')
          (Iso.hom (pushoutLeftPushoutInrIso f g g'))) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
have rw : Eq (α := Z ⟶ pushout f (g ≫ g'))
  (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g')
      (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g') (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
    Z ⟶ pushout f (g ≫ g'))
  (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, Category.assoc, inr_pushoutLeftPushoutInrIso_inv,
    pushout.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
rw :
  Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g')
        (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g') (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
⊢ Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
        (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inl (pushout.inr f g) g')
          (Iso.hom (pushoutLeftPushoutInrIso f g g'))) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
have rw₁ : Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
  ((g' ≫ pushout.inr f (g ≫ g')) ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, Category.assoc, inr_pushoutLeftPushoutInrIso_inv,
    pushout.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
rw :
  Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g')
        (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g') (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
rw₁ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
    ((g' ≫ pushout.inr f (g ≫ g')) ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
⊢ Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
        (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inl (pushout.inr f g) g')
          (Iso.hom (pushoutLeftPushoutInrIso f g g'))) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
have rw₂ : Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
  (g' ≫ pushout.inr f (g ≫ g') ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, Category.assoc, inr_pushoutLeftPushoutInrIso_inv,
    pushout.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
rw :
  Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g')
        (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g') (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
rw₁ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
    ((g' ≫ pushout.inr f (g ≫ g')) ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
rw₂ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
    (g' ≫ pushout.inr f (g ≫ g') ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
⊢ Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
        (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inl (pushout.inr f g) g')
          (Iso.hom (pushoutLeftPushoutInrIso f g g'))) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
have rw₃ : Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
  (g' ≫ pushout.inr (pushout.inr f g) g')
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, Category.assoc, inr_pushoutLeftPushoutInrIso_inv,
    pushout.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Y := pushout f g) (pushout.inr f g) g'
rw :
  Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g')
        (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g') (Iso.hom (pushoutLeftPushoutInrIso f g g')) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
rw₁ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
    ((g' ≫ pushout.inr f (g ≫ g')) ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
rw₂ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
    (g' ≫ pushout.inr f (g ≫ g') ≫ Iso.inv (pushoutLeftPushoutInrIso f g g'))
rw₃ :
  Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inr f g ≫ pushout.inl (pushout.inr f g) g')
    (g' ≫ pushout.inr (pushout.inr f g) g')
⊢ Eq (α := Z ⟶ pushout f (g ≫ g'))
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
        (CategoryStruct.comp (Y := pushout (Y := pushout f g) (pushout.inr f g) g') (pushout.inl (pushout.inr f g) g')
          (Iso.hom (pushoutLeftPushoutInrIso f g g'))) :
      Z ⟶ pushout f (g ≫ g'))
    (g' ≫ pushout.inr f (g ≫ g') : Z ⟶ pushout f (g ≫ g'))
have rw₄ : Eq (α := Z ⟶ pushout (Y := pushout f g) (pushout.inr f g) g') (g' ≫ pushout.inr (pushout.inr f g) g')
  (g' ≫ pushout.inr (pushout.inr f g) g')
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv, Category.assoc, inr_pushoutLeftPushoutInrIso_inv,
    pushout.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
⊢ Eq (α := Z ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout f g) (pushout.inr f g)
        (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inr f' (pushout.inl f g))
          (Iso.hom (pushoutRightPushoutInlIso f g f'))) :
      Z ⟶ pushout (f ≫ f') g)
    (pushout.inr (f ≫ f') g : Z ⟶ pushout (f ≫ f') g)
have rw : Eq (α := Z ⟶ pushout (f ≫ f') g)
  (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g))
      (pushout.inr f g ≫ pushout.inr f' (pushout.inl f g)) (Iso.hom (pushoutRightPushoutInlIso f g f')) :
    Z ⟶ pushout (f ≫ f') g)
  (pushout.inr (f ≫ f') g : Z ⟶ pushout (f ≫ f') g)
Tactic: rw [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
⊢ Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
        (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inr f' (pushout.inl f g))
          (Iso.hom (pushoutRightPushoutInlIso f g f'))) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
have rw : Eq (α := Y ⟶ pushout (f ≫ f') g)
  (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g))
      (pushout.inl f g ≫ pushout.inr f' (pushout.inl f g)) (Iso.hom (pushoutRightPushoutInlIso f g f')) :
    Y ⟶ pushout (f ≫ f') g)
  (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
Tactic: rw [← Category.assoc, ← pushout.condition, Category.assoc, inl_pushoutRightPushoutInlIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
rw :
  Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g))
        (pushout.inl f g ≫ pushout.inr f' (pushout.inl f g)) (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
⊢ Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
        (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inr f' (pushout.inl f g))
          (Iso.hom (pushoutRightPushoutInlIso f g f'))) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
have rw₁ : Eq (α := Y ⟶ pushout (f ≫ f') g)
  (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (f' ≫ pushout.inl f' (pushout.inl f g))
      (Iso.hom (pushoutRightPushoutInlIso f g f')) :
    Y ⟶ pushout (f ≫ f') g)
  (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
Tactic: rw [← Category.assoc, ← pushout.condition, Category.assoc, inl_pushoutRightPushoutInlIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
rw :
  Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g))
        (pushout.inl f g ≫ pushout.inr f' (pushout.inl f g)) (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
rw₁ :
  Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (f' ≫ pushout.inl f' (pushout.inl f g))
        (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
⊢ Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
        (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inr f' (pushout.inl f g))
          (Iso.hom (pushoutRightPushoutInlIso f g f'))) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
have rw₂ : Eq (α := Y ⟶ pushout (f ≫ f') g)
  (f' ≫
      CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inl f' (pushout.inl f g))
        (Iso.hom (pushoutRightPushoutInlIso f g f')) :
    Y ⟶ pushout (f ≫ f') g)
  (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
Tactic: rw [← Category.assoc, ← pushout.condition, Category.assoc, inl_pushoutRightPushoutInlIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst_1 : HasPushout f g
inst_2 : HasPushout (Z := pushout f g) f' (pushout.inl f g)
rw :
  Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g))
        (pushout.inl f g ≫ pushout.inr f' (pushout.inl f g)) (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
rw₁ :
  Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (f' ≫ pushout.inl f' (pushout.inl f g))
        (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
rw₂ :
  Eq (α := Y ⟶ pushout (f ≫ f') g)
    (f' ≫
        CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inl f' (pushout.inl f g))
          (Iso.hom (pushoutRightPushoutInlIso f g f')) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
⊢ Eq (α := Y ⟶ pushout (f ≫ f') g)
    (CategoryStruct.comp (Y := pushout f g) (pushout.inl f g)
        (CategoryStruct.comp (Y := pushout (Z := pushout f g) f' (pushout.inl f g)) (pushout.inr f' (pushout.inl f g))
          (Iso.hom (pushoutRightPushoutInlIso f g f'))) :
      Y ⟶ pushout (f ≫ f') g)
    (f' ≫ pushout.inl (f ≫ f') g : Y ⟶ pushout (f ≫ f') g)
have rw₃ : Eq (α := Y ⟶ pushout (f ≫ f') g) (f' ≫ pushout.inl (f ≫ f') g) (f' ≫ pushout.inl (f ≫ f') g)
Tactic: rw [← Category.assoc, ← pushout.condition, Category.assoc, inl_pushoutRightPushoutInlIso_hom]