awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ m ∈ N
have suffices : I = ⊤
Tactic: suffices I = ⊤ by simpa [I] using I.eq_top_iff_one.mp this
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ I = ⊤
have refine : (∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M) → ∀ (P : Ideal R) (hP : P.IsMaximal) (le : I ≤ P), False
Tactic: refine Not.imp_symm I.exists_le_maximal fun ⟨P, hP, le⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
⊢ False
have obtain : ∀ (a : M) (ha : a ∈ N) (s : ↥P.primeCompl)
  (e : Eq (α := Mₚ P) (IsLocalizedModule.mk' (f P) a s) ((f P : (a : M) → Mₚ P) m)), False
Tactic: obtain ⟨a, ha, s, e⟩ := h P
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s : ↥P.primeCompl
e : Eq (α := Mₚ P) (IsLocalizedModule.mk' (f P) a s) ((f P : (a : M) → Mₚ P) m)
⊢ False
have e₁ : ∃ (s_1 : ↥P.primeCompl), s_1 • s • m = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥P.primeCompl) 1 a
Tactic: rw [← IsLocalizedModule.mk'_one P.primeCompl, IsLocalizedModule.mk'_eq_mk'_iff] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s : ↥P.primeCompl
e : ∃ (s_1 : ↥P.primeCompl), s_1 • s • m = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥P.primeCompl) 1 a
⊢ False
have obtain : ∀ (t : ↥P.primeCompl) (ht : t • s • m = t • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥P.primeCompl) 1 a), False
Tactic: obtain ⟨t, ht⟩ := e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Membership.mem (α := Mₚ P) (γ := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N)
      ((f P : (a : M) → Mₚ P) m : Mₚ P)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
h_1 : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s t : ↥P.primeCompl
ht : t • s • m = t • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥P.primeCompl) 1 a
⊢ False
have ht₁ : (t * s) • m = (t * 1) • a
Tactic: simp_rw [smul_smul] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m m' : M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Eq.{u_5 + 1} (α := Mₚ P) ((f P : (a : M) → Mₚ P) m : Mₚ P) ((f P : (a : M) → Mₚ P) m' : Mₚ P)
⊢ m = m'
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'
Tactic: rw [← one_smul R m, ← one_smul R m']
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m m' : M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Eq.{u_5 + 1} (α := Mₚ P) ((f P : (a : M) → Mₚ P) m : Mₚ P) ((f P : (a : M) → Mₚ P) m' : Mₚ P)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'
have by_contra : ∀ (ne : ¬HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'), False
Tactic: by_contra ne
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m m' : M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Eq.{u_5 + 1} (α := Mₚ P) ((f P : (a : M) → Mₚ P) m : Mₚ P) ((f P : (a : M) → Mₚ P) m' : Mₚ P)
ne : ¬HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'
⊢ False
have have : ∀ (P : Ideal R) (mP : P.IsMaximal) (le : eqIdeal R m m' ≤ P), False
Tactic: have ⟨P, mP, le⟩ := (eqIdeal R m m').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m m' : M
h :
  ∀ (P : Ideal R) [inst_6 : P.IsMaximal],
    Eq.{u_5 + 1} (α := Mₚ P) ((f P : (a : M) → Mₚ P) m : Mₚ P) ((f P : (a : M) → Mₚ P) m' : Mₚ P)
ne : ¬HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'
P : Ideal R
mP : P.IsMaximal
le : eqIdeal R m m' ≤ P
⊢ False
have have : ∀ (s : ↥P.primeCompl) (hs : s • m = s • m'), False
Tactic: have ⟨s, hs⟩ := (IsLocalizedModule.eq_iff_exists P.primeCompl _).mp (h P)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
h : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], Eq.{u_5 + 1} (α := Mₚ P) ((f P : (a : M) → Mₚ P) m : Mₚ P) (0 : Mₚ P)
P : Ideal R
h_1 : P.IsMaximal
⊢ Eq.{u_5 + 1} (α := Mₚ P) ((f P : (a : M) → Mₚ P) m : Mₚ P) ((f P : (a : M) → Mₚ P) 0 : Mₚ P)
have rw : Eq.{u_5 + 1} (α := Mₚ P) (0 : Mₚ P) ((f P : (a : M) → Mₚ P) 0 : Mₚ P)
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
m : M
h : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], Eq.{u_5 + 1} (α := Mₚ P) ((f P : (a : M) → Mₚ P) m : Mₚ P) (0 : Mₚ P)
P : Ideal R
h_1 : P.IsMaximal
rw : Eq.{u_5 + 1} (α := Mₚ P) (0 : Mₚ P) ((f P : (a : M) → Mₚ P) 0 : Mₚ P)
⊢ Eq.{u_5 + 1} (α := Mₚ P) ((f P : (a : M) → Mₚ P) m : Mₚ P) ((f P : (a : M) → Mₚ P) 0 : Mₚ P)
have rw₁ : Eq.{u_5 + 1} (α := Mₚ P) 0 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_4 : (P : Ideal R) → [inst_6 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_6 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_5 : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton.{u_5 + 1} (Mₚ P)
⊢ Subsingleton M
have rw : ∀ (y : M), y = 0
Tactic: rw [subsingleton_iff_forall_eq 0]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
x y : M
h :
  ∀ (r : (↑s : Type u_1)), Eq.{u_5 + 1} (α := Mₚ r) ((f r : (a : M) → Mₚ r) x : Mₚ r) ((f r : (a : M) → Mₚ r) y : Mₚ r)
⊢ x = y
have suffices : Eq (α := Ideal R) (eqIdeal R x y) ⊤
Tactic: suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (eq_top_iff_one _).mp this
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
x y : M
h :
  ∀ (r : (↑s : Type u_1)), Eq.{u_5 + 1} (α := Mₚ r) ((f r : (a : M) → Mₚ r) x : Mₚ r) ((f r : (a : M) → Mₚ r) y : Mₚ r)
⊢ Eq (α := Ideal R) (eqIdeal R x y) ⊤
have by_contra : ∀ (ne : ¬Eq (α := Ideal R) (eqIdeal R x y) ⊤), False
Tactic: by_contra ne
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
x y : M
h :
  ∀ (r : (↑s : Type u_1)), Eq.{u_5 + 1} (α := Mₚ r) ((f r : (a : M) → Mₚ r) x : Mₚ r) ((f r : (a : M) → Mₚ r) y : Mₚ r)
ne : ¬Eq (α := Ideal R) (eqIdeal R x y) ⊤
⊢ False
have have : ∀ (r : R) (hrs : r ∈ s) (disj : Disjoint (↑(eqIdeal R x y) : Set R) (↑(Submonoid.powers r) : Set R)), False
Tactic: have ⟨r, hrs, disj⟩ := exists_disjoint_powers_of_span_eq_top s span_eq _ ne
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
x y : M
h :
  ∀ (r : (↑s : Type u_1)), Eq.{u_5 + 1} (α := Mₚ r) ((f r : (a : M) → Mₚ r) x : Mₚ r) ((f r : (a : M) → Mₚ r) y : Mₚ r)
ne : ¬Eq (α := Ideal R) (eqIdeal R x y) ⊤
r_1 : R
hrs : r_1 ∈ s
disj : Disjoint (↑(eqIdeal R x y) : Set R) (↑(Submonoid.powers r_1) : Set R)
r : (↑s : Type u_1) := Subtype.mk (p := fun (x : R) ↦ x ∈ s) r_1 hrs
⊢ False
have have : ∀ (n : ℕ)
  (eq :
    Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
          ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) sorry •
        x =
      Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
          ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) sorry •
        y),
  False
Tactic: have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalizedModule.eq_iff_exists (.powers r.1) _).mp (h r)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
m : M
N : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Membership.mem (α := Mₚ r) (localized₀ (Submonoid.powers (↑r : R)) (f r) N) ((f r : (a : M) → Mₚ r) m : Mₚ r)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ m ∈ N
have suffices : I = ⊤
Tactic: suffices I = ⊤ by simpa [I] using I.eq_top_iff_one.mp this
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
m : M
N : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Membership.mem (α := Mₚ r) (localized₀ (Submonoid.powers (↑r : R)) (f r) N) ((f r : (a : M) → Mₚ r) m : Mₚ r)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
⊢ I = ⊤
have by_contra! : ∀ (ne : I ≠ ⊤), False
Tactic: by_contra! ne
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
m : M
N : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Membership.mem (α := Mₚ r) (localized₀ (Submonoid.powers (↑r : R)) (f r) N) ((f r : (a : M) → Mₚ r) m : Mₚ r)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
⊢ False
have have : ∀ (r : R) (hrs : r ∈ s) (disj : Disjoint (↑I : Set R) (↑(Submonoid.powers r) : Set R)), False
Tactic: have ⟨r, hrs, disj⟩ := exists_disjoint_powers_of_span_eq_top s span_eq _ ne
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
m : M
N : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Membership.mem (α := Mₚ r) (localized₀ (Submonoid.powers (↑r : R)) (f r) N) ((f r : (a : M) → Mₚ r) m : Mₚ r)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r_1 : R
hrs : r_1 ∈ s
disj : Disjoint (↑I : Set R) (↑(Submonoid.powers r_1) : Set R)
r : (↑s : Type u_1) := Subtype.mk (p := fun (x : R) ↦ x ∈ s) r_1 hrs
⊢ False
have obtain : ∀ (a : M) (ha : a ∈ N) (t : ↥(Submonoid.powers (↑r : R))) (e : mk' (f r) a t = (f r : (a : M) → Mₚ r) m), False
Tactic: obtain ⟨a, ha, t, e⟩ := h r
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
m : M
N : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Membership.mem (α := Mₚ r) (localized₀ (Submonoid.powers (↑r : R)) (f r) N) ((f r : (a : M) → Mₚ r) m : Mₚ r)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r_1 : R
hrs : r_1 ∈ s
disj : Disjoint (↑I : Set R) (↑(Submonoid.powers r_1) : Set R)
r : (↑s : Type u_1) := Subtype.mk (p := fun (x : R) ↦ x ∈ s) r_1 hrs
a : M
ha : a ∈ N
t : ↥(Submonoid.powers (↑r : R))
e : mk' (f r) a t = (f r : (a : M) → Mₚ r) m
⊢ False
have e₁ : ∃ (s_1 : ↥(Submonoid.powers (↑r : R))),
  s_1 • t • m = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Submonoid.powers (↑r : R))) 1 a
Tactic: rw [← IsLocalizedModule.mk'_one (.powers r.1), IsLocalizedModule.mk'_eq_mk'_iff] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Submodule (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set R
span_eq : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u_1) → Type u_5
inst_3 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_4 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
f : (r : (↑s : Type u_1)) → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
m : M
N : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Membership.mem (α := Mₚ r) (localized₀ (Submonoid.powers (↑r : R)) (f r) N) ((f r : (a : M) → Mₚ r) m : Mₚ r)
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r_1 : R
hrs : r_1 ∈ s
disj : Disjoint (↑I : Set R) (↑(Submonoid.powers r_1) : Set R)
r : (↑s : Type u_1) := Subtype.mk (p := fun (x : R) ↦ x ∈ s) r_1 hrs
a : M
ha : a ∈ N
t : ↥(Submonoid.powers (↑r : R))
e :
  ∃ (s_1 : ↥(Submonoid.powers (↑r : R))),
    s_1 • t • m = s_1 • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Submonoid.powers (↑r : R))) 1 a
⊢ False
have have : ∀ (u : ↥(Submonoid.powers (↑r : R)))
  (hu : u • t • m = u • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Submonoid.powers (↑r : R))) 1 a), False
Tactic: have ⟨u, hu⟩ := e