awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
D : Cocone F
i j : J
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
k : J
f : i ⟶ k
g : j ⟶ k
hfg :
  Eq (α := (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget C (FC := FC) (CC := CC)).map f) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) → (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj k))
        x :
      (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))
h1 : (F ⋙ forget C (FC := FC) (CC := CC)).map f ≫ E.ι.app k = E.ι.app i := ⋯
h2 : (F ⋙ forget C (FC := FC) (CC := CC)).map g ≫ E.ι.app k = E.ι.app j := ⋯
⊢ Eq (α := CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app i) :
          (a : CC (F.obj i)) → CC (((Functor.const J).obj D.pt).obj i))
        x :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) i))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (D.ι.app j) :
          (a : CC (F.obj j)) → CC (((Functor.const J).obj D.pt).obj j))
        y :
      CC (Functor.obj.{r, v, w, u} (Functor.obj (Functor.const J) D.pt) j))
have change : Eq (α := (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app i) :
        (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) →
          (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj i))
      x :
    (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
        (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
          (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
      y :
    (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) j))
Tactic: change E.ι.app i x = E.ι.app j y
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst_1 : (X Y : C) → FunLike.{u_1 + 1, t + 1, t + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{t, v, u, u_1} C FC (CC := CC)
J : Type w
inst_3 : Category.{r, w} J
F : Functor.{r, v, w, u} J C
D : Cocone F
i j : J
x : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj i)
y : ToType.{t, v, u, u_1} (FC := FC) (CC := CC) (F.obj j)
E : Cocone (F ⋙ forget C (FC := FC) (CC := CC)) := Functor.mapCocone (forget C (FC := FC) (CC := CC)) D
k : J
f : i ⟶ k
g : j ⟶ k
hfg :
  Eq (α := (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget C (FC := FC) (CC := CC)).map f) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) → (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj k))
        x :
      (fun (X : Type t) ↦ X) ((F ⋙ forget C (FC := FC) (CC := CC)).obj k))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k))
h1 : (F ⋙ forget C (FC := FC) (CC := CC)).map f ≫ E.ι.app k = E.ι.app i := ⋯
h2 : (F ⋙ forget C (FC := FC) (CC := CC)).map g ≫ E.ι.app k = E.ι.app j := ⋯
⊢ Eq (α := (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app i) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj i)) →
            (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj i))
        x :
      (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
          (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
            (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
        y :
      (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) j))
have rw : Eq (α := (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app k) :
        (a : (F ⋙ forget C).obj k) → ((Functor.const J).obj E.pt).obj i)
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map g) : (a : CC (F.obj j)) → CC (F.obj k)) y : CC (F.obj k)) :
    Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) i)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (E.ι.app j) :
        (a : (fun (X : Type t) ↦ X) ((F ⋙ forget C).obj j)) →
          (fun (X : Type t) ↦ X) (((Functor.const J).obj E.pt).obj j))
      y :
    (fun (X : Type t) ↦ X) (Functor.obj.{r, t, w, t + 1} (Functor.obj (Functor.const J) E.pt) j))
