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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ fst' ≫ f' = snd' ≫ g'
have rw : e₁.hom ≫ fst' ≫ f' = e₁.hom ≫ snd' ≫ g'
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commfst, ← commf,
      ← reassoc_of% commsnd, ← commg, 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
rw : e₁.hom ≫ fst' ≫ f' = e₁.hom ≫ snd' ≫ g'
⊢ fst' ≫ f' = snd' ≫ g'
have rw₁ : fst ≫ e₂.hom ≫ f' = e₁.hom ≫ snd' ≫ g'
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commfst, ← commf,
      ← reassoc_of% commsnd, ← commg, 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
rw : e₁.hom ≫ fst' ≫ f' = e₁.hom ≫ snd' ≫ g'
rw₁ : fst ≫ e₂.hom ≫ f' = e₁.hom ≫ snd' ≫ g'
⊢ fst' ≫ f' = snd' ≫ g'
have rw₂ : fst ≫ f ≫ e₄.hom = e₁.hom ≫ snd' ≫ g'
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commfst, ← commf,
      ← reassoc_of% commsnd, ← commg, 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
rw : e₁.hom ≫ fst' ≫ f' = e₁.hom ≫ snd' ≫ g'
rw₁ : fst ≫ e₂.hom ≫ f' = e₁.hom ≫ snd' ≫ g'
rw₂ : fst ≫ f ≫ e₄.hom = e₁.hom ≫ snd' ≫ g'
⊢ fst' ≫ f' = snd' ≫ g'
have rw₃ : fst ≫ f ≫ e₄.hom = snd ≫ e₃.hom ≫ g'
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commfst, ← commf,
      ← reassoc_of% commsnd, ← commg, 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
rw : e₁.hom ≫ fst' ≫ f' = e₁.hom ≫ snd' ≫ g'
rw₁ : fst ≫ e₂.hom ≫ f' = e₁.hom ≫ snd' ≫ g'
rw₂ : fst ≫ f ≫ e₄.hom = e₁.hom ≫ snd' ≫ g'
rw₃ : fst ≫ f ≫ e₄.hom = snd ≫ e₃.hom ≫ g'
⊢ fst' ≫ f' = snd' ≫ g'
have rw₄ : fst ≫ f ≫ e₄.hom = snd ≫ g ≫ e₄.hom
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commfst, ← commf,
      ← reassoc_of% commsnd, ← commg, 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
rw : e₁.hom ≫ fst' ≫ f' = e₁.hom ≫ snd' ≫ g'
rw₁ : fst ≫ e₂.hom ≫ f' = e₁.hom ≫ snd' ≫ g'
rw₂ : fst ≫ f ≫ e₄.hom = e₁.hom ≫ snd' ≫ g'
rw₃ : fst ≫ f ≫ e₄.hom = snd ≫ e₃.hom ≫ g'
rw₄ : fst ≫ f ≫ e₄.hom = snd ≫ g ≫ e₄.hom
⊢ fst' ≫ f' = snd' ≫ g'
have rw₅ : snd ≫ g ≫ e₄.hom = snd ≫ g ≫ e₄.hom
Tactic: rw [← cancel_epi e₁.hom, ← reassoc_of% commfst, ← commf,
      ← reassoc_of% commsnd, ← commg, 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ h.cone ≅ (Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯)
have refine_1 : h.cone.fst =
  e₁.hom ≫ PullbackCone.fst ((Cone.postcompose (cospanExt e₂ e₃ e₄ sorry sorry).inv).obj (PullbackCone.mk fst' snd' sorry))
Tactic: refine PullbackCone.ext e₁ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_1 :
  h.cone.fst =
    e₁.hom ≫ PullbackCone.fst ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))
⊢ h.cone ≅ (Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯)
have refine_2 : h.cone.snd =
  e₁.hom ≫ PullbackCone.snd ((Cone.postcompose (cospanExt e₂ e₃ e₄ sorry sorry).inv).obj (PullbackCone.mk fst' snd' sorry))
Tactic: refine PullbackCone.ext e₁ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ h.cone.fst =
    e₁.hom ≫ PullbackCone.fst ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))
