-- Lean 4 proof step from Mathlib.Algebra.Module.Torsion.PrimaryComponent (goal)
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))
⊢ 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))
have 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))
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 _ _ _)