-- Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst_2 : AddCommGroup M₁
inst_3 : AddCommGroup M₂
inst_4 : Module A M₁
inst_5 : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective.{u_5 + 1, u_6 + 1} (α := M₁) (β := M₂) (⇑φ : (a : M₁) → M₂)
rintro :
  ∀ (y : M₂) (hy : Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) y),
    ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
      (map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a =
        Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x) y hy
rintro₁ :
  ∀ (b : M₁)
    (hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂)),
    ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
      Eq.{u_6 + 1} (α := ↥(primaryComponent M₂ P.asIdeal))
        ((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a :
          ↥(primaryComponent M₂ P.asIdeal))
        (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
            ((φ : (a : M₁) → M₂) b) hy :
          ↥(primaryComponent M₂ P.asIdeal))
rintro₂ :
  ∀ (b : M₁)
    (hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂))
    (f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal))
    (hf :
      ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
                (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
                  (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
              fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
            (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
          f =
        b),
    ∃ (a : ↥(primaryComponent M₁ P.asIdeal)),
      Eq.{u_6 + 1} (α := ↥(primaryComponent M₂ P.asIdeal))
        ((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal)) a :
          ↥(primaryComponent M₂ P.asIdeal))
        (Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
            ((φ : (a : M₁) → M₂) b) hy :
          ↥(primaryComponent M₂ P.asIdeal))
rintro₃ :
  ∀ (b : M₁)
    (hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂))
    (f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal))
    (hf :
      ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
                (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
                  (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
              fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
            (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
          f =
        b),
    Eq.{u_6 + 1} (α := M₂)
      ((↑((map P.asIdeal φ : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal))
              ((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P)) :
          M₂) :
        M₂)
      ((↑(Subtype.mk (p := fun (x : M₂) ↦ Membership.mem (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) x)
              ((φ : (a : M₁) → M₂) b) hy) :
          M₂) :
        M₂)
rintro₄ :
  ∀ (b : M₁)
    (hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂))
    (f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal))
    (hf :
      ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
                (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
                  (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
              fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
            (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
          f =
        b),
    Eq.{u_6 + 1} (α := M₂)
      ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂)
      ((φ : (a : M₁) → M₂) b : M₂)
rintro₅ :
  ∀ (b : M₁)
    (hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂))
    (f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal))
    (hf :
      ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
                (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
                  (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
              fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
            (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
          f =
        b),
    HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
        ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂) =
      0
refine_1 :
  ∀ (b : M₁)
    (hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂))
    (f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal))
    (hf :
      ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
                (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
                  (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
              fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
            (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
          f =
        b),
    Membership.mem (γ := Submodule A M₂)
      ((fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) P)
      (HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
        ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))
refine_2 refine_2₁ :
  ∀ (b : M₁)
    (hy : Membership.mem (α := M₂) (γ := Submodule A M₂) (primaryComponent M₂ P.asIdeal) ((φ : (a : M₁) → M₂) b : M₂))
    (f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal))
    (hf :
      ((DFinsupp.lsum ℕ (M := fun (i : HeightOneSpectrum A) ↦ ↥(primaryComponent M₁ i.asIdeal)) :
                (a : (i : HeightOneSpectrum A) → ↥(primaryComponent M₁ i.asIdeal) →ₗ[A] M₁) →
                  (Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) →ₗ[A] M₁)
              fun (i : HeightOneSpectrum A) ↦ Submodule.subtype (primaryComponent M₁ i.asIdeal) :
            (a : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)) → M₁)
          f =
        b),
    Membership.mem (γ := Submodule A M₂)
      (⨆ (j : HeightOneSpectrum A),
        ⨆ (_ : j ≠ P), (fun (P : HeightOneSpectrum A) ↦ (primaryComponent M₂ P.asIdeal : Submodule A M₂)) j)
      (HSub.hSub (α := M₂) (β := M₂) ((φ : (a : M₁) → M₂) b : M₂)
        ((φ : (a : M₁) → M₂) (↑((f : (a : HeightOneSpectrum A) → ↥(primaryComponent M₁ a.asIdeal)) P) : M₁) : M₂))
⊢ Surjective.{u_5 + 1, u_6 + 1} (α := ↥(primaryComponent M₁ P.asIdeal)) (β := ↥(primaryComponent M₂ P.asIdeal))
    (⇑(map P.asIdeal φ) : (a : ↥(primaryComponent M₁ P.asIdeal)) → ↥(primaryComponent M₂ P.asIdeal))

Tactic:
classical
  rintro ⟨y, hy⟩
  obtain ⟨b, rfl⟩ : ∃ a, φ a = y := hf y
  obtain ⟨f, hf⟩ : ∃ f : Π₀ i : HeightOneSpectrum A, primaryComponent M₁ i.asIdeal,
      (DFinsupp.lsum ℕ fun i : HeightOneSpectrum A ↦
      (primaryComponent M₁ i.asIdeal).subtype) f = b := by
    simp only [← mem_iSup_iff_exists_dfinsupp, iSup_primaryComponent_eq_top hM₁, mem_top]
  refine ⟨f P, Subtype.ext ?_⟩
  simp only [map_apply_coe]
  rw [eq_comm, ← sub_eq_zero]
  refine (Submodule.disjoint_def.mp (iSupIndep_primaryComponent A M₂ P)) _ ?_ ?_
  · exact Submodule.sub_mem _ hy (primaryComponent_map_mem _ _ _)
  · have hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q) := by
      rw [sub_eq_iff_eq_add', ← Finset.sum_eq_add_sum_diff_singleton P (fun P ↦ φ (f P)) (by aesop)]
      simpa [DFinsupp.sumAddHom_apply, DFinsupp.sum] using congr(φ $hf).symm
    rw [hdiff]
    exact Submodule.sum_mem _ fun Q hQ ↦ Submodule.mem_iSup_of_mem Q <|
        Submodule.mem_iSup_of_mem (by grind) (primaryComponent_map_mem _ _ _)

Premises used: sub_eq_zero, IsDedekindDomain.HeightOneSpectrum, Submodule.sum_mem, eq_comm, Ideal.iSupIndep_primaryComponent, Iff.mp, Submodule.mem_iSup_of_mem, Submodule.disjoint_def, Ideal.primaryComponent.map_apply_coe, rfl