awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 Z_1 : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
Y : Subobject.{v₁, u₁} X
W Z : Subobject.{v₁, u₁} (Functor.obj underlying Y)
mp :
  Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (W.arrow ≫ Y.arrow)) ⋯ ≤
      Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (Z.arrow ≫ Y.arrow)) ⋯ →
    W ≤ Z
⊢ Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (W.arrow ≫ Y.arrow)) ⋯ ≤
      Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (Z.arrow ≫ Y.arrow)) ⋯ ↔
    W ≤ Z
have mpr : W ≤ Z →
  Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (W.arrow ≫ Y.arrow)) sorry ≤
    Subtype.mk (p := fun (x : Subobject.{v₁, u₁} X) ↦ x ∈ Set.Iic Y) (mk (Z.arrow ≫ Y.arrow)) sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
y : Subobject.{v, u} Y
h : W ⟶ X
⊢ ((Subobject.pullback f).obj y).Factors h ↔ y.Factors (h ≫ f)
have refine : ∀ (hf : ((Subobject.pullback f).obj y).Factors h), y.Factors (h ≫ f)
Tactic: refine ⟨fun hf ↦ ?_, fun hF ↦ pullback_factors f y h hF⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
y : Subobject.{v, u} Y
h : W ⟶ X
hf : ((Subobject.pullback f).obj y).Factors h
⊢ y.Factors (h ≫ f)
have rw : (Functor.obj representative y).Factors (h ≫ f)
Tactic: rw [factors_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
y : Subobject.{v, u} Y
h : W ⟶ X
hf : ((Subobject.pullback f).obj y).Factors h
⊢ (Functor.obj representative y).Factors (h ≫ f)
have h₁ : (((Subobject.pullback f).obj y).factorThru h hf ≫ pullbackπ f y) ≫ (Functor.obj representative y).arrow = h ≫ f
Tactic: use Subobject.factorThru _ _ hf ≫ Subobject.pullbackπ f y
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
⊢ (equalizerSubobject f g).arrow ≫ f = (equalizerSubobject f g).arrow ≫ g
have rw : Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
  ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ f)
  ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ g)
Tactic: rw [← equalizerSubobject_arrow, Category.assoc, Category.assoc, equalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
rw :
  Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
    ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ f)
    ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ g)
⊢ (equalizerSubobject f g).arrow ≫ f = (equalizerSubobject f g).arrow ≫ g
have rw₁ : Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
  (Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g ≫ f)
  ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ g)
Tactic: rw [← equalizerSubobject_arrow, Category.assoc, Category.assoc, equalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
rw :
  Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
    ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ f)
    ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ g)
rw₁ :
  Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
    (Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g ≫ f)
    ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ g)
⊢ (equalizerSubobject f g).arrow ≫ f = (equalizerSubobject f g).arrow ≫ g
have rw₂ : Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
  (Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g ≫ f)
  (Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g ≫ g)
Tactic: rw [← equalizerSubobject_arrow, Category.assoc, Category.assoc, equalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
rw :
  Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
    ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ f)
    ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ g)
rw₁ :
  Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
    (Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g ≫ f)
    ((Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g) ≫ g)
rw₂ :
  Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
    (Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g ≫ f)
    (Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g ≫ g)
⊢ (equalizerSubobject f g).arrow ≫ f = (equalizerSubobject f g).arrow ≫ g
have rw₃ : Eq (α := Functor.obj underlying (equalizerSubobject f g) ⟶ Y)
  (Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g ≫ g)
  (Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g ≫ g)