Tactic: rw [← h1, comp_apply, hfg]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures (hypothesis)
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
j : J
x : (↑(F.obj j) : Type (max t w))
hx :
  Eq (α := (↑(colimit F) : Type (max t w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 : (↑(colimit F) : Type (max t w)))
⊢ ∃ (j' : J) (i : j ⟶ j'),
    Eq (α := (↑(F.obj j') : Type (max t w)))
      ((ModuleCat.Hom.hom (F.map i) : (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj j') : Type (max t w))) x :
        (↑(F.obj j') : Type (max t w)))
      (0 : (↑(F.obj j') : Type (max t w)))
have hx₁ : ∃ (k : J) (f : j ⟶ k) (g : j ⟶ k),
  Eq (α := (↑(F.obj k) : Type (max t w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (F.map f) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj k) : Type (max t w)))
        x :
      (↑(F.obj k) : Type (max t w)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (F.map g) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj k) : Type (max t w)))
        0 :
      (↑(F.obj k) : Type (max t w)))
Tactic: rw [show 0 = colimit.ι F j 0 by simp, colimit_rep_eq_iff_exists] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures (goal)
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
j : J
x : (↑(F.obj j) : Type (max t w))
hx :
  ∃ (k : J) (f : j ⟶ k) (g : j ⟶ k),
    Eq (α := (↑(F.obj k) : Type (max t w)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
              (CC := ModuleCat.carrier) (F.map f) :
            (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj k) : Type (max t w)))
          x :
        (↑(F.obj k) : Type (max t w)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
              (CC := ModuleCat.carrier) (F.map g) :
            (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj k) : Type (max t w)))
          0 :
        (↑(F.obj k) : Type (max t w)))
⊢ ∃ (j' : J) (i : j ⟶ j'),
    Eq (α := (↑(F.obj j') : Type (max t w)))
      ((ModuleCat.Hom.hom (F.map i) : (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj j') : Type (max t w))) x :
        (↑(F.obj j') : Type (max t w)))
      (0 : (↑(F.obj j') : Type (max t w)))
have obtain : ∀ (j' : J) (i y : j ⟶ j')
  (g :
    Eq (α := (↑(F.obj j') : Type (max t w)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
              (CC := ModuleCat.carrier) (F.map i) :
            (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj j') : Type (max t w)))
          x :
        (↑(F.obj j') : Type (max t w)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
              (CC := ModuleCat.carrier) (F.map y) :
            (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj j') : Type (max t w)))
          0 :
        (↑(F.obj j') : Type (max t w)))),
  ∃ (j' : J) (i : j ⟶ j'),
    Eq (α := (↑(F.obj j') : Type (max t w)))
      ((ModuleCat.Hom.hom (F.map i) : (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj j') : Type (max t w))) x :
        (↑(F.obj j') : Type (max t w)))
      (0 : (↑(F.obj j') : Type (max t w)))
Tactic: obtain ⟨j', i, y, g⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures (goal)
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
r : R
H : ∃ (j' : J), ∀ (j : J) (x : j' ⟶ j) (c : (↑(F.obj j) : Type (max t w))), r • c = 0 → c = 0
x :
  ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
    ModuleCat.carrier) (colimit F)
hx : r • x = 0
⊢ x = 0
have obtain : ∀ (j : J)
  (x :
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (F.obj j))
  (hx :
    HSMul.hSMul (β :=
        ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
          ModuleCat.carrier) (colimit F))
        r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
                (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
              (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
            x :
          (↑(colimit F) : Type (max t w))) =
      0),
  Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
Tactic: obtain ⟨j, x, rfl⟩ := Concrete.colimit_exists_rep F x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures (hypothesis)
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
r : R
H : ∃ (j' : J), ∀ (j : J) (x : j' ⟶ j) (c : (↑(F.obj j) : Type (max t w))), r • c = 0 → c = 0
j : J
x :
  ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
    ModuleCat.carrier) (F.obj j)
hx :
  HSMul.hSMul (β :=
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
      r
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
              (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
            (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
          x :
        (↑(colimit F) : Type (max t w))) =
    0
⊢ Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
have hx₁ : Eq (α :=
  ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
    ModuleCat.carrier) (colimit F))
  ((ModuleCat.Hom.hom (colimit.ι F j) : (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w))) (r • x) :
    (↑(colimit F) : Type (max t w)))
  (0 :
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
Tactic: rw [← map_smul (colimit.ι F j).hom] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures (goal)
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
r : R
H : ∃ (j' : J), ∀ (j : J) (x : j' ⟶ j) (c : (↑(F.obj j) : Type (max t w))), r • c = 0 → c = 0
j : J
x :
  ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
    ModuleCat.carrier) (F.obj j)
hx :
  Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ModuleCat.Hom.hom (colimit.ι F j) : (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        (r • x) :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
⊢ Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
have obtain : ∀ (j' : J) (i : j ⟶ j')
  (h :
    Eq (α := (↑(F.obj j') : Type (max t w)))
      ((ModuleCat.Hom.hom (F.map i) : (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj j') : Type (max t w))) (r • x) :
        (↑(F.obj j') : Type (max t w)))
      (0 : (↑(F.obj j') : Type (max t w)))),
  Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
Tactic: obtain ⟨j', i, h⟩ := Concrete.colimit_rep_eq_zero (hx := hx)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures (goal)
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
r : R
H : ∃ (j' : J), ∀ (j : J) (x : j' ⟶ j) (c : (↑(F.obj j) : Type (max t w))), r • c = 0 → c = 0
j : J
x :
  ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
    ModuleCat.carrier) (F.obj j)
hx :
  Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ModuleCat.Hom.hom (colimit.ι F j) : (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        (r • x) :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
j' : J
i : j ⟶ j'
h :
  Eq (α := (↑(F.obj j') : Type (max t w)))
    ((ModuleCat.Hom.hom (F.map i) : (a : (↑(F.obj j) : Type (max t w))) → (↑(F.obj j') : Type (max t w))) (r • x) :
      (↑(F.obj j') : Type (max t w)))
    (0 : (↑(F.obj j') : Type (max t w)))
⊢ Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
have obtain : ∀ (j'' : J) (H : ∀ (j : J) (x : j'' ⟶ j) (c : (↑(F.obj j) : Type (max t w))), r • c = 0 → c = 0),
  Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
Tactic: obtain ⟨j'', H⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures (goal)
Goal:
R : Type u_1
inst : Ring R
J : Type w
inst_1 : Category.{r, w} J
F : J ⥤ ModuleCat R
inst_2 :
  PreservesColimit F
    (forget (ModuleCat R) (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier))
inst_3 : IsFiltered.{r, w} J
inst_4 : HasColimit F
r : R
H : ∃ (j' : J), ∀ (j : J) (x : j' ⟶ j) (c : (↑(F.obj j) : Type (max t w))), r • c = 0 → c = 0
x :
  ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
    ModuleCat.carrier) (colimit F)
hx : r • x = 0
⊢ x = 0
have obtain : ∀ (j : J)
  (x :
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (F.obj j))
  (hx :
    HSMul.hSMul (β :=
        ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
          ModuleCat.carrier) (colimit F))
        r
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
                (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
              (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
            x :
          (↑(colimit F) : Type (max t w))) =
      0),
  Eq (α :=
    ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
      ModuleCat.carrier) (colimit F))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w)))
            (CC := ModuleCat.carrier) (Y := colimit F) (colimit.ι F j) :
          (a : (↑(F.obj j) : Type (max t w))) → (↑(colimit F) : Type (max t w)))
        x :
      (↑(colimit F) : Type (max t w)))
    (0 :
      ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type (max t w)) →ₗ[R] (↑x2 : Type (max t w))) (CC :=
        ModuleCat.carrier) (colimit F))
Tactic: classical
  obtain ⟨j, x, rfl⟩ := Concrete.colimit_exists_rep F x
  rw [← map_smul (colimit.ι F j).hom] at hx
  obtain ⟨j', i, h⟩ := Concrete.colimit_rep_eq_zero (hx := hx)
  obtain ⟨j'', H⟩ := H
  simpa [elementwise_of% (colimit.w F), map_zero] using congr(colimit.ι F _
    $(H (IsFiltered.sup {j, j', j''} { ⟨j, j', by simp, by simp, i⟩ })
      (IsFiltered.toSup _ _ <| by simp)
      (F.map (IsFiltered.toSup _ _ <| by simp) x)
      (by rw [← IsFiltered.toSup_commutes (f := i) (mY := by simp) (mf := by simp), F.map_comp,
        ModuleCat.comp_apply, ← map_smul, ← map_smul, h, map_zero])))
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.ConeCategory (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
X Y : CostructuredArrow (const J) F
f : X ⟶ Y
j : J
⊢ f.left ≫ { pt := Y.left, π := Y.hom : Cone F }.π.app j = { pt := X.left, π := X.hom }.π.app j
have h : ({ pt := X.left, π := X.hom : Cone F }.pt ⟶ F.obj j) =
    (obj.{v₁, v₃, u₁, u₃} (obj (const J) X.left) j ⟶ (obj (fromPUnit F) Y.right).obj j) →
  { pt := X.left, π := X.hom : Cone F }.π.app j = (X.hom ≫ map (fromPUnit F) f.right).app j
Tactic: convert! congr_fun (congr_arg NatTrans.app f.w) j