-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
lemma iff_flat_and_rTensor_faithful :
    FaithfullyFlat R M ↔
    (Flat R M ∧
      ∀ (N : Type max u v) [AddCommGroup N] [Module R N],
        Nontrivial N → Nontrivial (N ⊗[R] M))

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this : Nontrivial ((R ⧸ m) ⊗[R] M)
⊢ False

Tactic:
have := (quotTensorEquivQuotSMul M m).toEquiv.symm.nontrivial

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this✝ : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial (M ⧸ m • ⊤)
⊢ False

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
faithful : ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
⊢ False

Tactic:
specialize faithful (ULift (R ⧸ m)) inferInstance

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
⊢ False

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this✝ : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial (M ⧸ m • ⊤)
⊢ False

Tactic:
haveI H : Subsingleton (M ⧸ m • (⊤ : Submodule R M)) := by
  rwa [Submodule.subsingleton_quotient_iff_eq_top]

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this✝ : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial (M ⧸ m • ⊤)
H : Subsingleton (M ⧸ m • ⊤)
⊢ False

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
⊢ False

Tactic:
haveI : Nontrivial ((R ⧸ m) ⊗[R] M) :=
  (congr (ULift.moduleEquiv : ULift (R ⧸ m) ≃ₗ[R] R ⧸ m)
    (LinearEquiv.refl R M)).symm.toEquiv.nontrivial

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this : Nontrivial ((R ⧸ m) ⊗[R] M)
⊢ False

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ FaithfullyFlat R M ↔
    Flat R M ∧
      ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)

Tactic:
refine ⟨fun fl => ⟨inferInstance, rTensor_nontrivial R M⟩, fun ⟨flat, faithful⟩ => ⟨?_⟩⟩

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
faithful : ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
⊢ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this✝ : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial (M ⧸ m • ⊤)
⊢ Subsingleton (M ⧸ m • ⊤)

Tactic:
rwa [Submodule.subsingleton_quotient_iff_eq_top]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this✝ : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial (M ⧸ m • ⊤)
H : Subsingleton (M ⧸ m • ⊤)
⊢ False

Tactic:
rw [← not_nontrivial_iff_subsingleton] at H

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this✝ : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial (M ⧸ m • ⊤)
H : ¬Nontrivial (M ⧸ m • ⊤)
⊢ False

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this✝ : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial (M ⧸ m • ⊤)
H : ¬Nontrivial (M ⧸ m • ⊤)
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
faithful : ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
⊢ ∀ ⦃m : Ideal R⦄, m.IsMaximal → m • ⊤ ≠ ⊤

Tactic:
intro m hm rid

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ :
  Flat R M ∧ ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
faithful : ∀ (N : Type (max u v)) [inst : AddCommGroup N] [inst_1 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
m : Ideal R
hm : m.IsMaximal
rid : m • ⊤ = ⊤
⊢ False