-- Mathlib/RingTheory/Flat/Basic.lean
theorem directSum_iff : Flat R (⨁ i, M i) ↔ ∀ i, Flat R (M i)

Proof state:
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat R (M i)

Tactic:
simp_rw [iff_rTensor_injectiveₛ, ← EquivLike.comp_injective _ (directSumRight R _ _),
  ← LinearEquiv.coe_coe, ← coe_comp, directSumRight_comp_rTensor, coe_comp, LinearEquiv.coe_coe,
  EquivLike.injective_comp, lmap_injective]

Result:
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Function.Injective ⇑(rTensor (M i) N.subtype)) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Function.Injective ⇑(rTensor (M i) N.subtype)

Proof state:
case mpr
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor (M i) N.subtype)
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
i✝ : ι
⊢ Function.Injective ⇑(rTensor (M i✝) N✝.subtype)

Tactic:
apply h

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Function.Injective ⇑(rTensor (M i) N.subtype)) ↔
    ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Function.Injective ⇑(rTensor (M i) N.subtype)

Tactic:
constructor <;> (intro h; intros; apply h)

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Function.Injective ⇑(rTensor (M i) N.subtype)

Tactic:
intros

Result:
case mpr
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor (M i) N.subtype)
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
i✝ : ι
⊢ Function.Injective ⇑(rTensor (M i✝) N✝.subtype)

Proof state:
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat R (M i)

Tactic:
classical
simp_rw [iff_rTensor_injectiveₛ, ← EquivLike.comp_injective _ (directSumRight 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)

Result:
no goals

Proof state:
case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ (∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
      Function.Injective ⇑(rTensor (M i) N.subtype)) →
    ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
      Function.Injective ⇑(rTensor (M i) N.subtype)

Tactic:
intro h

Result:
case mpr
R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Function.Injective ⇑(rTensor (M i) N.subtype)
⊢ ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Function.Injective ⇑(rTensor (M i) N.subtype)