-- 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)
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)
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))
        (⇑((lmap (M := fun (x : ι) ↦ TensorProduct.{u, u, w} R (↥N) (M x)) (N := fun (x : ι) ↦
                    TensorProduct.{u, u, w} R P (M x)) fun (x : ι) ↦ rTensor (M x) N.subtype :
                  (⨁ (i : ι), TensorProduct.{u, u, w} R (↥N) (M i)) →ₗ[R]
                    ⨁ (i : ι), TensorProduct.{u, u, w} R P (M i)) ∘ₗ
                ((↑(directSumRight R R (↥N) M) :
                    (↥N ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R (↥N) (M i)) :
                  (↥N ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R (↥N) (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)
⊢ 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))
      (Function.comp (β := ⨁ (i : ι), TensorProduct.{u, u, w} R (↥N) (M i))
        (⇑(lmap (M := fun (x : ι) ↦ TensorProduct.{u, u, w} R (↥N) (M x)) (N := fun (x : ι) ↦
              TensorProduct.{u, u, w} R P (M x)) fun (x : ι) ↦ rTensor (M x) N.subtype) :
          (a : ⨁ (i : ι), ↥N ⊗[R] M i) → ⨁ (i : ι), P ⊗[R] M i)
        (⇑((↑(directSumRight R R (↥N) M) :
                (↥N ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R (↥N) (M i)) :
              (↥N ⊗[R] ⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), TensorProduct.{u, u, w} R (↥N) (M i)) :
          (a : ↥N ⊗[R] ⨁ (i : ι), M i) → ⨁ (i : ι), ↥N ⊗[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)