have refine_1 : fst = e₁.hom ≫ fst' ≫ e₂.inv
Tactic: change fst = e₁.hom ≫ fst' ≫ e₂.inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ fst = e₁.hom ≫ fst' ≫ e₂.inv
have refine_1 : fst = fst ≫ e₂.hom ≫ e₂.inv
Tactic: rw [← reassoc_of% commfst, e₂.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_1 : fst = fst ≫ e₂.hom ≫ e₂.inv
⊢ fst = e₁.hom ≫ fst' ≫ e₂.inv
have refine_1₁ : fst = fst ≫ 𝟙 X
Tactic: rw [← reassoc_of% commfst, e₂.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_1 : fst = fst ≫ e₂.hom ≫ e₂.inv
refine_1₁ : fst = fst ≫ 𝟙 X
⊢ fst = e₁.hom ≫ fst' ≫ e₂.inv
have refine_1₂ : fst = fst
Tactic: rw [← reassoc_of% commfst, e₂.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ h.cone.snd =
    e₁.hom ≫ PullbackCone.snd ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))
have refine_2 : snd = e₁.hom ≫ snd' ≫ e₃.inv
Tactic: change snd = e₁.hom ≫ snd' ≫ e₃.inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ snd = e₁.hom ≫ snd' ≫ e₃.inv
have refine_2 : snd = snd ≫ e₃.hom ≫ e₃.inv
Tactic: rw [← reassoc_of% commsnd, e₃.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_2 : snd = snd ≫ e₃.hom ≫ e₃.inv
⊢ snd = e₁.hom ≫ snd' ≫ e₃.inv
have refine_2₁ : snd = snd ≫ 𝟙 Y
Tactic: rw [← reassoc_of% commsnd, e₃.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
refine_2 : snd = snd ≫ e₃.hom ≫ e₃.inv
refine_2₁ : snd = snd ≫ 𝟙 Y
⊢ snd = e₁.hom ≫ snd' ≫ e₃.inv
have refine_2₂ : snd = snd
Tactic: rw [← reassoc_of% commsnd, e₃.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
⊢ IsPullback fst' snd' f' g'
have commfst₁ : fst ≫ e₂.symm.hom = e₁.symm.hom ≫ fst'
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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
commfst₁ : fst ≫ e₂.symm.hom = e₁.symm.hom ≫ fst'
⊢ IsPullback fst' snd' f' g'
have commsnd₁ : snd ≫ e₃.symm.hom = e₁.symm.hom ≫ snd'
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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
commfst₁ : fst ≫ e₂.symm.hom = e₁.symm.hom ≫ fst'
commsnd₁ : snd ≫ e₃.symm.hom = e₁.symm.hom ≫ snd'
⊢ IsPullback fst' snd' f' g'
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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P' ≅ P
e₂ : X' ≅ X
e₃ : Y' ≅ Y
e₄ : Z' ≅ Z
commfst : e₁.hom ≫ fst = fst' ≫ e₂.hom
commsnd : e₁.hom ≫ snd = snd' ≫ e₃.hom
commf : e₂.hom ≫ f = f' ≫ e₄.hom
commg : e₃.hom ≫ g = g' ≫ e₄.hom
commfst₁ : fst ≫ e₂.symm.hom = e₁.symm.hom ≫ fst'
commsnd₁ : snd ≫ e₃.symm.hom = e₁.symm.hom ≫ snd'
commf₁ : f ≫ e₄.symm.hom = e₂.symm.hom ≫ f'
⊢ IsPullback fst' snd' f' g'
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_1 : 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 : Mono g
⊢ Mono fst
have right_cancellation : ∀ {Z : C} (g h : Z ⟶ P), g ≫ fst = h ≫ fst → 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : IsIso g
⊢ IsIso fst
have this : HasPullback f g
Tactic: have := h.hasPullback
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst_1 : 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 : IsIso g
this : HasPullback f g
⊢ IsIso fst
have rw : IsIso (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g))
Tactic: rw [← h.isoPullback_hom_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (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
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 : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
⊢ h₁₃ ≫ v₁₃ = (v₁₁ ≫ h₂₁) ≫ h₂₂
have rw : v₁₁ ≫ h₂₁ ≫ h₂₂ = (v₁₁ ≫ h₂₁) ≫ 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
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 : IsPullback h₁₃ v₁₁ v₁₃ (h₂₁ ≫ h₂₂)
t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂
rw : v₁₁ ≫ h₂₁ ≫ h₂₂ = (v₁₁ ≫ h₂₁) ≫ h₂₂
⊢ h₁₃ ≫ v₁₃ = (v₁₁ ≫ h₂₁) ≫ h₂₂
have rw₁ : v₁₁ ≫ h₂₁ ≫ h₂₂ = v₁₁ ≫ h₂₁ ≫ 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
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 : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁
t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
⊢ (h₁₁ ≫ v₁₂) ≫ v₂₂ = v₃₁ ≫ h₃₁
have rw : h₁₁ ≫ v₁₂ ≫ 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
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 : IsPullback h₁₁ v₃₁ (v₁₂ ≫ v₂₂) h₃₁
t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁
rw : h₁₁ ≫ v₁₂ ≫ v₂₂ = v₃₁ ≫ h₃₁
⊢ (h₁₁ ≫ v₁₂) ≫ 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
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
⊢ { l :
    s.pt ⟶
      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)) ⋯) //
    l ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst ∧
      l ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.snd ∧
        ∀
          {m :
            s.pt ⟶
              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)) ⋯)},
          m ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst →
            m ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) =
                s.snd →
              m = l }
have refine_1 : 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.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) sorry)) =
  s.fst
Tactic: refine ⟨prod.lift s.fst (s.snd ≫ prod.snd), ?_, ?_, ?_⟩
-- 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_1 :
  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.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)) =
    s.fst
⊢ { l :
    s.pt ⟶
      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)) ⋯) //
    l ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst ∧
      l ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.snd ∧
        ∀
          {m :
            s.pt ⟶
              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)) ⋯)},
          m ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst →
            m ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) =
                s.snd →
              m = l }
have refine_2 : 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)) =
  s.snd
Tactic: refine ⟨prod.lift s.fst (s.snd ≫ prod.snd), ?_, ?_, ?_⟩
-- 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_1 :
  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.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯)) =
    s.fst
refine_2 :
  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
⊢ { l :
    s.pt ⟶
      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)) ⋯) //
    l ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst ∧
      l ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.snd ∧
        ∀
          {m :
            s.pt ⟶
              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)) ⋯)},
          m ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) = s.fst →
            m ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) ⋯) =
                s.snd →
              m = l }
have refine_3 : ∀
  {m :
    s.pt ⟶
      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)},
  m ≫ PullbackCone.fst (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) sorry) = s.fst →
    m ≫ PullbackCone.snd (PullbackCone.mk (W := Limits.prod.{v₁, u₁} A X) prod.fst (prod.map f (𝟙 X)) sorry) = s.snd →
      m = prod.lift s.fst (s.snd ≫ prod.snd)
Tactic: refine ⟨prod.lift s.fst (s.snd ≫ prod.snd), ?_, ?_, ?_⟩