-- Module: Mathlib.RingTheory.Flat.Tensor
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
simp_rw :
  Baer.{u, v} R (CharacterModule M) ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
simp_rw₁ :
  (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : R) (mem : x ∈ I),
          Eq.{v + 1} (α := CharacterModule M) ((g' : (a : R) → CharacterModule M) x : CharacterModule M)
            ((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M)) ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)
simp_rw₂ :
  (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : R) (mem : x ∈ I),
          Eq.{v + 1} (α := CharacterModule M) ((g' : (a : R) → CharacterModule M) x : CharacterModule M)
            ((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M)) ↔
    ∀ (I : Ideal R),
      Surjective (α := LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)) (β :=
        LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M))
        (⇑(lcomp R (CharacterModule M) (Submodule.subtype I)) :
          (a : R →ₗ[R] CharacterModule M) → ↥I →ₗ[R] CharacterModule M)
simp_rw₃ :
  (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : R) (mem : x ∈ I),
          Eq.{v + 1} (α := CharacterModule M) ((g' : (a : R) → CharacterModule M) x : CharacterModule M)
            ((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M)) ↔
    ∀ (I : Ideal R) (b : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (a : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        (lcomp R (CharacterModule M) (Submodule.subtype I) :
              (a : R →ₗ[R] CharacterModule M) → ↥I →ₗ[R] CharacterModule M)
            a =
          b
simp_rw₄ :
  (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : R) (mem : x ∈ I) (x_1 : M),
          Eq (α := AddCircle (𝕜 := ℚ) 1)
            ((((g' : (a : R) → CharacterModule M) x : CharacterModule M) : (a : M) → AddCircle 1) x_1 :
              AddCircle (𝕜 := ℚ) 1)
            ((((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M) :
                  (a : M) → AddCircle 1)
                x_1 :
              AddCircle (𝕜 := ℚ) 1)) ↔
    ∀ (I : Ideal R) (b : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (a : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : ↥I) (x_1 : M),
          Eq (α := AddCircle (𝕜 := ℚ) 1)
            ((((((lcomp R (CharacterModule M) (Submodule.subtype I) :
                              (a : R →ₗ[R] CharacterModule M) → ↥I →ₗ[R] CharacterModule M)
                            a :
                          LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)) :
                        (a : ↥I) → CharacterModule M)
                      x :
                    CharacterModule M) :
                  (a : M) → AddCircle 1)
                x_1 :
              AddCircle (𝕜 := ℚ) 1)
            ((((b : (a : ↥I) → CharacterModule M) x : CharacterModule M) : (a : M) → AddCircle 1) x_1 :
              AddCircle (𝕜 := ℚ) 1)
simp_rw₅ :
  (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : R) (mem : x ∈ I) (x_1 : M),
          Eq (α := AddCircle (𝕜 := ℚ) 1)
            ((((g' : (a : R) → CharacterModule M) x : CharacterModule M) : (a : M) → AddCircle 1) x_1 :
              AddCircle (𝕜 := ℚ) 1)
            ((((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M) :
                  (a : M) → AddCircle 1)
                x_1 :
              AddCircle (𝕜 := ℚ) 1)) ↔
    ∀ (I : Ideal R) (b : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (a : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (a_1 : R) (b_1 : a_1 ∈ I) (x : M),
          Eq (α := AddCircle (𝕜 := ℚ) 1)
            ((((((lcomp R (CharacterModule M) (Submodule.subtype I) :
                              (a : R →ₗ[R] CharacterModule M) → ↥I →ₗ[R] CharacterModule M)
                            a :
                          LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)) :
                        (a : ↥I) → CharacterModule M)
                      (Subtype.mk (p := fun (a : R) ↦ a ∈ I) a_1 b_1) :
                    CharacterModule M) :
                  (a : M) → AddCircle 1)
                x :
              AddCircle (𝕜 := ℚ) 1)
            ((((b : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (a : R) ↦ a ∈ I) a_1 b_1) : CharacterModule M) :
                  (a : M) → AddCircle 1)
                x :
              AddCircle (𝕜 := ℚ) 1)
simp_rw₆ :
  (∀ (I : Ideal R) (g : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (g' : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (x : R) (mem : x ∈ I) (x_1 : M),
          Eq (α := AddCircle (𝕜 := ℚ) 1)
            ((((g' : (a : R) → CharacterModule M) x : CharacterModule M) : (a : M) → AddCircle 1) x_1 :
              AddCircle (𝕜 := ℚ) 1)
            ((((g : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : CharacterModule M) :
                  (a : M) → AddCircle 1)
                x_1 :
              AddCircle (𝕜 := ℚ) 1)) ↔
    ∀ (I : Ideal R) (b : LinearMap.{u, u, u, v} (RingHom.id R) (↥I) (CharacterModule M)),
      ∃ (a : LinearMap.{u, u, u, v} (RingHom.id R) R (CharacterModule M)),
        ∀ (a_1 : R) (b_1 : a_1 ∈ I) (x : M),
          Eq (α := AddCircle (𝕜 := ℚ) 1)
            ((((a : (a : R) → CharacterModule M)
                      ((Submodule.subtype I : (a : ↥I) → R) (Subtype.mk (p := fun (a : R) ↦ a ∈ I) a_1 b_1)) :
                    CharacterModule M) :
                  (a : M) → AddCircle 1)
                x :
              AddCircle (𝕜 := ℚ) 1)
            ((((b : (a : ↥I) → CharacterModule M) (Subtype.mk (p := fun (a : R) ↦ a ∈ I) a_1 b_1) : CharacterModule M) :
                  (a : M) → AddCircle 1)
                x :
              AddCircle (𝕜 := ℚ) 1)
⊢ Flat R M ↔
    ∀ (I : Ideal R),
      Function.Injective (α := TensorProduct R (↥I) M) (β := TensorProduct R R M)
        (⇑(rTensor M (Submodule.subtype I)) : (a : TensorProduct R (↥I) M) → TensorProduct R R M)

Tactic:
simp_rw [iff_characterModule_baer, Baer, rTensor_injective_iff_lcomp_surjective,
    Surjective, DFunLike.ext_iff, Subtype.forall, lcomp_apply, Submodule.subtype_apply]

Premises used: rTensor_injective_iff_lcomp_surjective, Submodule.subtype_apply, Subtype.forall, LinearMap.lcomp_apply, Module.Baer, DFunLike.ext_iff, Function.Surjective, Module.Flat.iff_characterModule_baer