awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
fac : hX.to A ≫ i = 𝟙 X
rw : (i ≫ hX.to A) ≫ i = 𝟙 A ≫ i
rw₁ : i ≫ hX.to A ≫ i = 𝟙 A ≫ i
rw₂ : i ≫ 𝟙 X = 𝟙 A ≫ i
rw₃ : i ≫ 𝟙 X = i
rw₄ rw₅ : i = i
⊢ i ≫ hX.to A = 𝟙 A

Tactic:
rw [← cancel_mono i, assoc, fac, id_comp, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
fac : hX.to A ≫ i = 𝟙 X
e : A ≅ X := { hom := i, inv := hX.to A, hom_inv_id := ⋯, inv_hom_id := fac }
⊢ e.hom ≫ 𝟙 X = i

Tactic:
simp [e]
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsInitial.{v₁, u₁} X
A : C
i : A ⟶ X
w : Mono i
fac : hX.to A ≫ i = 𝟙 X
e : A ≅ X := { hom := i, inv := hX.to A, hom_inv_id := ⋯, inv_hom_id := fac }
⊢ mk i = mk (𝟙 X)

Tactic:
exact mk_eq_mk_of_comm i (𝟙 X) e (by simp [e])

Premises used: CategoryTheory.Subobject.mk_eq_mk_of_comm, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
hX : IsZero.{v₁, u₁} X
⊢ Subsingleton (Subobject.{v₁, u₁} X)

Tactic:
subsingleton_of_isInitial hX.isInitial

Premises used: CategoryTheory.Subobject.subsingleton_of_isInitial, CategoryTheory.Limits.IsZero.isInitial
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : HasZeroObject.{v₁, u₁} C
X : C
h : ¬IsZero.{v₁, u₁} X
⊢ Nontrivial (Subobject.{v₁, u₁} X)

Tactic:
⟨⟨mk (0 : 0 ⟶ X), mk (𝟙 X), fun w => h (IsZero.of_iso (isZero_zero C) (isoOfMkEqMk _ _ w).symm)⟩⟩

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.CategoryStruct.id, Nontrivial.mk, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Subobject.mk, CategoryTheory.Subobject.isoOfMkEqMk, Exists.intro, CategoryTheory.Iso.symm, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
Z : Subobject.{v₁, u₁} (Functor.obj underlying Y)
⊢ (Iso.hom (underlyingIso (Z.arrow ≫ Y.arrow)) ≫ Z.arrow) ≫ Y.arrow = (mk (Z.arrow ≫ Y.arrow)).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
Z : (↑(Set.Iic Y) : Type (max u₁ v₁))
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v₁, u₁} (Functor.obj underlying Y)) underlying
        ((fun (Z : (↑(Set.Iic Y) : Type (max u₁ v₁))) ↦ mk ((↑Z : Subobject X).ofLE Y ⋯)) Z) ⟶
      X)
    (Iso.hom (underlyingIso ((↑Z : Subobject X).ofLE Y ⋯)) ≫ (↑Z : Subobject X).arrow)
    (arrow ((fun (Z : (↑(Set.Iic Y) : Type (max u₁ v₁))) ↦ mk ((↑Z : Subobject X).ofLE Y ⋯)) Z) ≫ Y.arrow)

Tactic:
simp [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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
mpr :
  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)) ⋯
⊢ 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

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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)
h :
  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

Tactic:
exact le_of_comm (((underlyingIso _).inv ≫ ofLE _ _ (Subtype.mk_le_mk.mp h) ≫
        (underlyingIso _).hom)) (by cat_disch)

Premises used: CategoryTheory.Subobject.le_of_comm, CategoryTheory.Subobject.ofLE, CategoryTheory.Subobject.underlyingIso, CategoryTheory.CategoryStruct.comp, Iff.mp, Subtype.mk_le_mk, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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)
h : W ≤ Z
⊢ (Iso.hom (underlyingIso (W.arrow ≫ Y.arrow)) ≫ W.ofLE Z h ≫ Iso.inv (underlyingIso (Z.arrow ≫ Y.arrow))) ≫
      (mk (Z.arrow ≫ Y.arrow)).arrow =
    (mk (W.arrow ≫ Y.arrow)).arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Lattice
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)
h : 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)) ⋯

Tactic:
exact Subtype.mk_le_mk.mpr (le_of_comm
        ((underlyingIso _).hom ≫ ofLE _ _ h ≫ (underlyingIso _).inv) (by simp))

Premises used: Iff.mpr, CategoryTheory.Subobject.le_of_comm, CategoryTheory.Subobject.ofLE, CategoryTheory.Subobject.underlyingIso, CategoryTheory.CategoryStruct.comp, Subtype.mk_le_mk, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 : y.Factors (h ≫ f)
⊢ ((Subobject.pullback f).obj y).Factors h

