awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : Ideal R
h : m.IsMaximal
r : HSMul.hSMul (β := Submodule R R) m ⊤ = ⊤
⊢ 1 ∈ m

Tactic:
simpa using show 1 ∈ (m • ⊤ : Ideal R) from r.symm ▸ ⟨⟩

Premises used: Eq.rec, Eq.symm, True.intro
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw :
  (Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤) ↔
    Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
⊢ FaithfullyFlat R M ↔ Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤

Tactic:
rw [faithfullyFlat_iff]

Premises used: Module.faithfullyFlat_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ (Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤) ↔
    Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤

Tactic:
⟨fun ⟨flat, h⟩ => ⟨flat, fun I hI r => ?_⟩, fun h => ⟨h.1, fun m hm => h.2 _ hm.ne_top⟩⟩

Premises used: _private.0.Module.FaithfullyFlat.iff_flat_and_proper_ideal.match_1, Module.Flat, And, And.right, And.left, And.intro, Iff.intro, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
refine :
  (Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤) →
    ∀ (flat : Flat R M) (h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤) (I : Ideal R)
      (hI : I ≠ ⊤) (r : HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤), False
⊢ (Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤) ↔
    Flat R M ∧ ∀ (I : Ideal R), I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤

Tactic:
refine ⟨fun ⟨flat, h⟩ => ⟨flat, fun I hI r => ?_⟩, fun h => ⟨h.1, fun m hm => h.2 _ hm.ne_top⟩⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤
flat : Flat R M
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤
I : Ideal R
hI : I ≠ ⊤
r : HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤
obtain : ∀ (m : Ideal R) (hm : m.IsMaximal) (le : I ≤ m), False
⊢ False

Tactic:
obtain ⟨m, hm, le⟩ := I.exists_le_maximal hI

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤
flat : Flat R M
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤
I : Ideal R
hI : I ≠ ⊤
r : HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤
m : Ideal R
hm : m.IsMaximal
le : I ≤ m
⊢ ⊤ ≤ HSMul.hSMul (β := Submodule R M) I ⊤

Tactic:
simp [r]
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h_1 : Flat R M ∧ ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤
flat : Flat R M
h : ∀ ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤
I : Ideal R
hI : I ≠ ⊤
r : HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤
m : Ideal R
hm : m.IsMaximal
le : I ≤ m
⊢ False

Tactic:
exact h hm <| eq_top_iff.2 <| show ⊤ ≤ m • ⊤ from r ▸ Submodule.smul_mono le (by simp [r])

Premises used: Iff.mpr, eq_top_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : Flat R M
I : Ideal R
mp : (I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤) → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
mpr : (HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤) → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
mp₁ : ¬I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
mp₂ : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
mp₃ : ¬I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
mp₄ : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
mp₅ : ¬I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
mp₆ : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
mpr₁ : ¬HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
mpr₂ : I = ⊤ → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
mpr₃ : ¬HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
mpr₄ : I = ⊤ → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
mpr₅ : ¬HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
mpr₆ : I = ⊤ → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
mp₇ mp₈ mp₉ : I = ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
mp₁₀ : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
mpr₇ : I = ⊤ → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → False
⊢ I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ ↔ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤

Tactic:
tauto
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
obtain : ∀ (n : N) (hn : n ≠ 0), Nontrivial (N ⊗[R] M)
⊢ Nontrivial (N ⊗[R] M)

Tactic:
obtain ⟨n, hn⟩ := nontrivial_iff_exists_ne (0 : N) |>.1 inferInstance

Premises used: inferInstance, nontrivial_iff_exists_ne, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
pos : ∀ (I_ne_top : I = ⊤), Nontrivial (N ⊗[R] M)
neg : ∀ (I_ne_top : ¬I = ⊤), Nontrivial (N ⊗[R] M)
⊢ Nontrivial (N ⊗[R] M)

Tactic:
by_cases I_ne_top : I = ⊤
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : I = ⊤
⊢ n = 0

Tactic:
rw [Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton, one_smul] at I_ne_top

