awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 ⋯) ⟶ s.pt //
    Cofork.π (Cofork.ofπ f ⋯) ≫ l = s.π ∧
      ∀
        {m :
          Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶
            s.pt},
        Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π → m = l }
have choose : (g : B ⟶ s.pt) →
  (hg : f ≫ g = s.π) →
    { 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: choose g hg using h s.condition
-- 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
s : Cofork (X := pullback f f) (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
⊢ { l :
    Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶ s.pt //
    Cofork.π (Cofork.ofπ f ⋯) ≫ l = s.π ∧
      ∀
        {m :
          Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶
            s.pt},
        Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π → m = l }
have refine : ∀ {m : Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f sorry) ⟶ s.pt}
  (hm : Cofork.π (Cofork.ofπ f sorry) ≫ m = s.π), m = g
Tactic: refine ⟨g, hg, fun hm ↦ ?_⟩
-- 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
s : Cofork (X := pullback f f) (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
m : Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶ s.pt
hm : Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π
⊢ m = g
have rwa : f ≫ m = f ≫ g
Tactic: rwa [← cancel_epi f, hg]
-- 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
s : Cofork (X := pullback f f) (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
m : Cocone.pt (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (Cofork.ofπ f ⋯) ⟶ s.pt
hm : Cofork.π (Cofork.ofπ f ⋯) ≫ m = s.π
rwa : f ≫ m = f ≫ g
⊢ m = g
have rwa₁ : f ≫ m = s.π
Tactic: rwa [← cancel_epi f, hg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z : C
g₁ g₂ : Z ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ s.ι.app WalkingParallelPair.one = g₂ ≫ s.ι.app WalkingParallelPair.one
have simp : g₁ ≫ Cofork.π s = g₂ ≫ Cofork.π s
Tactic: simp only [Cofork.app_one_eq_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z : C
g₁ g₂ : Z ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ Cofork.π s = g₂ ≫ Cofork.π s
have rw : g₁ ≫ Cofork.π s = PullbackCone.IsLimit.lift hc g₁ g₂ hg ≫ s.ι.app WalkingParallelPair.zero
Tactic: rw [← PullbackCone.IsLimit.lift_snd hc g₁ g₂ hg,
        Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y B X : C
f : X ⟶ B
inst_1 : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
⊢ ∀ (j : WalkingParallelPair),
    (Cofork.ofπ f ⋯).ι.app j ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) ⋯ = s.ι.app j
have this : f ≫ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) sorry = s.ι.app WalkingParallelPair.one
Tactic: have := EffectiveEpi.fac f (s.ι.app WalkingParallelPair.one) fun g₁ g₂ hg ↦ (by
      simp only [Cofork.app_one_eq_π]
      rw [← PullbackCone.IsLimit.lift_snd hc g₁ g₂ hg,
        Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
      simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 X Y Z : C
p : Y ⟶ X
hp : EffectiveEpiStruct p
p₁ p₂ : Z ⟶ Y
sq : IsPullback p₁ p₂ p p
s : Cofork p₁ p₂
T : C
g₁ g₂ : T ⟶ Y
h : g₁ ≫ p = g₂ ≫ p
⊢ g₁ ≫ s.π = g₂ ≫ s.π
have obtain : ∀ (l : T ⟶ Z) (h : (l ≫ p₁) ≫ p = (l ≫ p₂) ≫ p), (l ≫ p₁) ≫ s.π = (l ≫ p₂) ≫ s.π
Tactic: obtain ⟨l, rfl, rfl⟩ := sq.exists_lift g₁ g₂ h
Cleared hypotheses: g₁, g₂, h
-- 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ (gr.left ≫ f) ≫ h = (gr.right ≫ f) ≫ h
have rw : gr.left ≫ g ≫ k = gr.right ≫ g ≫ k
Tactic: rw [Category.assoc, Category.assoc, 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ IsColimit (Cofork.ofπ h ⋯)
have apply : (s : Cofork (gr.left ≫ f) (gr.right ≫ f)) →
  { l : (Cofork.ofπ h sorry).pt ⟶ s.pt //
    (Cofork.ofπ h sorry).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h sorry).pt ⟶ s.pt}, (Cofork.ofπ h sorry).π ≫ m = s.π → m = l }
Tactic: apply Cofork.IsColimit.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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
⊢ gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
have rw : (gr.left ≫ f) ≫ s.π = gr.right ≫ f ≫ s.π
Tactic: rw [← Category.assoc, ← Category.assoc, s.condition]
-- 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
rw : (gr.left ≫ f) ≫ s.π = gr.right ≫ f ≫ s.π
⊢ gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
have rw₁ : (gr.left ≫ f) ≫ s.π = (gr.right ≫ f) ≫ s.π
Tactic: rw [← Category.assoc, ← Category.assoc, s.condition]
-- 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
rw : (gr.left ≫ f) ≫ s.π = gr.right ≫ f ≫ s.π
rw₁ : (gr.left ≫ f) ≫ s.π = (gr.right ≫ f) ≫ s.π
⊢ gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
have rw₂ : (gr.right ≫ f) ≫ s.π = (gr.right ≫ f) ≫ s.π
Tactic: rw [← Category.assoc, ← Category.assoc, s.condition]
-- 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
⊢ { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
    (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
have l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
Tactic: have l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π := by
      rw [← Category.assoc, ← Category.assoc, s.condition]
-- 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
⊢ { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
    (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
have obtain : (l : (Cofork.ofπ g sorry).pt ⟶ s.pt) →
  (hl : (Cofork.ofπ g sorry).π ≫ l = f ≫ s.π) →
    { l : (Cofork.ofπ h sorry).pt ⟶ s.pt //
      (Cofork.ofπ h sorry).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h sorry).pt ⟶ s.pt}, (Cofork.ofπ h sorry).π ≫ m = s.π → m = l }
Tactic: obtain ⟨l, hl⟩ := Cofork.IsColimit.desc' gr.isColimit (f ≫ Cofork.π s) 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
⊢ { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
    (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
have obtain : (p : (PushoutCocone.mk h k comm).pt ⟶ s.pt) →
  (hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π) →
    (PushoutCocone.mk h k comm).inr ≫ p = l →
      { l : (Cofork.ofπ h sorry).pt ⟶ s.pt //
        (Cofork.ofπ h sorry).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h sorry).pt ⟶ s.pt}, (Cofork.ofπ h sorry).π ≫ m = s.π → m = l }
Tactic: obtain ⟨p, hp₁, _⟩ := PushoutCocone.IsColimit.desc' t _ _ hl.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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
⊢ { l : (Cofork.ofπ h ⋯).pt ⟶ s.pt //
    (Cofork.ofπ h ⋯).π ≫ l = s.π ∧ ∀ {m : (Cofork.ofπ h ⋯).pt ⟶ s.pt}, (Cofork.ofπ h ⋯).π ≫ m = s.π → m = l }
have refine : ∀ {m : (Cofork.ofπ h sorry).pt ⟶ s.pt}, (Cofork.ofπ h sorry).π ≫ m = 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
⊢ m = p
have z : (Cofork.ofπ h sorry).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
Tactic: have z := 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
⊢ m = p
have apply : ∀ (j : WalkingSpan), (PushoutCocone.mk h k comm).ι.app j ≫ m = (PushoutCocone.mk h k comm).ι.app j ≫ p
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk h k comm).ι.app j ≫ m = (PushoutCocone.mk h k comm).ι.app j ≫ p
have this : Epi g
Tactic: have := gr.epi
-- 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk h k comm).ι.app j ≫ m = (PushoutCocone.mk h k comm).ι.app j ≫ p
have h₀ : (PushoutCocone.mk h k comm).inl ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
Tactic: apply (PushoutCocone.mk _ _ comm).coequalizer_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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
h₀ : (PushoutCocone.mk h k comm).inl ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
⊢ ∀ (j : WalkingSpan), (PushoutCocone.mk h k comm).ι.app j ≫ m = (PushoutCocone.mk h k comm).ι.app j ≫ p
have h₁ : (PushoutCocone.mk h k comm).inr ≫ m = (PushoutCocone.mk h k comm).inr ≫ p
Tactic: apply (PushoutCocone.mk _ _ comm).coequalizer_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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (PushoutCocone.mk h k comm).inr ≫ m = (PushoutCocone.mk h k comm).inr ≫ p
have h₁ : (f ≫ h) ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p
Tactic: erw [← cancel_epi g, ← 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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
l₁ : gr.left ≫ f ≫ s.π = gr.right ≫ f ≫ s.π
l : (Cofork.ofπ g ⋯).pt ⟶ s.pt
hl : (Cofork.ofπ g ⋯).π ≫ l = f ≫ s.π
p : (PushoutCocone.mk h k comm).pt ⟶ s.pt
hp₁ : (PushoutCocone.mk h k comm).inl ≫ p = s.π
right : (PushoutCocone.mk h k comm).inr ≫ p = l
m : (Cofork.ofπ h ⋯).pt ⟶ s.pt
w : (Cofork.ofπ h ⋯).π ≫ m = s.π
z : (Cofork.ofπ h ⋯).π ≫ m = (PushoutCocone.mk h k comm).inl ≫ p
this : Epi g
⊢ (f ≫ h) ≫ m = g ≫ (PushoutCocone.mk h k comm).inr ≫ p
have h₁ : (f ≫ h) ≫ m = (f ≫ h) ≫ p
Tactic: erw [← Category.assoc, ← eq_whisker comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : SplitEpiCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Epi f
⊢ IsRegularEpi f
have this : IsSplitEpi f
Tactic: haveI := isSplitEpi_of_epi f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.RegularMono (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : IsRegularEpiCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Epi f
⊢ StrongEpi f
have this : IsRegularEpi f
Tactic: haveI := isRegularEpi_of_regularEpi <| regularEpiOfEpi f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n : ℕ
⊢ functorObj.{v_1, u_1} M N (n + 1) ⟶ functorObj.{v_1, u_1} M N n
have refine_1 : ∀ (m : ℕ) (h : m < n), Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
Tactic: refine Limits.Pi.map fun m ↦ if h : m < n then eqToHom ?_ else
    if h' : m < n + 1 then eqToHom ?_ ≫ f m ≫ eqToHom ?_ else eqToHom ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n : ℕ
refine_1 :
  ∀ (m : ℕ) (h : m < n), Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
⊢ functorObj.{v_1, u_1} M N (n + 1) ⟶ functorObj.{v_1, u_1} M N n
have refine_2 : ∀ (m : ℕ) (h : ¬m < n) (h' : m < n + 1), (if x : m < n + 1 then M m else N m) = M m
Tactic: refine Limits.Pi.map fun m ↦ if h : m < n then eqToHom ?_ else
    if h' : m < n + 1 then eqToHom ?_ ≫ f m ≫ eqToHom ?_ else eqToHom ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n : ℕ
refine_1 :
  ∀ (m : ℕ) (h : m < n), Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
refine_2 : ∀ (m : ℕ) (h : ¬m < n) (h' : m < n + 1), (if x : m < n + 1 then M m else N m) = M m
⊢ functorObj.{v_1, u_1} M N (n + 1) ⟶ functorObj.{v_1, u_1} M N n
have refine_3 : ∀ (m : ℕ) (h : ¬m < n) (h' : m < n + 1), N m = if x : m < n then M m else N m
Tactic: refine Limits.Pi.map fun m ↦ if h : m < n then eqToHom ?_ else
    if h' : m < n + 1 then eqToHom ?_ ≫ f m ≫ eqToHom ?_ else eqToHom ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n : ℕ
refine_1 :
  ∀ (m : ℕ) (h : m < n), Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
refine_2 : ∀ (m : ℕ) (h : ¬m < n) (h' : m < n + 1), (if x : m < n + 1 then M m else N m) = M m
refine_3 : ∀ (m : ℕ) (h : ¬m < n) (h' : m < n + 1), N m = if x : m < n then M m else N m
⊢ functorObj.{v_1, u_1} M N (n + 1) ⟶ functorObj.{v_1, u_1} M N n
have refine_4 : ∀ (m : ℕ) (h : ¬m < n) (h' : ¬m < n + 1),
  Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
Tactic: refine Limits.Pi.map fun m ↦ if h : m < n then eqToHom ?_ else
    if h' : m < n + 1 then eqToHom ?_ ≫ f m ≫ eqToHom ?_ else eqToHom ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : m < n
⊢ Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
have pos : m < n + 1 → M m = M m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : m < n
pos : m < n + 1 → M m = M m
⊢ Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
have neg : ¬m < n + 1 → N m = M m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ (if x : m < n + 1 then M m else N m) = M m
have refine_2 : M m = M m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
h' : m < n + 1
⊢ N m = if x : m < n then M m else N m
have refine_3 : N m = N m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct (goal)
Goal:
C : Type u_1
M N : ℕ → C
inst : Category.{v_1, u_1} C
f : (n : ℕ) → M n ⟶ N n
inst_1 : HasCountableProducts.{v_1, u_1} C
n m : ℕ
h : ¬m < n
h' : ¬m < n + 1
⊢ Eq.{u_1 + 1} (α := C) (if x : m < n + 1 then M m else N m) (if x : m < n then M m else N m)
have refine_4 : N m = N m
Tactic: split_ifs