-- Lean 4 proof step from Mathlib.RingTheory.Flat.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
simp_rw :
  (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := ↥N ⊗[R] ⨁ (i : ι), M i) (β := P ⊗[R] ⨁ (i : ι), M i)
        (⇑(rTensor (⨁ (i : ι), M i) N.subtype) : (a : ↥N ⊗[R] ⨁ (i : ι), M i) → P ⊗[R] ⨁ (i : ι), M i)) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)
simp_rw₁ :
  (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := ↥N ⊗[R] ⨁ (i : ι), M i) (β := ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i))
        (Function.comp (β := P ⊗[R] ⨁ (i : ι), M i)
          (⇑(directSumRight R R P M : (P ⊗[R] ⨁ (i : ι), M i) ≃ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) :
            (a : P ⊗[R] ⨁ (i : ι), M i) → ⨁ (i : ι), P ⊗[R] M i)
          (⇑(rTensor (⨁ (i : ι), M i) N.subtype) : (a : ↥N ⊗[R] ⨁ (i : ι), M i) → P ⊗[R] ⨁ (i : ι), M i))) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)
simp_rw₂ :
  (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := ↥N ⊗[R] ⨁ (i : ι), M i) (β := ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i))
        (Function.comp (β := P ⊗[R] ⨁ (i : ι), M i)
          (⇑((↑(directSumRight R R P M) : (P ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) :
                (P ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) :
            (a : P ⊗[R] ⨁ (i : ι), M i) → ⨁ (i : ι), P ⊗[R] M i)
          (⇑(rTensor (⨁ (i : ι), M i) N.subtype) : (a : ↥N ⊗[R] ⨁ (i : ι), M i) → P ⊗[R] ⨁ (i : ι), M i))) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
        (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat.{u, w} R (M i)
have simp_rw₃ : (∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
    Injective (α := ↥N ⊗[R] ⨁ (i : ι), M i) (β := ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i))
      (⇑(((↑(directSumRight R R P M) : (P ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) :
                (P ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) ∘ₗ
              (rTensor (⨁ (i : ι), M i) N.subtype : (↥N ⊗[R] ⨁ (i : ι), M i) →ₗ[R] P ⊗[R] ⨁ (i : ι), M i) :
            (↥N ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) :
        (a : ↥N ⊗[R] ⨁ (i : ι), M i) → ⨁ (i : ι), P ⊗[R] M i)) ↔
  ∀ (i : ι) ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
    Injective (α := TensorProduct.{u, u, w} R (↥N) (M i)) (β := TensorProduct.{u, u, w} R P (M i))
      (⇑(rTensor (M i) N.subtype) : (a : ↥N ⊗[R] M i) → P ⊗[R] M i)
Tactic: classical
  simp_rw [iff_rTensor_injectiveₛ, ← EquivLike.comp_injective _ (directSumRight R R _ _),
    ← LinearEquiv.coe_coe, ← coe_comp, directSumRight_comp_rTensor, coe_comp, LinearEquiv.coe_coe,
    EquivLike.injective_comp, lmap_injective]
  constructor <;> (intro h; intros; apply h)