awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.π.app one = l ≫ s.π.app one
have this : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
Tactic: have : k ≫ ι s ≫ f = l ≫ ι s ≫ f := by
      simp only [← Category.assoc]; exact congrArg (· ≫ f) h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
this : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
rw : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
⊢ k ≫ s.π.app one = l ≫ s.π.app one
have rw₁ : l ≫ s.ι ≫ f = l ≫ s.ι ≫ f
Tactic: rw [s.app_one_eq_ι_comp_left, this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Fork f g
hs : ∀ (s : Fork f g), ∃! l : s.pt ⟶ t.pt, l ≫ t.ι = s.ι
⊢ IsLimit t
have choose : (d : (s : Fork f g) → s.pt ⟶ t.pt) →
  (hd : ∀ (s : Fork f g), (fun (l : s.pt ⟶ t.pt) ↦ l ≫ t.ι = s.ι) (d s)) →
    (hd' : ∀ (s : Fork f g) (y : s.pt ⟶ t.pt), (fun (l : s.pt ⟶ t.pt) ↦ l ≫ t.ι = s.ι) y → y = d s) → IsLimit t
Tactic: choose d hd hd' using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Cofork f g
hs : ∀ (s : Cofork f g), ∃! d : t.pt ⟶ s.pt, t.π ≫ d = s.π
⊢ IsColimit t
have choose : (d : (s : Cofork f g) → t.pt ⟶ s.pt) →
  (hd : ∀ (s : Cofork f g), (fun (d : t.pt ⟶ s.pt) ↦ t.π ≫ d = s.π) (d s)) →
    (hd' : ∀ (s : Cofork f g) (y : t.pt ⟶ s.pt), (fun (d : t.pt ⟶ s.pt) ↦ t.π ≫ d = s.π) y → y = d s) → IsColimit t
Tactic: choose d hd hd' using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app one = s.π.app one
have one : (k ≫ t.ι) ≫ f = s.ι ≫ f
Tactic: simp only [Fork.app_one_eq_ι_comp_left, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s t : Fork f g
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
⊢ i.inv ≫ s.ι = t.ι
have rw : i.inv ≫ i.hom ≫ t.ι = t.ι
Tactic: rw [← w, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s t : Fork f g
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
rw : i.inv ≫ i.hom ≫ t.ι = t.ι
⊢ i.inv ≫ s.ι = t.ι
have rw₁ : t.ι = t.ι
Tactic: rw [← w, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
s t : Fork f_1 g
f : s ⟶ t
⊢ f.hom ≫ t.ι = s.ι
have mk : ∀ (pt : C) (π : Functor.obj (Functor.const WalkingParallelPair) pt ⟶ parallelPair f_1 g)
  (f : { pt := pt, π := π : Cone (parallelPair f_1 g) } ⟶ t), f.hom ≫ t.ι = ι { pt := pt, π := π }
Tactic: cases s
Cleared hypotheses: s, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
t : Fork f_1 g
pt : C
π : Functor.obj (Functor.const WalkingParallelPair) pt ⟶ parallelPair f_1 g
f : { pt := pt, π := π : Cone (parallelPair f_1 g) } ⟶ t
⊢ f.hom ≫ t.ι = ι { pt := pt, π := π }
have mk : ∀ (pt_1 : C) (π_1 : Functor.obj (Functor.const WalkingParallelPair) pt_1 ⟶ parallelPair f_1 g)
  (f : { pt := pt, π := π : Cone (parallelPair f_1 g) } ⟶ { pt := pt_1, π := π_1 }),
  f.hom ≫ ι { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) } = ι { pt := pt, π := π }
Tactic: cases t
Cleared hypotheses: t, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
pt : C
π : Functor.obj (Functor.const WalkingParallelPair) pt ⟶ parallelPair f_1 g
pt_1 : C
π_1 : Functor.obj (Functor.const WalkingParallelPair) pt_1 ⟶ parallelPair f_1 g
f : { pt := pt, π := π : Cone (parallelPair f_1 g) } ⟶ { pt := pt_1, π := π_1 }
⊢ f.hom ≫ ι { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) } = ι { pt := pt, π := π }
have mk : ∀ (hom : { pt := pt, π := π : Cone (parallelPair f_1 g) }.pt ⟶ { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) }.pt)
  (w :
    ∀ (j : WalkingParallelPair),
      hom ≫ { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) }.π.app j = { pt := pt, π := π }.π.app j),
  { hom := hom, w := w :
          ConeMorphism { pt := pt, π := π : Cone (parallelPair f_1 g) }
            { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) } }.hom ≫
      ι { pt := pt_1, π := π_1 : Cone (parallelPair f_1 g) } =
    ι { pt := pt, π := π }
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
s t : Cofork f_1 g
f : s ⟶ t
⊢ s.π ≫ f.hom = t.π
have mk : ∀ (pt : C) (ι : parallelPair f_1 g ⟶ Functor.obj (Functor.const WalkingParallelPair) pt)
  (f : { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ⟶ t),
  Cofork.π { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ≫ f.hom = t.π
Tactic: cases s
Cleared hypotheses: s, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
t : Cofork f_1 g
pt : C
ι : parallelPair f_1 g ⟶ Functor.obj (Functor.const WalkingParallelPair) pt
f : { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ⟶ t
⊢ Cofork.π { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ≫ f.hom = t.π
have mk : ∀ (pt_1 : C) (ι_1 : parallelPair f_1 g ⟶ Functor.obj (Functor.const WalkingParallelPair) pt_1)
  (f : { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ⟶ { pt := pt_1, ι := ι_1 }),
  Cofork.π { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ≫ f.hom = Cofork.π { pt := pt_1, ι := ι_1 }
Tactic: cases t
Cleared hypotheses: t, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
pt : C
ι : parallelPair f_1 g ⟶ Functor.obj (Functor.const WalkingParallelPair) pt
pt_1 : C
ι_1 : parallelPair f_1 g ⟶ Functor.obj (Functor.const WalkingParallelPair) pt_1
f : { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ⟶ { pt := pt_1, ι := ι_1 }
⊢ Cofork.π { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ≫ f.hom = Cofork.π { pt := pt_1, ι := ι_1 }
have mk : ∀
  (hom :
    { pt := pt, ι := ι : Cocone (parallelPair f_1 g) }.pt ⟶ { pt := pt_1, ι := ι_1 : Cocone (parallelPair f_1 g) }.pt)
  (w :
    ∀ (j : WalkingParallelPair),
      { pt := pt, ι := ι : Cocone (parallelPair f_1 g) }.ι.app j ≫ hom = { pt := pt_1, ι := ι_1 }.ι.app j),
  Cofork.π { pt := pt, ι := ι : Cocone (parallelPair f_1 g) } ≫
      { hom := hom, w := w :
          CoconeMorphism { pt := pt, ι := ι : Cocone (parallelPair f_1 g) }
            { pt := pt_1, ι := ι_1 : Cocone (parallelPair f_1 g) } }.hom =
    Cofork.π { pt := pt_1, ι := ι_1 }
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s t : Cofork f g
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π ≫ i.inv = s.π
have rw : t.π = s.π ≫ i.hom
Tactic: rw [Iso.comp_inv_eq, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s t : Cofork f g
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
rw : t.π = s.π ≫ i.hom
⊢ t.π ≫ i.inv = s.π
have rw₁ : t.π = t.π
Tactic: rw [Iso.comp_inv_eq, w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
X Y : C
f g : X ⟶ Y
X' Y' : C
c : Cofork f g
f' g' : X' ⟶ Y'
c' : Cofork f' g'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
e : c.pt ≅ c'.pt
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
comm₃ : e₁.inv ≫ c.π ≫ e.hom = c'.π
i : parallelPair f g ≅ parallelPair f' g' := parallelPair.ext e₀ e₁ ⋯ ⋯
⊢ π ((Cocone.precompose i.inv).obj c) ≫ e.hom = c'.π
have rw : π ((Cocone.precompose i.inv).obj c) ≫ e.hom = (e₁.inv ≫ c.π) ≫ e.hom
Tactic: rw [← comm₃, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h_1 : f = g
s : Fork f g
m : s.pt ⟶ (idFork h_1).pt
h : m ≫ (idFork h_1).ι = s.ι
⊢ m = (fun (s : Fork f g) ↦ s.ι) s
have h₁ : (s.pt ⟶ (idFork h_1).pt) = (s.pt ⟶ X) → m = m ≫ (idFork h_1).ι
Tactic: convert! h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (isoSourceOfSelf f).inv = lift (𝟙 X) ⋯
have h : (isoSourceOfSelf f).inv ≫ ι f f = CategoryStruct.comp (Y := equalizer f f) (lift (𝟙 X) sorry) (ι f f)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
c : PullbackCone s.ι h
⊢ c.snd ≫ h ≫ f = c.snd ≫ h ≫ g
have rw : c.fst ≫ s.ι ≫ f = c.snd ≫ h ≫ g
Tactic: rw [← c.condition_assoc, ← c.condition_assoc, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
c : PullbackCone s.ι h
rw : c.fst ≫ s.ι ≫ f = c.snd ≫ h ≫ g
⊢ c.snd ≫ h ≫ f = c.snd ≫ h ≫ g
have rw₁ : c.fst ≫ s.ι ≫ f = c.fst ≫ s.ι ≫ g
Tactic: rw [← c.condition_assoc, ← c.condition_assoc, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
c : PullbackCone s.ι h
rw : c.fst ≫ s.ι ≫ f = c.snd ≫ h ≫ g
rw₁ : c.fst ≫ s.ι ≫ f = c.fst ≫ s.ι ≫ g
⊢ c.snd ≫ h ≫ f = c.snd ≫ h ≫ g
have rw₂ : c.fst ≫ s.ι ≫ g = c.fst ≫ s.ι ≫ g
Tactic: rw [← c.condition_assoc, ← c.condition_assoc, s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
⊢ ∀ (j : WalkingCospan), m ≫ c.π.app j = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.π.app j
have h₀ : m ≫ c.fst = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.fst
Tactic: apply PullbackCone.equalizer_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
h₀ : m ≫ c.fst = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.fst
⊢ ∀ (j : WalkingCospan), m ≫ c.π.app j = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.π.app j
have h₁ : m ≫ c.snd = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.snd
Tactic: apply PullbackCone.equalizer_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
⊢ m ≫ c.fst = (fun (s' : Fork (h_1 ≫ f) (h_1 ≫ g)) ↦ liftPrecomp h_1 hs hc s') s' ≫ c.fst
have h₀ : m ≫ c.fst = hs.lift (Fork.ofι (s'.ι ≫ h_1) sorry)
Tactic: simp only [liftPrecomp, Fork.ofι_pt, IsLimit.fac, PullbackCone.mk_π_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
⊢ m ≫ c.fst = hs.lift (Fork.ofι (s'.ι ≫ h_1) ⋯)
have h₀ : ∀ (j : WalkingParallelPair), (m ≫ c.fst) ≫ s.π.app j = hs.lift (Fork.ofι (s'.ι ≫ h_1) sorry) ≫ s.π.app j
Tactic: apply hs.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g_1 f g : X ⟶ Y
Z : C
h_1 : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h_1
hc : IsLimit c
s' : Fork (h_1 ≫ f) (h_1 ≫ g)
m : s'.pt ⟶ (precompFork h_1 s c).pt
h : m ≫ (precompFork h_1 s c).ι = s'.ι
⊢ ∀ (j : WalkingParallelPair), (m ≫ c.fst) ≫ s.π.app j = hs.lift (Fork.ofι (s'.ι ≫ h_1) ⋯) ≫ s.π.app j
have h₀ : (m ≫ c.fst) ≫ s.ι = hs.lift (Fork.ofι (s'.ι ≫ h_1) sorry) ≫ s.ι
Tactic: apply Fork.equalizer_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst_2 : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
⊢ CategoryStruct.comp (Y := coequalizer f g) (π f g)
      (CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimMap (parallelPairHom f g f' g' p q wf wg))
        (desc h wh)) =
    q ≫ h
have rw : (parallelPairHom f g f' g' p q wf wg).app one ≫
    CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimit.ι (parallelPair f' g') one) (desc h wh) =
  q ≫ h
Tactic: rw [ι_colimMap_assoc, parallelPairHom_app_one, coequalizer.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst_2 : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
rw :
  (parallelPairHom f g f' g' p q wf wg).app one ≫
      CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimit.ι (parallelPair f' g') one) (desc h wh) =
    q ≫ h
⊢ CategoryStruct.comp (Y := coequalizer f g) (π f g)
      (CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimMap (parallelPairHom f g f' g' p q wf wg))
        (desc h wh)) =
    q ≫ h
have rw₁ : q ≫ CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimit.ι (parallelPair f' g') one) (desc h wh) = q ≫ h
Tactic: rw [ι_colimMap_assoc, parallelPairHom_app_one, coequalizer.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst_2 : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
rw :
  (parallelPairHom f g f' g' p q wf wg).app one ≫
      CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimit.ι (parallelPair f' g') one) (desc h wh) =
    q ≫ h
rw₁ :
  q ≫ CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimit.ι (parallelPair f' g') one) (desc h wh) = q ≫ h
⊢ CategoryStruct.comp (Y := coequalizer f g) (π f g)
      (CategoryStruct.comp (Y := colimit (parallelPair f' g')) (colimMap (parallelPairHom f g f' g' p q wf wg))
        (desc h wh)) =
    q ≫ h
have rw₂ : q ≫ h = q ≫ h
Tactic: rw [ι_colimMap_assoc, parallelPairHom_app_one, coequalizer.π_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
h_1 : f = g
s : Cofork f g
m : (idCofork h_1).pt ⟶ s.pt
h : (idCofork h_1).π ≫ m = s.π
⊢ m = (fun (s : Cofork f g) ↦ s.π) s
have h₁ : ((idCofork h_1).pt ⟶ s.pt) = (Y ⟶ s.pt) → m = (idCofork h_1).π ≫ m
Tactic: convert! h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ (isoTargetOfSelf f).hom = desc (𝟙 Y) ⋯
have h : π f f ≫ (isoTargetOfSelf f).hom = CategoryStruct.comp (Y := coequalizer f f) (π f f) (desc (𝟙 Y) sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
⊢ Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g) ≫ G.map f) (G.map (equalizer.ι f g) ≫ G.map g)
have simp : Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ f)) (G.map (equalizer.ι f g ≫ g))
Tactic: simp only [← G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
⊢ Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ f)) (G.map (equalizer.ι f g ≫ g))
have rw : Eq (α := G.obj (equalizer f g) ⟶ G.obj Y) (G.map (equalizer.ι f g ≫ g)) (G.map (equalizer.ι f g ≫ g))
Tactic: rw [equalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasEqualizer f g
inst_3 : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ Eq (α := G.obj Z ⟶ equalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (equalizer f g)) (G.map (equalizer.lift h w)) (equalizerComparison f g G))
    (equalizer.lift (G.map h) ⋯)
have h₁ : CategoryStruct.comp (Y := equalizer (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (equalizer f g)) (G.map (equalizer.lift h w)) (equalizerComparison f g G))
    (equalizer.ι (G.map f) (G.map g)) =
  CategoryStruct.comp (Y := equalizer (G.map f) (G.map g)) (equalizer.lift (G.map h) sorry)
    (equalizer.ι (G.map f) (G.map g))
Tactic: apply equalizer.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
⊢ Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map f ≫ G.map (coequalizer.π f g))
    (G.map g ≫ G.map (coequalizer.π f g))
have simp : Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (f ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
Tactic: simp only [← G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
⊢ Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (f ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
have rw : Eq (α := G.obj X ⟶ G.obj (coequalizer f g)) (G.map (g ≫ coequalizer.π f g)) (G.map (g ≫ coequalizer.π f g))
Tactic: rw [coequalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
inst_2 : HasCoequalizer f g
inst_3 : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ Eq (α := coequalizer (G.map f) (G.map g) ⟶ G.obj Z)
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G) (G.map (coequalizer.desc h w)))
    (coequalizer.desc (G.map h) ⋯)
have h₁ : CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (coequalizer f g)) (coequalizerComparison f g G) (G.map (coequalizer.desc h w))) =
  CategoryStruct.comp (Y := coequalizer (G.map f) (G.map g)) (coequalizer.π (G.map f) (G.map g))
    (coequalizer.desc (G.map h) sorry)
Tactic: apply coequalizer.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitMono f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
⊢ (s.ι ≫ retraction f) ≫ Fork.ι (coneOfIsSplitMono f) = s.ι
have dsimp : (s.ι ≫ retraction f) ≫ f = s.ι
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitMono f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
⊢ (s.ι ≫ retraction f) ≫ f = s.ι
have rw : s.ι ≫ 𝟙 Y = s.ι
Tactic: rw [Category.assoc, ← s.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm : Mono h
⊢ c.ι ≫ f ≫ h = c.ι ≫ g ≫ h
have simp : (c.ι ≫ f) ≫ h = (c.ι ≫ g) ≫ h
Tactic: simp only [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm : Mono h
s : Fork (f ≫ h) (g ≫ h)
⊢ s.ι ≫ f = s.ι ≫ g
have a : (s.ι ≫ f) ≫ h = (s.ι ≫ g) ≫ h
Tactic: apply hm.right_cancellation
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm_1 : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m ≫ (Fork.ofι c.ι ⋯).ι = s.ι
⊢ m = (↑l : s'.pt ⟶ c.pt)
have apply : m ≫ c.ι = (↑l : s'.pt ⟶ c.pt) ≫ c.ι
Tactic: apply Fork.IsLimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm_1 : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m ≫ (Fork.ofι c.ι ⋯).ι = s.ι
⊢ m ≫ c.ι = (↑l : s'.pt ⟶ c.pt) ≫ c.ι
have hm₁ : m ≫ c.ι = s.ι
Tactic: rw [Fork.ι_ofι] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm_1 : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l : s'.pt ⟶ c.pt // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m ≫ c.ι = s.ι
⊢ m ≫ c.ι = (↑l : s'.pt ⟶ c.pt) ≫ c.ι
have rw : s.ι = (↑l : s'.pt ⟶ c.pt) ≫ c.ι
Tactic: rw [hm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f_1 g : X_1 ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Fork (𝟙 X) f
i : IsLimit c
this : Mono c.ι := ⋯
⊢ c.ι ≫ i.lift (Fork.ofι f ⋯) = 𝟙 c.pt
have rw : c.ι ≫ 𝟙 X = c.ι
Tactic: rw [← cancel_mono_id c.ι, Category.assoc, Fork.IsLimit.lift_ι, Fork.ι_ofι, ← c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitEpi f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
⊢ Cofork.π (coconeOfIsSplitEpi f) ≫ section_ f ≫ s.π = s.π
have dsimp : f ≫ section_ f ≫ s.π = s.π
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g : X_1 ⟶ Y_1
inst_1 : IsSplitEpi f_1
X Y : C
f : X ⟶ Y
inst_2 : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
⊢ f ≫ section_ f ≫ s.π = s.π
have rw : (f ≫ section_ f) ≫ s.π = s.π
Tactic: rw [← Category.assoc, ← s.condition, Category.id_comp]