Premises used: one_smul, Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : n = 0
⊢ Nontrivial (N ⊗[R] M)

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
r : R
hr : r ∈ I
⊢ Membership.mem (γ := Submodule R R)
    (LinearMap.ker.{u, u, u, u_1} (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R)
      ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n))
    r

Tactic:
simpa only [LinearMap.mem_ker, LinearMap.flip_apply, LinearMap.lsmul_apply,
      Submodule.mem_annihilator_span_singleton, I] using hr

Premises used: LinearMap.flip_apply, LinearMap.mem_ker, LinearMap.lsmul_apply, Submodule.mem_annihilator_span_singleton
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n) ⋯
r : R
hr : Quotient.mk'' r ∈ inc.ker
⊢ Membership.mem (γ := Submodule R (R ⧸ I)) ⊥ (Quotient.mk'' r)

Tactic:
simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.mem_bot, Submodule.Quotient.mk_eq_zero,
      Submodule.mem_annihilator_span_singleton, LinearMap.mem_ker, Submodule.liftQ_apply,
      LinearMap.flip_apply, LinearMap.lsmul_apply, I, inc] using hr

Premises used: Submodule.mem_bot, LinearMap.flip_apply, LinearMap.mem_ker, LinearMap.lsmul_apply, Submodule.liftQ_apply, Submodule.mem_annihilator_span_singleton, Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n) ⋯
r : R ⧸ I
hr : r ∈ inc.ker
h : ∀ (r : R) (hr : Quotient.mk'' r ∈ inc.ker), Membership.mem (γ := Submodule R (R ⧸ I)) ⊥ (Quotient.mk'' r)
⊢ Membership.mem (γ := Submodule R (R ⧸ I)) ⊥ r

Tactic:
induction r using Quotient.inductionOn' with | h r =>
    simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.mem_bot, Submodule.Quotient.mk_eq_zero,
      Submodule.mem_annihilator_span_singleton, LinearMap.mem_ker, Submodule.liftQ_apply,
      LinearMap.flip_apply, LinearMap.lsmul_apply, I, inc] using hr

Premises used: Submodule.mem_bot, LinearMap.flip_apply, LinearMap.mem_ker, LinearMap.lsmul_apply, Submodule.liftQ_apply, Submodule.mem_annihilator_span_singleton, Submodule.Quotient.mk''_eq_mk, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n) ⋯
⊢ Function.Injective.{u + 1, u_1 + 1} (α := R ⧸ I) (β := N) (⇑inc : (a : R ⧸ I) → N)

Tactic:
have injective_inc : Function.Injective inc := LinearMap.ker_eq_bot.1 <| eq_bot_iff.2 <| by
    intro r hr
    induction r using Quotient.inductionOn' with | h r =>
    simpa only [Submodule.Quotient.mk''_eq_mk, Submodule.mem_bot, Submodule.Quotient.mk_eq_zero,
      Submodule.mem_annihilator_span_singleton, LinearMap.mem_ker, Submodule.liftQ_apply,
      LinearMap.flip_apply, LinearMap.lsmul_apply, I, inc] using hr
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n) ⋯
injective_inc : Function.Injective.{u + 1, u_1 + 1} (α := R ⧸ I) (β := N) (⇑inc : (a : R ⧸ I) → N)
⊢ HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤

Tactic:
have ne_top := iff_flat_and_proper_ideal R M |>.1 fl |>.2 I I_ne_top
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n) ⋯
injective_inc : Function.Injective.{u + 1, u_1 + 1} (α := R ⧸ I) (β := N) (⇑inc : (a : R ⧸ I) → N)
ne_top : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
⊢ Nontrivial (N ⊗[R] M)

Tactic:
subsingleton_or_nontrivial _ |>.resolve_left fun rid => ne_top ?_

Premises used: subsingleton_or_nontrivial, Or.resolve_left
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n) ⋯
injective_inc : Function.Injective.{u + 1, u_1 + 1} (α := R ⧸ I) (β := N) (⇑inc : (a : R ⧸ I) → N)
ne_top : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
neg : ∀ (rid : Subsingleton (N ⊗[R] M)), HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤
⊢ Nontrivial (N ⊗[R] M)

