awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
this : k = J.fst default ∨ k = J.snd default
⊢ k = J.snd default
have inl : ∀ (this : k = J.fst default), k = J.snd default
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
this : k = J.fst default ∨ k = J.snd default
inl : ∀ (this : k = J.fst default), k = J.snd default
⊢ k = J.snd default
have inr : ∀ (this : k = J.snd default), k = J.snd default
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
⊢ I.right k = I.right (J.snd default)
have obtain : ∀ (hk : ¬J.snd default = J.fst default), I.right (J.snd default) = I.right (J.snd default)
Tactic: obtain rfl : k = J.snd default := by
            have := h.symm.le (Set.mem_univ k)
            push _ ∈ _ at this
            tauto
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
⊢ ∀ (a : J.L),
    Eq (α := I.left a ⟶ s.pt)
      (I.fst a ≫
        (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr : I.right k ⟶ s.pt))
          (J.fst a))
      (I.snd a ≫
        (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr : I.right k ⟶ s.pt))
          (J.snd a))
have rw : Eq (α := I.left default ⟶ s.pt)
  (I.fst default ≫
    (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom sorry ≫ s.inl else eqToHom sorry ≫ s.inr : I.right k ⟶ s.pt))
      (J.fst default))
  (I.snd default ≫
    (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom sorry ≫ s.inl else eqToHom sorry ≫ s.inr : I.right k ⟶ s.pt))
      (J.snd default))