Tactic: rw [← equalizerSubobject_arrow, Category.assoc, Category.assoc, equalizer.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
w : (equalizerSubobject f g).Factors h
⊢ h ≫ f = h ≫ g
have rw : ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ f =
  ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g
Tactic: rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp,
      Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
w : (equalizerSubobject f g).Factors h
rw :
  ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ f =
    ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g
⊢ h ≫ f = h ≫ g
have rw₁ : (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ f =
  ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g
Tactic: rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp,
      Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
w : (equalizerSubobject f g).Factors h
rw :
  ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ f =
    ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g
rw₁ :
  (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ f =
    ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g
⊢ h ≫ f = h ≫ g
have rw₂ : (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ g =
  ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g
Tactic: rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp,
      Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
w : (equalizerSubobject f g).Factors h
rw :
  ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ f =
    ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g
rw₁ :
  (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ f =
    ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g
rw₂ :
  (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ g =
    ((equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow) ≫ g
⊢ h ≫ f = h ≫ g
have rw₃ : (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ g =
  (equalizerSubobject f g).factorThru h w ≫ (equalizerSubobject f g).arrow ≫ g
Tactic: rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp,
      Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
⊢ (Subobject.pullback h).obj (equalizerSubobject f g) = equalizerSubobject (h ≫ f) (h ≫ g)
have refine_1 : (equalizerSubobject (h ≫ f) (h ≫ g)).Factors ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow
Tactic: refine skeletal _ ⟨iso_of_both_ways (homOfFactors ?_) (homOfFactors ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
refine_1 : (equalizerSubobject (h ≫ f) (h ≫ g)).Factors ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow
⊢ (Subobject.pullback h).obj (equalizerSubobject f g) = equalizerSubobject (h ≫ f) (h ≫ g)
have refine_2 : ((Subobject.pullback h).obj (equalizerSubobject f g)).Factors (equalizerSubobject (h ≫ f) (h ≫ g)).arrow
Tactic: refine skeletal _ ⟨iso_of_both_ways (homOfFactors ?_) (homOfFactors ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
⊢ (equalizerSubobject (h ≫ f) (h ≫ g)).Factors ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow
have refine_1 : ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ f =
  ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
Tactic: apply equalizerSubobject_factors
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
have this : pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow =
  ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h
Tactic: have := (Subobject.isPullback h (equalizerSubobject f g)).w
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
this :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
have refine_1 : pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ f =
  ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
Tactic: rw [← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      ← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      equalizerSubobject_arrow_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
this :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h
refine_1 :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
have refine_1₁ : Eq (α := Functor.obj underlying ((Subobject.pullback h).obj (equalizerSubobject f g)) ⟶ Y)
  (pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ f)
  (pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ g)
Tactic: rw [← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      ← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      equalizerSubobject_arrow_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
this :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h
refine_1 :
  pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
refine_1₁ :
  Eq (α := Functor.obj underlying ((Subobject.pullback h).obj (equalizerSubobject f g)) ⟶ Y)
    (pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ f)
    (pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ g)
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
have refine_1₂ : Eq (α := Functor.obj underlying ((Subobject.pullback h).obj (equalizerSubobject f g)) ⟶ Y)
  (pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ g)
  (pullbackπ h (equalizerSubobject f g) ≫ (equalizerSubobject f g).arrow ≫ g)
Tactic: rw [← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      ← reassoc_of% (Subobject.isPullback h (equalizerSubobject f g)).w,
      equalizerSubobject_arrow_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).Factors (equalizerSubobject (h ≫ f) (h ≫ g)).arrow
have refine_2 : (equalizerSubobject f g).Factors ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h)
Tactic: apply pullback_factors
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
⊢ (equalizerSubobject f g).Factors ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h)
have refine_2 : ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g
Tactic: apply equalizerSubobject_factors
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
⊢ ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g
have refine_2 : (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g
Tactic: rw [assoc, assoc, equalizerSubobject_arrow_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
refine_2 : (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g
⊢ ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g
have refine_2₁ : (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ f = (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ g
Tactic: rw [assoc, assoc, equalizerSubobject_arrow_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
W : C
h : W ⟶ X
inst_2 : HasPullbacks.{v, u} C
refine_2 : (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g
refine_2₁ : (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ f = (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ g
⊢ ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g
have refine_2₂ : (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ g = (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ g
Tactic: rw [assoc, assoc, equalizerSubobject_arrow_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
⊢ (kernelSubobject f).arrow ≫ f = 0
have rw : Eq (α := Functor.obj underlying (kernelSubobject f) ⟶ Y) ((Iso.hom (kernelSubobjectIso f) ≫ kernel.ι f) ≫ f) 0
Tactic: rw [← kernelSubobject_arrow]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
⊢ h ≫ f = 0
have rw : ((kernelSubobject f).factorThru h w ≫ (kernelSubobject f).arrow) ≫ f = 0
Tactic: rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp,
      comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
rw : ((kernelSubobject f).factorThru h w ≫ (kernelSubobject f).arrow) ≫ f = 0
⊢ h ≫ f = 0
have rw₁ : (kernelSubobject f).factorThru h w ≫ (kernelSubobject f).arrow ≫ f = 0
Tactic: rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp,
      comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
rw : ((kernelSubobject f).factorThru h w ≫ (kernelSubobject f).arrow) ≫ f = 0
rw₁ : (kernelSubobject f).factorThru h w ≫ (kernelSubobject f).arrow ≫ f = 0
⊢ h ≫ f = 0
have rw₂ : Eq (α := W ⟶ Y) ((kernelSubobject f).factorThru h w ≫ 0) 0
Tactic: rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp,
      comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
W : C
h : W ⟶ X
w : (kernelSubobject f).Factors h
rw : ((kernelSubobject f).factorThru h w ≫ (kernelSubobject f).arrow) ≫ f = 0
rw₁ : (kernelSubobject f).factorThru h w ≫ (kernelSubobject f).arrow ≫ f = 0
rw₂ : Eq (α := W ⟶ Y) ((kernelSubobject f).factorThru h w ≫ 0) 0
⊢ h ≫ f = 0
have rw₃ : Eq.{v + 1} (α := W ⟶ Y) 0 0
Tactic: rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp,
      comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ factorThruKernelSubobject f h w ≫ (kernelSubobject f).arrow = h
have dsimp : (kernelSubobject f).factorThru h sorry ≫ (kernelSubobject f).arrow = h
Tactic: dsimp [factorThruKernelSubobject]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z_1 : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X ⟶ Y
inst_2 : HasKernel f_1
f : X ⟶ Y
inst_3 : HasKernel f
Z : C
h : Y ⟶ Z
inst_4 : Mono h
⊢ IsIso (Y := Functor.obj underlying (kernelSubobject (f ≫ h))) ((kernelSubobject f).ofLE (kernelSubobject (f ≫ h)) ⋯)
have rw : IsIso (X := Functor.obj underlying (kernelSubobject f)) (Y := Functor.obj underlying (kernelSubobject (f ≫ h)))
  (Iso.hom (underlyingIso (kernel.ι f)) ≫
      CategoryStruct.comp (Y := kernel (f ≫ h)) (Iso.inv (kernelCompMono f h) : kernel f ⟶ kernel (f ≫ h))
        (Iso.inv (underlyingIso (kernel.ι (f ≫ h))) :
          kernel (f ≫ h) ⟶ Functor.obj underlying (Subobject.mk (A := kernel (f ≫ h)) (kernel.ι (f ≫ h)))) :
    Functor.obj underlying (Subobject.mk (A := kernel f) (kernel.ι f)) ⟶
      Functor.obj underlying (Subobject.mk (A := kernel (f ≫ h)) (kernel.ι (f ≫ h))))
Tactic: rw [ofLE_mk_le_mk_of_comm (kernelCompMono f h).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z_1 : C
inst_1 : HasZeroMorphisms.{v, u} C
f_1 : X ⟶ Y
inst_2 : HasKernel f_1
f : X ⟶ Y
inst_3 : HasKernel f
Z : C
h : Y ⟶ Z
inst_4 : Mono h
rw :
  IsIso (X := Functor.obj underlying (kernelSubobject f)) (Y := Functor.obj underlying (kernelSubobject (f ≫ h)))
    (Iso.hom (underlyingIso (kernel.ι f)) ≫
        CategoryStruct.comp (Y := kernel (f ≫ h)) (Iso.inv (kernelCompMono f h) : kernel f ⟶ kernel (f ≫ h))
          (Iso.inv (underlyingIso (kernel.ι (f ≫ h))) :
            kernel (f ≫ h) ⟶ Functor.obj underlying (Subobject.mk (A := kernel (f ≫ h)) (kernel.ι (f ≫ h)))) :
      Functor.obj underlying (Subobject.mk (A := kernel f) (kernel.ι f)) ⟶
        Functor.obj underlying (Subobject.mk (A := kernel (f ≫ h)) (kernel.ι (f ≫ h))))
⊢ IsIso (Y := Functor.obj underlying (kernelSubobject (f ≫ h))) ((kernelSubobject f).ofLE (kernelSubobject (f ≫ h)) ⋯)
have rw₁ : Eq (α := kernel f ⟶ X)
  (CategoryStruct.comp (Y := kernel (f ≫ h)) (Iso.inv (kernelCompMono f h) : kernel f ⟶ kernel (f ≫ h))
    (kernel.ι (f ≫ h) : kernel (f ≫ h) ⟶ X))
  (kernel.ι f)
Tactic: rw [ofLE_mk_le_mk_of_comm (kernelCompMono f h).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasCokernels.{v, u} C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Eq (α := (Subobject.{v, u} (op X))ᵒᵈ)
    ((fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦
        (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)) : Subobject.{v, u} (op X)))
      A (i.hom ≫ g) hf)
    ((fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦
        (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)) : Subobject.{v, u} (op X)))
      B g hg)
have refine_1 : cokernel g ≅ cokernel (i.hom ≫ g)
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ (Iso.op ?_) (Quiver.Hom.unop_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Limits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X_1 ⟶ Y
inst_2 : HasKernel f
inst_3 : HasCokernels.{v, u} C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
refine_1 : cokernel g ≅ cokernel (i.hom ≫ g)
⊢ Eq (α := (Subobject.{v, u} (op X))ᵒᵈ)
    ((fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦
        (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)) : Subobject.{v, u} (op X)))
      A (i.hom ≫ g) hf)
    ((fun (x : C) (f : x ⟶ X) (x_1 : Mono f) ↦
        (Subobject.mk (A := op (cokernel f)) (Quiver.Hom.op (cokernel.π f)) : Subobject.{v, u} (op X)))
      B g hg)
have refine_2 : Eq (α := unop (op X) ⟶ unop (op (cokernel (i.hom ≫ g))))
  (Quiver.Hom.unop
    (CategoryStruct.comp (Y := op (cokernel g))
      (Iso.hom
        (Iso.op
          (Iso.symm
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair (i.hom ≫ g) 0))
              (isCokernelEpiComp (colimit.isColimit (parallelPair g 0)) i.hom sorry)))))
      (Quiver.Hom.op (cokernel.π g))))
  (Quiver.Hom.unop (Quiver.Hom.op (cokernel.π (i.hom ≫ g))))
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ (Iso.op ?_) (Quiver.Hom.unop_inj ?_)