Tactic:
refine subsingleton_or_nontrivial _ |>.resolve_left fun rid => ne_top ?_

Premises used: subsingleton_or_nontrivial, Or.resolve_left
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n) ⋯
injective_inc : Function.Injective.{u + 1, u_1 + 1} (α := R ⧸ I) (β := N) (⇑inc : (a : R ⧸ I) → N)
ne_top : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
rid : Subsingleton (N ⊗[R] M)
neg : Subsingleton.{v + 1} (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
⊢ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤

Tactic:
rw [← Submodule.Quotient.subsingleton_iff]

Premises used: Submodule.Quotient.subsingleton_iff
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n) ⋯
injective_inc : Function.Injective.{u + 1, u_1 + 1} (α := R ⧸ I) (β := N) (⇑inc : (a : R ⧸ I) → N)
ne_top : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
rid : Subsingleton (N ⊗[R] M)
⊢ Subsingleton.{v + 1} (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)

Tactic:
(fl.toFlat.rTensor_preserves_injective_linearMap inc injective_inc).comp
    (quotTensorEquivQuotSMul M I).symm.injective |>.subsingleton

Premises used: LinearEquiv.symm, TensorProduct.quotTensorEquivQuotSMul, Function.Injective.subsingleton, Function.Injective.comp, LinearEquiv.injective, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
fl : FaithfullyFlat R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Nontrivial N
n : N
hn : n ≠ 0
I : Ideal R := Submodule.annihilator (M := N) (R ∙ n)
I_ne_top : ¬I = ⊤
inc : R ⧸ I →ₗ[R] N := Submodule.liftQ I ((LinearMap.flip (LinearMap.lsmul R N) : (a : N) → R →ₗ[R] N) n) ⋯
injective_inc : Function.Injective.{u + 1, u_1 + 1} (α := R ⧸ I) (β := N) (⇑inc : (a : R ⧸ I) → N)
ne_top : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
rid : Subsingleton (N ⊗[R] M)
⊢ Subsingleton.{v + 1} (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)

Tactic:
exact (fl.toFlat.rTensor_preserves_injective_linearMap inc injective_inc).comp
    (quotTensorEquivQuotSMul M I).symm.injective |>.subsingleton

Premises used: LinearEquiv.symm, TensorProduct.quotTensorEquivQuotSMul, Function.Injective.subsingleton, Function.Injective.comp, LinearEquiv.injective, Module.Flat.rTensor_preserves_injective_linearMap
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FaithfullyFlat R M
N : Type u_1
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : Nontrivial N
⊢ Nontrivial (M ⊗[R] N)

Tactic:
TensorProduct.comm R M N |>.toEquiv.nontrivial

Premises used: TensorProduct.comm, Equiv.nontrivial, LinearEquiv.toEquiv
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FaithfullyFlat R M
N : Type u_1
inst_4 : AddCommGroup N
inst_5 : Module R N
h : Subsingleton (N ⊗[R] M)
revert : ∀ [h : Subsingleton (N ⊗[R] M)], Subsingleton N
⊢ Subsingleton N

Tactic:
revert h
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FaithfullyFlat R M
N : Type u_1
inst_4 : AddCommGroup N
inst_5 : Module R N
contrapose! : Nontrivial N → Nontrivial (N ⊗[R] M)
⊢ Subsingleton (N ⊗[R] M) → Subsingleton N

Tactic:
contrapose!
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FaithfullyFlat R M
N : Type u_1
inst_4 : AddCommGroup N
inst_5 : Module R N
h : Nontrivial N
⊢ Nontrivial (N ⊗[R] M)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FaithfullyFlat R M
N : Type u_1
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : Subsingleton (M ⊗[R] N)
⊢ Subsingleton (N ⊗[R] M)

