awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 ⊤ ≠ ⊤
have 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
Tactic: refine ⟨fun ⟨flat, h⟩ => ⟨flat, fun I hI r => ?_⟩, fun h => ⟨h.1, fun m hm => h.2 _ hm.ne_top⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 ⊤ = ⊤
⊢ False
have obtain : ∀ (m : Ideal R) (hm : m.IsMaximal) (le : I ≤ m), False
Tactic: obtain ⟨m, hm, le⟩ := I.exists_le_maximal hI
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
⊢ I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ ↔ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
have mp : (I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤) → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 = ⊤
⊢ I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ ↔ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
have mpr : (HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤) → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 ⊤ ≠ ⊤
⊢ I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ ↔ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
have mp₁ : ¬I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 = ⊤
⊢ I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ ↔ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
have mp₂ : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 = ⊤
⊢ I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ ↔ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
have mpr₁ : ¬HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 ⊤ ≠ ⊤
⊢ I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ ↔ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
have mpr₂ : I = ⊤ → I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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 ⊤ ≠ ⊤
⊢ I ≠ ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤ ↔ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
have mp₇ : I = ⊤ → HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤ → I = ⊤
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
⊢ Nontrivial (N ⊗[R] M)
have obtain : ∀ (n : N) (hn : n ≠ 0), Nontrivial (N ⊗[R] M)
Tactic: obtain ⟨n, hn⟩ := nontrivial_iff_exists_ne (0 : N) |>.1 inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ Nontrivial (N ⊗[R] M)
have pos : ∀ (I_ne_top : I = ⊤), Nontrivial (N ⊗[R] M)
Tactic: by_cases I_ne_top : I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ Nontrivial (N ⊗[R] M)
have neg : ∀ (I_ne_top : ¬I = ⊤), Nontrivial (N ⊗[R] M)
Tactic: by_cases I_ne_top : I = ⊤
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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 = ⊤
⊢ Nontrivial (N ⊗[R] M)
have I_ne_top₁ : n = 0
Tactic: rw [Ideal.eq_top_iff_one, Submodule.mem_annihilator_span_singleton, one_smul] at I_ne_top
Cleared hypotheses: I_ne_top
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R (R ⧸ I)) ⊥ r
have h : ∀ (r : R) (hr : Quotient.mk'' r ∈ inc.ker), Membership.mem (γ := Submodule R (R ⧸ I)) ⊥ (Quotient.mk'' 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
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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) ⋯
⊢ Nontrivial (N ⊗[R] M)
have injective_inc : 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
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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)
⊢ Nontrivial (N ⊗[R] M)
have ne_top : HSMul.hSMul (β := Submodule R M) I ⊤ ≠ ⊤
Tactic: have ne_top := iff_flat_and_proper_ideal R M |>.1 fl |>.2 I I_ne_top
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
have neg : ∀ (rid : Subsingleton (N ⊗[R] M)), HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤
Tactic: refine subsingleton_or_nontrivial _ |>.resolve_left fun rid => ne_top ?_
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ HSMul.hSMul (β := Submodule R M) I ⊤ = ⊤
have neg : Subsingleton.{v + 1} (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Tactic: rw [← Submodule.Quotient.subsingleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
⊢ Subsingleton N
have revert : ∀ [h : Subsingleton (N ⊗[R] M)], Subsingleton N
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
⊢ Subsingleton (N ⊗[R] M) → Subsingleton N
have contrapose! : Nontrivial N → Nontrivial (N ⊗[R] M)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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
have this : Subsingleton (N ⊗[R] M)
Tactic: haveI : Subsingleton (N ⊗[R] M) := (TensorProduct.comm R N M).toEquiv.injective.subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
have 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 ⊤ ≠ ⊤
Tactic: refine ⟨fun fl => ⟨inferInstance, rTensor_nontrivial R M⟩, fun ⟨flat, faithful⟩ => ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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 ⊤ = ⊤
⊢ False
have faithful₁ : Nontrivial (ULift.{v, u} (R ⧸ m) ⊗[R] M)
Tactic: specialize faithful (ULift (R ⧸ m)) inferInstance
Cleared hypotheses: faithful
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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)
⊢ False
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (hypothesis)
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)
⊢ False
have this₁ : Nontrivial.{v} (M ⧸ HSMul.hSMul (β := Submodule R M) m ⊤)
Tactic: have := (quotTensorEquivQuotSMul M m).toEquiv.symm.nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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
have refine : Subsingleton.{v + 1} (M ⧸ HSMul.hSMul (β := Submodule R M) m ⊤)
Tactic: refine not_subsingleton (M ⧸ m • (⊤ : Submodule R M)) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
x : AddCommGroup N
x_1 : Module R N
⊢ Nontrivial N → Nontrivial (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
have simp : ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
Tactic: simp only [← not_subsingleton_iff_nontrivial]
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
x : AddCommGroup N
x_1 : Module R N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
have mp : (¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)) → Subsingleton (N ⊗[R] M) → Subsingleton N
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
x : AddCommGroup N
x_1 : Module R N
mp : (¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)) → Subsingleton (N ⊗[R] M) → Subsingleton N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
have mpr : (Subsingleton (N ⊗[R] M) → Subsingleton N) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
x : AddCommGroup N
x_1 : Module R N
mp : (¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)) → Subsingleton (N ⊗[R] M) → Subsingleton N
mpr : (Subsingleton (N ⊗[R] M) → Subsingleton N) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
have mp₁ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
x : AddCommGroup N
x_1 : Module R N
mp : (¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)) → Subsingleton (N ⊗[R] M) → Subsingleton N
mpr : (Subsingleton (N ⊗[R] M) → Subsingleton N) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mp₁ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
have mp₂ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
x : AddCommGroup N
x_1 : Module R N
mp : (¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)) → Subsingleton (N ⊗[R] M) → Subsingleton N
mpr : (Subsingleton (N ⊗[R] M) → Subsingleton N) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mp₁ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₂ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₃ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₄ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₅ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₆ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
have mpr₁ : ¬Subsingleton (N ⊗[R] M) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
Tactic: tauto
-- Lean 4 proof step from Mathlib.RingTheory.Flat.FaithfullyFlat.Basic (goal)
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)
x : AddCommGroup N
x_1 : Module R N
mp : (¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)) → Subsingleton (N ⊗[R] M) → Subsingleton N
mpr : (Subsingleton (N ⊗[R] M) → Subsingleton N) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
mp₁ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₂ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₃ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₄ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₅ : ¬¬Subsingleton N → Subsingleton (N ⊗[R] M) → Subsingleton N
mp₆ : ¬Subsingleton (N ⊗[R] M) → Subsingleton (N ⊗[R] M) → Subsingleton N
mpr₁ : ¬Subsingleton (N ⊗[R] M) → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
⊢ ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M) ↔ Subsingleton (N ⊗[R] M) → Subsingleton N
have mpr₂ : Subsingleton N → ¬Subsingleton N → ¬Subsingleton (N ⊗[R] M)
Tactic: tauto