Tactic:
let h' := Subobject.factorThru _ _ hF
  let w := Subobject.factorThru_arrow _ _ hF
  (factors_iff _ _).mpr
    ⟨(Subobject.isPullback f y).lift h' h w,
      (Subobject.isPullback f y).lift_snd h' h w⟩

Premises used: CategoryTheory.Subobject.factors_iff, Iff.mpr, CategoryTheory.Subobject.factorThru, CategoryTheory.IsPullback.lift_snd, CategoryTheory.Subobject.pullback, CategoryTheory.Subobject.factorThru_arrow, CategoryTheory.Subobject.isPullback, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsPullback.lift, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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)

Tactic:
⟨fun hf ↦ ?_, fun hF ↦ pullback_factors f y h hF⟩

Premises used: CategoryTheory.Limits.pullback_factors, Iff.intro
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
refine : ∀ (hf : ((Subobject.pullback f).obj y).Factors h), y.Factors (h ≫ f)
⊢ ((Subobject.pullback f).obj y).Factors h ↔ y.Factors (h ≫ f)

Tactic:
refine ⟨fun hf ↦ ?_, fun hF ↦ pullback_factors f y h hF⟩
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
rw : (Functor.obj representative y).Factors (h ≫ f)
⊢ y.Factors (h ≫ f)

Tactic:
rw [factors_iff]

Premises used: CategoryTheory.Subobject.factors_iff
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
h₁ : (((Subobject.pullback f).obj y).factorThru h hf ≫ pullbackπ f y) ≫ (Functor.obj representative y).arrow = h ≫ f
⊢ (Functor.obj representative y).Factors (h ≫ f)

Tactic:
use Subobject.factorThru _ _ hf ≫ Subobject.pullbackπ f y

Premises used: CategoryTheory.Subobject.factorThru, CategoryTheory.Subobject.pullbackπ
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
⊢ (((Subobject.pullback f).obj y).factorThru h hf ≫ pullbackπ f y) ≫ (Functor.obj representative y).arrow = h ≫ f

Tactic:
simp [(Subobject.isPullback f y).w]

Premises used: CategoryTheory.Subobject.isPullback, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
⊢ Iso.hom (equalizerSubobjectIso f g) ≫ equalizer.ι f g = (equalizerSubobject f g).arrow

Tactic:
simp [equalizerSubobjectIso]

Premises used: CategoryTheory.Limits.equalizerSubobjectIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
⊢ Iso.inv (equalizerSubobjectIso f g) ≫ (equalizerSubobject f g).arrow = equalizer.ι f g

Tactic:
simp [equalizerSubobjectIso]

Premises used: CategoryTheory.Limits.equalizerSubobjectIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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)
rw₃ 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)
⊢ (equalizerSubobject f g).arrow ≫ f = (equalizerSubobject f g).arrow ≫ g

Tactic:
rw [← equalizerSubobject_arrow, Category.assoc, Category.assoc, equalizer.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.equalizer.condition, CategoryTheory.Limits.equalizerSubobject_arrow
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ equalizerSubobject f f = ⊤

Tactic:
apply mk_eq_top_of_isIso

Premises used: CategoryTheory.Subobject.mk_eq_top_of_isIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 : h ≫ f = h ≫ g
⊢ equalizer.lift h w ≫ (MonoOver.mk (A := equalizer f g) (equalizer.ι f g)).arrow = h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
rw₃ 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

Tactic:
rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp,
      Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.equalizerSubobject_arrow_comp, CategoryTheory.Subobject.factorThru_arrow
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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)

Tactic:
skeletal _ ⟨iso_of_both_ways (homOfFactors ?_) (homOfFactors ?_)⟩

Premises used: CategoryTheory.iso_of_both_ways, Nonempty.intro, CategoryTheory.Subobject.homOfFactors, CategoryTheory.Subobject.skeletal
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
refine_2 : ((Subobject.pullback h).obj (equalizerSubobject f g)).Factors (equalizerSubobject (h ≫ f) (h ≫ g)).arrow
⊢ (Subobject.pullback h).obj (equalizerSubobject f g) = equalizerSubobject (h ≫ f) (h ≫ g)

Tactic:
refine skeletal _ ⟨iso_of_both_ways (homOfFactors ?_) (homOfFactors ?_)⟩

Premises used: CategoryTheory.iso_of_both_ways, Nonempty.intro, CategoryTheory.Subobject.homOfFactors, CategoryTheory.Subobject.skeletal
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 :
  ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ f =
    ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ g
⊢ (equalizerSubobject (h ≫ f) (h ≫ g)).Factors ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow

Tactic:
apply equalizerSubobject_factors

Premises used: CategoryTheory.Limits.equalizerSubobject_factors
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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)
refine_1₂ 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)
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).arrow ≫ h ≫ 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]