Tactic:
haveI : Subsingleton (N ⊗[R] M) := (TensorProduct.comm R N M).toEquiv.injective.subsingleton
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FaithfullyFlat R M
N : Type u_1
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : Subsingleton (M ⊗[R] N)
this : Subsingleton (N ⊗[R] M)
⊢ Subsingleton N

Tactic:
apply rTensor_reflects_triviality R M

Premises used: Module.FaithfullyFlat.rTensor_reflects_triviality
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ FaithfullyFlat R M ↔
    Flat R M ∧
      ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)

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

Premises used: Module.FaithfullyFlat.mk, inferInstance, Module.FaithfullyFlat.rTensor_nontrivial, And.intro, Iff.intro, Module.FaithfullyFlat, _private.0.Module.FaithfullyFlat.iff_flat_and_rTensor_faithful.match_1
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
refine :
  (Flat R M ∧
      ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)) →
    ∀ (flat : Flat R M)
      (faithful :
        ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M))
      ⦃m : Ideal R⦄, m.IsMaximal → HSMul.hSMul (β := Submodule R M) m ⊤ ≠ ⊤
⊢ FaithfullyFlat R M ↔
    Flat R M ∧
      ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)

Tactic:
refine ⟨fun fl => ⟨inferInstance, rTensor_nontrivial R M⟩, fun ⟨flat, faithful⟩ => ⟨?_⟩⟩
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
faithful : ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
m : Ideal R
hm : m.IsMaximal
rid : HSMul.hSMul (β := Submodule R M) m ⊤ = ⊤
⊢ Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)

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

Premises used: ULift, inferInstance, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : HSMul.hSMul (β := Submodule R M) m ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
⊢ Nontrivial ((R ⧸ m) ⊗[R] M)

Tactic:
haveI : Nontrivial ((R ⧸ m) ⊗[R] M) :=
    (congr (ULift.moduleEquiv : ULift (R ⧸ m) ≃ₗ[R] R ⧸ m)
      (LinearEquiv.refl R M)).symm.toEquiv.nontrivial
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : HSMul.hSMul (β := Submodule R M) m ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this : Nontrivial ((R ⧸ m) ⊗[R] M)
⊢ Nontrivial.{v} (M ⧸ HSMul.hSMul (β := Submodule R M) m ⊤)

Tactic:
have := (quotTensorEquivQuotSMul M m).toEquiv.symm.nontrivial
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : HSMul.hSMul (β := Submodule R M) m ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this_1 : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial.{v} (M ⧸ HSMul.hSMul (β := Submodule R M) m ⊤)
⊢ False

Tactic:
not_subsingleton (M ⧸ m • (⊤ : Submodule R M)) ?_

Premises used: HasQuotient.Quotient, not_subsingleton, HSMul.hSMul, Top.top
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : HSMul.hSMul (β := Submodule R M) m ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this_1 : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial.{v} (M ⧸ HSMul.hSMul (β := Submodule R M) m ⊤)
refine : Subsingleton.{v + 1} (M ⧸ HSMul.hSMul (β := Submodule R M) m ⊤)
⊢ False

Tactic:
refine not_subsingleton (M ⧸ m • (⊤ : Submodule R M)) ?_

Premises used: HasQuotient.Quotient, not_subsingleton, HSMul.hSMul, Top.top
-- Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  Flat R M ∧
    ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N], Nontrivial N → Nontrivial (N ⊗[R] M)
flat : Flat R M
m : Ideal R
hm : m.IsMaximal
rid : HSMul.hSMul (β := Submodule R M) m ⊤ = ⊤
faithful : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
this_1 : Nontrivial ((R ⧸ m) ⊗[R] M)
this : Nontrivial.{v} (M ⧸ HSMul.hSMul (β := Submodule R M) m ⊤)
rwa rwa₁ rwa₂ rwa₃ : HSMul.hSMul (β := Submodule R M) m ⊤ = ⊤
⊢ Subsingleton.{v + 1} (M ⧸ HSMul.hSMul (β := Submodule R M) m ⊤)

Tactic:
rwa [Submodule.Quotient.subsingleton_iff]

Premises used: Submodule.Quotient.subsingleton_iff