Tactic: rw [Unique.forall_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
⊢ (multicofork h h' s).π (J.fst default) = s.inl
have dsimp : (if hk : J.fst default = J.fst default then eqToHom sorry ≫ s.inl else eqToHom sorry ≫ s.inr) = s.inl
Tactic: dsimp only [multicofork, ofπ, π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
⊢ (if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inl
have rw : eqToHom sorry ≫ s.inl = s.inl
Tactic: rw [dif_pos rfl, eqToHom_refl, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
rw : eqToHom ⋯ ≫ s.inl = s.inl
⊢ (if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inl
have rw₁ : 𝟙 (I.right (J.fst default)) ≫ s.inl = s.inl
Tactic: rw [dif_pos rfl, eqToHom_refl, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
rw : eqToHom ⋯ ≫ s.inl = s.inl
rw₁ : 𝟙 (I.right (J.fst default)) ≫ s.inl = s.inl
⊢ (if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inl
have rw₂ : s.inl = s.inl
Tactic: rw [dif_pos rfl, eqToHom_refl, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
⊢ (multicofork h h' s).π (J.snd default) = s.inr
have dsimp : (if hk : J.snd default = J.fst default then eqToHom sorry ≫ s.inl else eqToHom sorry ≫ s.inr) = s.inr
Tactic: dsimp only [multicofork, ofπ, π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
⊢ (if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inr
have rw : eqToHom sorry ≫ s.inr = s.inr
Tactic: rw [dif_neg h'.symm, eqToHom_refl, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
rw : eqToHom ⋯ ≫ s.inr = s.inr
⊢ (if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inr
have rw₁ : 𝟙 (I.right (J.snd default)) ≫ s.inr = s.inr
Tactic: rw [dif_neg h'.symm, eqToHom_refl, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
rw : eqToHom ⋯ ≫ s.inr = s.inr
rw₁ : 𝟙 (I.right (J.snd default)) ≫ s.inr = s.inr
⊢ (if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inr
have rw₂ : s.inr = s.inr
Tactic: rw [dif_neg h'.symm, eqToHom_refl, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ m =
    (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
        (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
      s
have apply : ∀ (a : J.R),
  c.π a ≫ m =
    c.π a ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s
Tactic: apply Multicofork.IsColimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
⊢ c.π k ≫ m =
    c.π k ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s
have this : Membership.mem (γ := Set J.R) {J.fst default, J.snd default} k
Tactic: have := h.symm.le (Set.mem_univ k)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
this : Membership.mem (γ := Set J.R) {J.fst default, J.snd default} k
⊢ c.π k ≫ m =
    c.π k ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s
have this₁ : k = J.fst default ∨ k = J.snd default
Tactic: push _ ∈ _ at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
this : k = J.fst default ∨ k = J.snd default
⊢ c.π k ≫ m =
    c.π k ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s
have inl : Eq (α := I.right (J.fst default) ⟶ s.pt) (c.π (J.fst default) ≫ m)
  (c.π (J.fst default) ≫
    (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
        (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
      s)
Tactic: obtain rfl | rfl := this
Cleared hypotheses: k, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
this : k = J.fst default ∨ k = J.snd default
inl :
  Eq (α := I.right (J.fst default) ⟶ s.pt) (c.π (J.fst default) ≫ m)
    (c.π (J.fst default) ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s)
⊢ c.π k ≫ m =
    c.π k ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s
have inr : Eq (α := I.right (J.snd default) ⟶ s.pt) (c.π (J.snd default) ≫ m)
  (c.π (J.snd default) ≫
    (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
        (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
      s)
Tactic: obtain rfl | rfl := this
Cleared hypotheses: k, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
W : D
h : @NormalMono.Z _ _ _ _ inst_3 (F.map f) _ ⟶ W
⊢ F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
have rw : (F.map f ≫ NormalMono.g) ≫ h = 0 ≫ h
Tactic: rw [← Category.assoc, eq_whisker hf.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
W : D
h : @NormalMono.Z _ _ _ _ inst_3 (F.map f) _ ⟶ W
rw : (F.map f ≫ NormalMono.g) ≫ h = 0 ≫ h
⊢ F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
have rw₁ : Eq (α := F.obj X ⟶ W) (0 ≫ h) (0 ≫ h)
Tactic: rw [← Category.assoc, eq_whisker hf.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ Eq (α := F.obj X ⟶ F.obj (F.objPreimage (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _)))
    (F.map (f ≫ F.preimage (NormalMono.g ≫ Iso.inv (F.objObjPreimageIso (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _)))))
    (F.map 0)
have reassoc' : ∀ {W : D} (h : @NormalMono.Z _ _ _ _ inst_3 (F.map f) _ ⟶ W), F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
Tactic: have reassoc' {W : D} (h : hf.Z ⟶ W) : F.map f ≫ hf.g ≫ h = 0 ≫ h := by
      rw [← Category.assoc, eq_whisker hf.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (g ≫ k ≫ NormalMono.g) 0
have reassoc' : ∀ {W : C} (h' : S ⟶ W), f ≫ h ≫ h' = g ≫ k ≫ h'
Tactic: have reassoc' {W : C} (h' : S ⟶ W) : f ≫ h ≫ h' = g ≫ k ≫ h' := by
      simp only [← Category.assoc, eq_whisker comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
reassoc' : ∀ {W : C} (h' : S ⟶ W), f ≫ h ≫ h' = g ≫ k ≫ h'
⊢ Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (g ≫ k ≫ NormalMono.g) 0
have rw : Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (f ≫ h ≫ NormalMono.g) 0
Tactic: rw [← reassoc', hn.w, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
reassoc' : ∀ {W : C} (h' : S ⟶ W), f ≫ h ≫ h' = g ≫ k ≫ h'
rw : Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (f ≫ h ≫ NormalMono.g) 0
⊢ Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (g ≫ k ≫ NormalMono.g) 0
have rw₁ : Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (f ≫ 0) 0
Tactic: rw [← reassoc', hn.w, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
reassoc' : ∀ {W : C} (h' : S ⟶ W), f ≫ h ≫ h' = g ≫ k ≫ h'
rw : Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (f ≫ h ≫ NormalMono.g) 0
rw₁ : Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (f ≫ 0) 0
⊢ Eq (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) (g ≫ k ≫ NormalMono.g) 0
have rw₂ : Eq.{v₁ + 1} (α := P ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) 0 0
Tactic: rw [← reassoc', hn.w, HasZeroMorphisms.comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hn : NormalMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
gr : RegularMono g := regularOfIsPullbackSndOfRegular (NormalMono.regularMono h) comm t
⊢ IsLimit (F := parallelPair (Y := @NormalMono.Z _ _ _ _ inst_1 h _) (k ≫ NormalMono.g) 0) (KernelFork.ofι g ⋯)
have q : Eq (α := R ⟶ @NormalMono.Z _ _ _ _ inst_1 h _) 0 (k ≫ 0)
Tactic: have q := (HasZeroMorphisms.comp_zero k hn.Z).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (f' ≫ Arrow.Hom.right e.inv ≫ g) 0
have this : Arrow.Hom.left e.inv ≫ (Arrow.mk f).hom = (Arrow.mk f').hom ≫ Arrow.Hom.right e.inv
Tactic: have := Arrow.w e.inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.inv ≫ f = f' ≫ Arrow.Hom.right e.inv
⊢ Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (f' ≫ Arrow.Hom.right e.inv ≫ g) 0
have rw : Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (Arrow.Hom.left e.inv ≫ f ≫ g) 0
Tactic: rw [← reassoc_of% this, hf.w, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.inv ≫ f = f' ≫ Arrow.Hom.right e.inv
rw : Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (Arrow.Hom.left e.inv ≫ f ≫ g) 0
⊢ Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (f' ≫ Arrow.Hom.right e.inv ≫ g) 0
have rw₁ : Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (Arrow.Hom.left e.inv ≫ 0) 0
Tactic: rw [← reassoc_of% this, hf.w, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
this : Arrow.Hom.left e.inv ≫ f = f' ≫ Arrow.Hom.right e.inv
rw : Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (Arrow.Hom.left e.inv ≫ f ≫ g) 0
rw₁ : Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (Arrow.Hom.left e.inv ≫ 0) 0
⊢ Eq (α := X' ⟶ @Z _ _ _ _ inst_1 f _) (f' ≫ Arrow.Hom.right e.inv ≫ g) 0
have rw₂ : Eq.{v₁ + 1} (α := X' ⟶ @Z _ _ _ _ inst_1 f _) 0 0
Tactic: rw [← reassoc_of% this, hf.w, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
⊢ IsLimit (KernelFork.ofι f' ⋯)
have refine_1 : parallelPair (X := Y) (Y := @Z _ _ _ _ inst_1 f _) g 0 ≅
  parallelPair (Y := @Z _ _ _ _ inst_1 f _) (Arrow.Hom.right e.inv ≫ g) 0
Tactic: refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : NormalMono f
X' Y' : C
f' : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk f'
refine_1 :
  parallelPair (X := Y) (Y := @Z _ _ _ _ inst_1 f _) g 0 ≅
    parallelPair (Y := @Z _ _ _ _ inst_1 f _) (Arrow.Hom.right e.inv ≫ g) 0
⊢ IsLimit (KernelFork.ofι f' ⋯)
have refine_2 : Functor.obj
    (Cone.postcompose
      (Iso.hom
        (parallelPair.ext (Functor.mapIso Arrow.rightFunc e)
          (Iso.refl
            (Functor.obj.{0, v₁, 0, u₁} (parallelPair (X := Y) (Y := @Z _ _ _ _ inst_1 f _) g 0)
              WalkingParallelPair.one))
          sorry sorry)))
    (KernelFork.ofι f sorry) ≅
  KernelFork.ofι f' sorry
Tactic: refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
inst_2 : IsNormalMonoCategory.{v₁, u₁} C
X_1 Y_1 : C
f : X_1 ⟶ Y_1
h : Mono f
⊢ IsRegularMono f
have haveI : ∀ (this : NormalMono f), IsRegularMono f
Tactic: haveI := normalMonoOfMono f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
W : C
h' : R ⟶ W
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')
have rw : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) ((NormalEpi.g ≫ g) ≫ h') (0 ≫ h')
Tactic: rw [← Category.assoc, eq_whisker gn.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
W : C
h' : R ⟶ W
rw : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) ((NormalEpi.g ≫ g) ≫ h') (0 ≫ h')
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')
have rw₁ : Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (0 ≫ h') (0 ≫ h')
Tactic: rw [← Category.assoc, eq_whisker gn.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
gn : NormalEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ S) ((NormalEpi.g ≫ f) ≫ h) 0
have reassoc' : ∀ {W : C} (h' : R ⟶ W), Eq (α := @NormalEpi.W _ _ _ _ inst_1 g _ ⟶ W) (NormalEpi.g ≫ g ≫ h') (0 ≫ h')
Tactic: have reassoc' {W : C} (h' : R ⟶ W) : gn.g ≫ g ≫ h' = 0 ≫ h' := by
      rw [← Category.assoc, eq_whisker gn.w]