-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder (goal)
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_2
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst_3 : Finite ι
this :
  Eq (α := Submodule R M)
    (ker (M₂ := ((i : ι) → R ⧸ I i) ⊗[R] M)
      (rTensor M (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)) ∘ₗ
        (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)))
    (range (M :=
      ↥(ker (M₂ := (i : ι) → R ⧸ I i)
            (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
        M)
      ((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
        rTensor M
          (Submodule.subtype
            (ker (M₂ := (i : ι) → R ⧸ I i)
              (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))))
x :
  ↥(ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R] M
h :
  ∀ (r : ↥(ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))))
    (m : M),
    Membership.mem (α := R) (γ := Submodule R R) (⨅ (i : ι), I i)
      (((Submodule.subtype
                  (ker (M₂ := (i : ι) → R ⧸ I i)
                    (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) :
                (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker) → R)
              (r, m).1,
            (LinearMap.id : (a : M) → M) (r, m).2).1 :
        R)
⊢ Membership.mem (α := M) (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤)
    (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
            rTensor M
              (Submodule.subtype
                (ker (M₂ := (i : ι) → R ⧸ I i)
                  (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))) :
          (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → M)
        x :
      M)
have h₁ : ∀
  (x x_1 :
    ↥(ker (M₂ := (i : ι) → R ⧸ I i) (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i))) ⊗[R]
      M),
  Membership.mem (α := M) (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤)
      (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
              rTensor M
                (Submodule.subtype
                  (ker (M₂ := (i : ι) → R ⧸ I i)
                    (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))) :
            (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → M)
          x :
        M) →
    Membership.mem (α := M) (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤)
        (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
                rTensor M
                  (Submodule.subtype
                    (ker (M₂ := (i : ι) → R ⧸ I i)
                      (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))) :
              (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → M)
            x_1 :
          M) →
      Membership.mem (α := M) (HSMul.hSMul.{u_1, u_3, u_3} (α := Ideal R) (β := Submodule R M) (⨅ (i : ι), I i) ⊤)
        (((↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ
                rTensor M
                  (Submodule.subtype
                    (ker (M₂ := (i : ι) → R ⧸ I i)
                      (LinearMap.pi (φ := fun (i : ι) ↦ R ⧸ I i) fun (i : ι) ↦ Submodule.mkQ (I i)))) :
              (a : ↥(LinearMap.pi fun (i : ι) ↦ Submodule.mkQ (I i)).ker ⊗[R] M) → M)
            (x + x_1) :
          M)
Tactic: refine x.induction_on (by simp) (fun r m ↦ Submodule.smul_mem_smul ?_ ⟨⟩) fun _ _ ↦ ?_