Premises used: CategoryTheory.Limits.equalizerSubobject_arrow_comp, CategoryTheory.Limits.equalizerSubobject, CategoryTheory.Subobject.isPullback, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 f g).Factors ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h)
⊢ ((Subobject.pullback h).obj (equalizerSubobject f g)).Factors (equalizerSubobject (h ≫ f) (h ≫ g)).arrow

Tactic:
apply pullback_factors

Premises used: CategoryTheory.Limits.pullback_factors
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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 f g).Factors ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h)

Tactic:
apply equalizerSubobject_factors

Premises used: CategoryTheory.Limits.equalizerSubobject_factors
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
refine_2₂ refine_2₃ :
  (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ g = (equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h ≫ g
⊢ ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ f = ((equalizerSubobject (h ≫ f) (h ≫ g)).arrow ≫ h) ≫ g

Tactic:
rw [assoc, assoc, equalizerSubobject_arrow_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.equalizerSubobject_arrow_comp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
⊢ Iso.hom (kernelSubobjectIso f) ≫ kernel.ι f = (kernelSubobject f).arrow

Tactic:
simp [kernelSubobjectIso]

Premises used: CategoryTheory.Limits.kernelSubobjectIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
⊢ Iso.inv (kernelSubobjectIso f) ≫ (kernelSubobject f).arrow = kernel.ι f

Tactic:
simp [kernelSubobjectIso]

Premises used: CategoryTheory.Limits.kernelSubobjectIso
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
rw : Eq (α := Functor.obj underlying (kernelSubobject f) ⟶ Y) ((Iso.hom (kernelSubobjectIso f) ≫ kernel.ι f) ≫ f) 0
⊢ (kernelSubobject f).arrow ≫ f = 0

Tactic:
rw [← kernelSubobject_arrow]

Premises used: CategoryTheory.Limits.kernelSubobject_arrow
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
⊢ Eq (α := Functor.obj underlying (kernelSubobject f) ⟶ Y) ((Iso.hom (kernelSubobjectIso f) ≫ kernel.ι f) ≫ f) 0

Tactic:
simp only [Category.assoc, kernel.condition, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.kernel.condition
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
⊢ kernel.lift f h w ≫ (MonoOver.mk (A := kernel f) (kernel.ι f)).arrow = h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
rw₃ rw₄ : Eq.{v + 1} (α := W ⟶ Y) 0 0
⊢ h ≫ f = 0

Tactic:
rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp,
      comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Subobject.factorThru_arrow, CategoryTheory.Limits.kernelSubobject_arrow_comp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
dsimp : (kernelSubobject f).factorThru h ⋯ ≫ (kernelSubobject f).arrow = h
⊢ factorThruKernelSubobject f h w ≫ (kernelSubobject f).arrow = h

Tactic:
dsimp [factorThruKernelSubobject]

Premises used: CategoryTheory.Limits.factorThruKernelSubobject
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
⊢ (kernelSubobject f).factorThru h ⋯ ≫ (kernelSubobject f).arrow = h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
⊢ CategoryStruct.comp (Y := kernel f) (factorThruKernelSubobject f h w ≫ Iso.hom (kernelSubobjectIso f)) (kernel.ι f) =
    CategoryStruct.comp (Y := kernel f) (kernel.lift f h w) (kernel.ι f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ ((kernelSubobject f).arrow ≫ Arrow.Hom.left sq) ≫ f' = 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ kernelSubobjectMap sq ≫ (kernelSubobject f').arrow = (kernelSubobject f).arrow ≫ Arrow.Hom.left sq

Tactic:
simp [kernelSubobjectMap]

Premises used: CategoryTheory.Limits.kernelSubobjectMap
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
X' Y' : C
f' : X' ⟶ Y'
inst_3 : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ Eq (α := Functor.obj underlying (kernelSubobject f) ⟶ kernel f')
    (Iso.hom (kernelSubobjectIso f) ≫ kernel.map f f' sq.left sq.right ⋯)
    (kernelSubobjectMap sq ≫ Iso.hom (kernelSubobjectIso f'))

Tactic:
simp [← Iso.comp_inv_eq, kernel_map_comp_kernelSubobjectIso_inv]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
A B : C
⊢ Eq (α := Subobject.{v, u} A) (kernelSubobject (Y := B) 0) ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
inst_1 : HasZeroMorphisms.{v, u} C
f : X ⟶ Y
inst_2 : HasKernel f
⊢ Eq (α := Subobject.{v, u} X) (kernelSubobject (Y := Y) 0) ⊤

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subobject.Limits
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
A : Subobject.{v, u} X
h : A.arrow ≫ f = 0
⊢ CategoryStruct.comp (Y := kernel f) (kernel.lift f A.arrow h) (kernel.ι f) = A.arrow

Tactic:
simp