awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} WalkingReflexivePair C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst_1 : Category.{v₂, u₂} D
H : Functor.{v, v₂, u, u₂} C D
x : WalkingReflexivePair
w :
  (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app zero =
    NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯) zero
⊢ (Functor.whiskerRight (mkNatTrans e₀ e₁ ⋯ ⋯ ⋯) H).app x = NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) ⋯ ⋯ ⋯) x
have w₁ : (Functor.whiskerRight (mkNatTrans e₀ e₁ sorry sorry sorry) H).app one = NatTrans.app (mkNatTrans (H.map e₀) (H.map e₁) sorry sorry sorry) one
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : ReflexiveCofork F
⊢ F.map left ≫ G.π = F.map right ≫ G.π
have rw : G.ι.app one = F.map right ≫ G.π
Tactic: rw [Cocone.w G left, Cocone.w G right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : ReflexiveCofork F
rw : G.ι.app one = F.map right ≫ G.π
⊢ F.map left ≫ G.π = F.map right ≫ G.π
have rw₁ : G.ι.app one = G.ι.app one
Tactic: rw [Cocone.w G left, Cocone.w G right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : ReflexiveCofork F
⊢ ((reflexiveCoforkEquivCofork F).functor.obj G).π = G.π
have dsimp : ((Cocone.precompose (diagramIsoParallelPair (WalkingParallelPair.inclusionWalkingReflexivePair ⋙ F)).inv).obj
      (Cocone.whisker WalkingParallelPair.inclusionWalkingReflexivePair G)).π =
  G.π
Tactic: dsimp [reflexiveCoforkEquivCofork]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : Cofork (F.map left) (F.map right)
⊢ ((reflexiveCoforkEquivCofork F).inverse.obj G).π = G.π
have dsimp : NatTrans.app
    (Cocone.ι
      (Functor.obj (C :=
        Cocone.{0, v, 0, u} (J := WalkingParallelPair) (C := C)
          { obj := fun (X : WalkingParallelPair) ↦ F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
            map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
              F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
            map_id := sorry, map_comp := sorry })
        Functor.Final.extendCocone
        { pt := G.pt,
          ι :=
            Iso.hom
                (diagramIsoParallelPair
                  {
                    obj := fun (X : WalkingParallelPair) ↦
                      F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                    map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                      F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                    map_id := sorry, map_comp := sorry }) ≫
              G.ι }))
    zero =
  G.π
Tactic: dsimp only [reflexiveCoforkEquivCofork, Equivalence.symm, Equivalence.trans,
    ReflexiveCofork.π, Cocone.precomposeEquivalence, Cocone.precompose,
    Functor.comp, Functor.Final.coconesEquiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
G : Cofork (F.map left) (F.map right)
⊢ NatTrans.app
      (Cocone.ι
        (Functor.obj (C :=
          Cocone.{0, v, 0, u} (J := WalkingParallelPair) (C := C)
            { obj := fun (X : WalkingParallelPair) ↦ F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
              map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
              map_id := ⋯, map_comp := ⋯ })
          Functor.Final.extendCocone
          { pt := G.pt,
            ι :=
              Iso.hom
                  (diagramIsoParallelPair
                    {
                      obj := fun (X : WalkingParallelPair) ↦
                        F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                      map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                        F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                      map_id := ⋯, map_comp := ⋯ }) ≫
                G.ι }))
      zero =
    G.π
have rw : F.map (𝟙 zero) ≫
    NatTrans.app
      (Cocone.ι
        { pt := G.pt,
          ι :=
            Iso.hom
                (diagramIsoParallelPair
                  {
                    obj := fun (X : WalkingParallelPair) ↦
                      F.obj (WalkingParallelPair.inclusionWalkingReflexivePair.obj X),
                    map := fun {X Y : WalkingParallelPair} (f : X ⟶ Y) ↦
                      F.map (WalkingParallelPair.inclusionWalkingReflexivePair.map f),
                    map_id := sorry, map_comp := sorry }) ≫
              G.ι })
      WalkingParallelPair.one =
  G.π
Tactic: rw [Functor.Final.extendCocone_obj_ι_app' (Y := .one) (f := 𝟙 zero)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingReflexivePair C
inst_1 : HasCoequalizer (F.map left) (F.map right)
⊢ Eq (α := F.obj zero ⟶ colimit F)
    (CategoryStruct.comp (Y := coequalizer (F.map left) (F.map right)) (coequalizer.π (F.map left) (F.map right))
        (Iso.inv (reflexiveCoequalizerIsoCoequalizer F)) :
      F.obj zero ⟶ colimit F)
    (colimit.ι F zero : F.obj zero ⟶ colimit F)
have rw : Eq (α := F.obj zero ⟶ colimit F)
  (CategoryStruct.comp (Y := coequalizer (F.map left) (F.map right)) (coequalizer.π (F.map left) (F.map right))
      (Iso.inv
        (IsColimit.coconePointUniqueUpToIso
          ((Equiv.symm (ReflexiveCofork.isColimitEquiv F (colimit.cocone F)) :
              (a : IsColimit (colimit.cocone F)) → IsColimit (ReflexiveCofork.toCofork (colimit.cocone F)))
            (colimit.isColimit F))
          (colimit.isColimit (parallelPair (F.map left) (F.map right))))) :
    F.obj zero ⟶ colimit F)
  (colimit.ι F zero : F.obj zero ⟶ colimit F)
Tactic: rw [reflexiveCoequalizerIsoCoequalizer]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst_1 : HasLimit (parallelPair g h)
s : Fork g h
m : s.pt ⟶ (Fork.ofι (P := Limits.equalizer g h) (equalizer.ι g h) ⋯).pt
w : m ≫ (Fork.ofι (P := Limits.equalizer g h) (equalizer.ι g h) ⋯).ι = s.ι
⊢ m = (fun (s : Fork g h) ↦ (limit.lift (parallelPair g h) s : s.pt ⟶ limit (parallelPair g h))) s
have h₁ : m ≫ equalizer.ι g h =
  CategoryStruct.comp (Y := Limits.equalizer g h)
    ((fun (s : Fork g h) ↦ (limit.lift (parallelPair g h) s : s.pt ⟶ limit (parallelPair g h))) s) (equalizer.ι g h)
Tactic: apply equalizer.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ g ≫ k ≫ hr.left = g ≫ k ≫ hr.right
have rw : (f ≫ h) ≫ hr.left = g ≫ k ≫ hr.right
Tactic: rw [← Category.assoc, ← eq_whisker comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = g ≫ k ≫ hr.right
have rw : (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right
Tactic: rw [← Category.assoc, ← eq_whisker comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ g ≫ k ≫ hr.left = g ≫ k ≫ hr.right
have repeat : (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right
Tactic: repeat (rw [← Category.assoc, ← eq_whisker comm])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ IsLimit (Fork.ofι g ⋯)
have apply : (s : Fork (k ≫ hr.left) (k ≫ hr.right)) →
  { l : s.pt ⟶ (Fork.ofι g sorry).pt //
    l ≫ (Fork.ofι g sorry).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g sorry).pt}, m ≫ (Fork.ofι g sorry).ι = s.ι → m = l }
Tactic: apply Fork.IsLimit.mk' _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
⊢ (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
have rw : s.ι ≫ k ≫ hr.left = (s.ι ≫ k) ≫ hr.right
Tactic: rw [Category.assoc, s.condition, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
rw : s.ι ≫ k ≫ hr.left = (s.ι ≫ k) ≫ hr.right
⊢ (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
have rw₁ : s.ι ≫ k ≫ hr.right = (s.ι ≫ k) ≫ hr.right
Tactic: rw [Category.assoc, s.condition, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
rw : s.ι ≫ k ≫ hr.left = (s.ι ≫ k) ≫ hr.right
rw₁ : s.ι ≫ k ≫ hr.right = (s.ι ≫ k) ≫ hr.right
⊢ (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
have rw₂ : s.ι ≫ k ≫ hr.right = s.ι ≫ k ≫ hr.right
Tactic: rw [Category.assoc, s.condition, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
⊢ { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
    l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
have l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
Tactic: have l₁ : (Fork.ι s ≫ k) ≫ hr.left = (Fork.ι s ≫ k) ≫ hr.right := by
      rw [Category.assoc, s.condition, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
⊢ { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
    l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
have obtain : (l : s.pt ⟶ (Fork.ofι h sorry).pt) →
  (hl : l ≫ (Fork.ofι h sorry).ι = s.ι ≫ k) →
    { l : s.pt ⟶ (Fork.ofι g sorry).pt //
      l ≫ (Fork.ofι g sorry).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g sorry).pt}, m ≫ (Fork.ofι g sorry).ι = s.ι → m = l }
Tactic: obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hr.isLimit _ l₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
⊢ { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
    l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
have obtain : (p : s.pt ⟶ (PullbackCone.mk f g comm).pt) →
  p ≫ (PullbackCone.mk f g comm).fst = l →
    (hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι) →
      { l : s.pt ⟶ (Fork.ofι g sorry).pt //
        l ≫ (Fork.ofι g sorry).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g sorry).pt}, m ≫ (Fork.ofι g sorry).ι = s.ι → m = l }
Tactic: obtain ⟨p, _, hp₂⟩ := PullbackCone.IsLimit.lift' t _ _ hl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
⊢ { l : s.pt ⟶ (Fork.ofι g ⋯).pt //
    l ≫ (Fork.ofι g ⋯).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι g ⋯).pt}, m ≫ (Fork.ofι g ⋯).ι = s.ι → m = l }
have refine : ∀ {m : s.pt ⟶ (Fork.ofι g sorry).pt}, m ≫ (Fork.ofι g sorry).ι = s.ι → m = p
Tactic: refine ⟨p, hp₂, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
⊢ m = p
have z : m ≫ g = p ≫ g
Tactic: have z : m ≫ g = p ≫ g := w.trans hp₂.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
⊢ m = p
have apply : ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk f g comm).π.app j = p ≫ (PullbackCone.mk f g comm).π.app j
Tactic: apply t.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
⊢ ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk f g comm).π.app j = p ≫ (PullbackCone.mk f g comm).π.app j
have this : Mono h
Tactic: have := hr.mono
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
this : Mono h
⊢ ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk f g comm).π.app j = p ≫ (PullbackCone.mk f g comm).π.app j
have h₀ : m ≫ (PullbackCone.mk f g comm).fst = p ≫ (PullbackCone.mk f g comm).fst
Tactic: apply (PullbackCone.mk f g comm).equalizer_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
this : Mono h
h₀ : m ≫ (PullbackCone.mk f g comm).fst = p ≫ (PullbackCone.mk f g comm).fst
⊢ ∀ (j : WalkingCospan), m ≫ (PullbackCone.mk f g comm).π.app j = p ≫ (PullbackCone.mk f g comm).π.app j
have h₁ : m ≫ (PullbackCone.mk f g comm).snd = p ≫ (PullbackCone.mk f g comm).snd
Tactic: apply (PullbackCone.mk f g comm).equalizer_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
s : Fork (k ≫ hr.left) (k ≫ hr.right)
l₁ : (s.ι ≫ k) ≫ hr.left = (s.ι ≫ k) ≫ hr.right
l : s.pt ⟶ (Fork.ofι h ⋯).pt
hl : l ≫ (Fork.ofι h ⋯).ι = s.ι ≫ k
p : s.pt ⟶ (PullbackCone.mk f g comm).pt
left : p ≫ (PullbackCone.mk f g comm).fst = l
hp₂ : p ≫ (PullbackCone.mk f g comm).snd = s.ι
m : s.pt ⟶ (Fork.ofι g ⋯).pt
w : m ≫ (Fork.ofι g ⋯).ι = s.ι
z : m ≫ g = p ≫ g
this : Mono h
⊢ m ≫ (PullbackCone.mk f g comm).fst = p ≫ (PullbackCone.mk f g comm).fst
have h₀ : (m ≫ f) ≫ h = (p ≫ f) ≫ h
Tactic: simp only [PullbackCone.mk_π_app, ← cancel_mono h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ v ≫ h.left = v ≫ h.right
have apply : z ≫ v ≫ h.left = z ≫ v ≫ h.right
Tactic: apply (cancel_epi z).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ z ≫ v ≫ h.left = z ≫ v ≫ h.right
have rw : (u ≫ f) ≫ h.left = z ≫ v ≫ h.right
Tactic: rw [← Category.assoc, ← eq_whisker sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = z ≫ v ≫ h.right
have rw : (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
Tactic: rw [← Category.assoc, ← eq_whisker sq.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ z ≫ v ≫ h.left = z ≫ v ≫ h.right
have repeat : (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
Tactic: repeat (rw [← Category.assoc, ← eq_whisker sq.w])
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ sq.HasLift
have this₁ : v ≫ h.left = v ≫ h.right
Tactic: have : v ≫ h.left = v ≫ h.right := by
        apply (cancel_epi z).1
        repeat (rw [← Category.assoc, ← eq_whisker sq.w])
        simp only [Category.assoc, RegularMono.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this_1 : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ h.left = v ≫ h.right
⊢ sq.HasLift
have obtain : ∀ (t : B ⟶ X) (ht : t ≫ f = v), sq.HasLift
Tactic: obtain ⟨t, ht⟩ := RegularMono.lift' _ _ this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this_1 : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
this : v ≫ h.left = v ≫ h.right
t : B ⟶ X
ht : t ≫ f = v
⊢ sq.HasLift
have refine : (z ≫ t) ≫ f = u ≫ f
Tactic: refine CommSq.HasLift.mk' ⟨t, (cancel_mono f).1 ?_, ht⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk g
h : RegularEpi f
⊢ (h.left ≫ Arrow.Hom.left e.hom) ≫ g = (h.right ≫ Arrow.Hom.left e.hom) ≫ g
have simp : h.left ≫ f ≫ Arrow.Hom.right e.hom = h.right ≫ f ≫ Arrow.Hom.right e.hom
Tactic: simp only [Category.assoc, Arrow.w_mk_right, Arrow.mk_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk g
h : RegularEpi f
⊢ h.left ≫ f ≫ Arrow.Hom.right e.hom = h.right ≫ f ≫ Arrow.Hom.right e.hom
have rw : h.right ≫ f ≫ Arrow.Hom.right e.hom = h.right ≫ f ≫ Arrow.Hom.right e.hom
Tactic: rw [reassoc_of% h.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
g h : X ⟶ Y
inst_1 : HasColimit (parallelPair g h)
s : Cofork g h
m : (Cofork.ofπ (P := coequalizer g h) (coequalizer.π g h) ⋯).pt ⟶ s.pt
w : (Cofork.ofπ (P := coequalizer g h) (coequalizer.π g h) ⋯).π ≫ m = s.π
⊢ m = (fun (s : Cofork g h) ↦ (colimit.desc (parallelPair g h) s : colimit (parallelPair g h) ⟶ s.pt)) s
have h₁ : coequalizer.π g h ≫ m =
  CategoryStruct.comp (Y := coequalizer g h) (coequalizer.π g h)
    ((fun (s : Cofork g h) ↦ (colimit.desc (parallelPair g h) s : colimit (parallelPair g h) ⟶ s.pt)) s)
Tactic: apply coequalizer.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst_1 : HasPullback f f
inst_2 : Epi f
h :
  ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄,
    Eq (α := pullback f f ⟶ Z) (pullback.fst f f ≫ g) (pullback.snd f f ≫ g) → ∃ (u : B ⟶ Z), f ≫ u = g
⊢ IsRegularEpi f
have refine : (s : Cofork (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) →
  { l :
    Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f sorry) ⟶ s.pt //
    Cofork.π (Cofork.ofπ f sorry) ≫ l = s.π ∧
      ∀
        {m :
          Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f sorry) ⟶
            s.pt},
        Cofork.π (Cofork.ofπ f sorry) ≫ m = s.π → m = l }
Tactic: refine ⟨⟨regularEpiOfKernelPair _ <| Cofork.IsColimit.mk' _ fun s ↦ ?_⟩⟩