-- Mathlib/CategoryTheory/Limits/ConcreteCategory/WithAlgebraicStructures.lean
/--
if `r` has no zero smul divisors for all small-enough sections, then `r` has no zero smul divisors
in the colimit.
-/
lemma colimit_no_zero_smul_divisor
    (F : J ⥤ ModuleCat.{max t w} R) [PreservesColimit F (forget (ModuleCat R))]
    [IsFiltered J] [HasColimit F]
    (r : R) (H : ∃ (j' : J), ∀ (j : J) (_ : j' ⟶ j), ∀ (c : F.obj j), r • c = 0 → c = 0)
    (x : ToType (colimit F)) (hx : r • x = 0) : x = 0

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J), (j'' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ r • (ConcreteCategory.hom (F.map (IsFiltered.toSup {j, j', j''} {⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩} ⋯))) x = 0

Tactic:
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]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J), (j' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Tactic:
obtain ⟨j'', H⟩ := H

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J), (j'' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Proof state:
case intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J), (j' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Tactic:
obtain ⟨j', i, h⟩ := Concrete.colimit_rep_eq_zero (hx := hx)

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J), (j' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J), (j' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
x : ToType (colimit F)
hx : r • x = 0
⊢ x = 0

Tactic:
obtain ⟨j, x, rfl⟩ := Concrete.colimit_exists_rep F x

Result:
case intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J), (j' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : r • (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J), (j'' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j ∈ {j, j', j''}

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J), (j' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : r • (ConcreteCategory.hom (colimit.ι F j)) x = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Tactic:
rw [← map_smul (colimit.ι F j).hom] at hx

Result:
case intro.intro
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J), (j' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
⊢ (ConcreteCategory.hom (colimit.ι F j)) x = 0

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
H : ∃ j', ∀ (j : J), (j' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
x : ToType (colimit F)
hx : r • x = 0
⊢ x = 0

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])))

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J), (j'' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ j' ∈ {j, j', j''}

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
J : Type w
inst✝³ : Category.{r, w} J
F : J ⥤ ModuleCat R
inst✝² : PreservesColimit F (forget (ModuleCat R))
inst✝¹ : IsFiltered J
inst✝ : HasColimit F
r : R
j : J
x : ToType (F.obj j)
hx : (ModuleCat.Hom.hom (colimit.ι F j)) (r • x) = 0
j' : J
i : j ⟶ j'
h : (ModuleCat.Hom.hom (F.map i)) (r • x) = 0
j'' : J
H : ∀ (j : J), (j'' ⟶ j) → ∀ (c : ↑(F.obj j)), r • c = 0 → c = 0
⊢ ⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩ ∈ {⟨j, ⟨j', ⟨⋯, ⟨⋯, i⟩⟩⟩⟩}

Tactic:
simp

Result:
no goals