awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
N : Submodule R M
h : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], Eq (α := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N) ⊥
P : Ideal R
hP : P.IsMaximal
⊢ Eq (α := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N) (localized₀ P.primeCompl (f P) ⊥)

Tactic:
simpa using h P
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
N : Submodule R M
h : ∀ (P : Ideal R) [inst_6 : P.IsMaximal], Eq (α := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N) ⊤
P : Ideal R
hP : P.IsMaximal
⊢ Eq (α := Submodule R (Mₚ P)) (localized₀ P.primeCompl (f P) N) (localized₀ P.primeCompl (f P) ⊤)

Tactic:
simpa using h P
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'
⊢ m = m'

Tactic:
rw [← one_smul R m, ← one_smul R m']

Premises used: one_smul
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
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
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 m'

Tactic:
by_contra ne
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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'
have : ∀ (P : Ideal R) (mP : P.IsMaximal) (le : eqIdeal R m m' ≤ P), False
⊢ False

Tactic:
have ⟨P, mP, le⟩ := (eqIdeal R m m').exists_le_maximal ((Ideal.ne_top_iff_one _).mpr ne)
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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
have : ∀ (s : ↥P.primeCompl) (hs : s • m = s • m'), False
⊢ False

Tactic:
have ⟨s, hs⟩ := (IsLocalizedModule.eq_iff_exists P.primeCompl _).mp (h P)
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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
s : ↥P.primeCompl
hs : s • m = s • m'
⊢ False

Tactic:
s.2 (le hs)

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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
s : ↥P.primeCompl
hs : s • m = s • m'
⊢ False

Tactic:
exact s.2 (le hs)

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
rw₁ rw₂ : Eq.{u_5 + 1} (α := Mₚ P) 0 0
⊢ Eq.{u_5 + 1} (α := Mₚ P) ((f P : (a : M) → Mₚ P) m : Mₚ P) ((f P : (a : M) → Mₚ P) 0 : Mₚ P)

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M₁
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_5 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_6 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
f : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_7 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
M₁ₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (M₁ₚ P)
inst_9 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_6} R (M₁ₚ P)
f₁ : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_3, u_6} (RingHom.id R) M₁ (M₁ₚ P)
inst_10 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule (M' := M₁ₚ P) P.primeCompl (f₁ P)
g g' : M →ₗ[R] M₁
h :
  ∀ (P : Ideal R) [inst_11 : P.IsMaximal],
    Eq (α := LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ P) (M₁ₚ P))
      ((IsLocalizedModule.map P.primeCompl (f P) (f₁ P) : (a : M →ₗ[R] M₁) → Mₚ P →ₗ[R] M₁ₚ P) g :
        LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ P) (M₁ₚ P))
      ((IsLocalizedModule.map P.primeCompl (f P) (f₁ P) : (a : M →ₗ[R] M₁) → Mₚ P →ₗ[R] M₁ₚ P) g' :
        LinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (Mₚ P) (M₁ₚ P))
x : M
P : Ideal R
h_1 : P.IsMaximal
⊢ Eq.{u_6 + 1} (α := M₁ₚ P) ((f₁ P : (a : M₁) → M₁ₚ P) ((g : (a : M) → M₁) x : M₁) : M₁ₚ P)
    ((f₁ P : (a : M₁) → M₁ₚ P) ((g' : (a : M) → M₁) x : M₁) : M₁ₚ P)

Tactic:
simpa only [IsLocalizedModule.map_apply] using DFunLike.congr_fun (h P) (f P x)

Premises used: DFunLike.congr_fun, IsLocalizedModule.map_apply, DFunLike.coe
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
rw : ∀ (y : M), y = 0
⊢ Subsingleton M

Tactic:
rw [subsingleton_iff_forall_eq 0]

Premises used: subsingleton_iff_forall_eq, OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
x : M
⊢ x = 0

Tactic:
Module.eq_of_localization_maximal Mₚ f x 0 fun _ _ ↦ Subsingleton.elim _ _

Premises used: Subsingleton.elim, OfNat.ofNat, DFunLike.coe, Module.eq_of_localization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
x : M
⊢ x = 0

Tactic:
exact Module.eq_of_localization_maximal Mₚ f x 0 fun _ _ ↦ Subsingleton.elim _ _

Premises used: Subsingleton.elim, OfNat.ofNat, DFunLike.coe, Module.eq_of_localization_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_4 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Algebra.{u_1, u_4} R (Rₚ P)
inst_5 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_4} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_7 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_4, u_5} (Rₚ P) (Mₚ P)
inst_9 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsScalarTower.{u_1, u_4, u_5} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
N₁ N₂ : Submodule R M
h :
  ∀ (P : Ideal R) [inst_11 : P.IsMaximal],
    Eq (α := Submodule.{u_4, u_5} (Rₚ P) (Mₚ P)) (localized' (Rₚ P) P.primeCompl (f P) N₁)
      (localized' (Rₚ P) P.primeCompl (f P) N₂)
⊢ N₁ = N₂

Tactic:
eq_of_localization₀_maximal Mₚ f fun P _ ↦ congr(restrictScalars _ $(h P))

Premises used: congrArg, Submodule.restrictScalars, id, Submodule.eq_of_localization₀_maximal
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_4 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Algebra.{u_1, u_4} R (Rₚ P)
inst_5 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_4} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_7 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_4, u_5} (Rₚ P) (Mₚ P)
inst_9 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsScalarTower.{u_1, u_4, u_5} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_11 : P.IsMaximal],
    Eq (α := Submodule.{u_4, u_5} (Rₚ P) (Mₚ P)) (localized' (Rₚ P) P.primeCompl (f P) N) ⊥
P : Ideal R
hP : P.IsMaximal
⊢ Eq (α := Submodule.{u_4, u_5} (Rₚ P) (Mₚ P)) (localized' (Rₚ P) P.primeCompl (f P) N)
    (localized' (Rₚ P) P.primeCompl (f P) ⊥)

Tactic:
simpa using h P
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_4 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Algebra.{u_1, u_4} R (Rₚ P)
inst_5 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_4} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_7 : (P : Ideal R) → [inst_11 : P.IsMaximal] → Module.{u_1, u_5} R (Mₚ P)
inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_4, u_5} (Rₚ P) (Mₚ P)
inst_9 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsScalarTower.{u_1, u_4, u_5} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_11 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_11 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
N : Submodule R M
h :
  ∀ (P : Ideal R) [inst_11 : P.IsMaximal],
    Eq (α := Submodule.{u_4, u_5} (Rₚ P) (Mₚ P)) (localized' (Rₚ P) P.primeCompl (f P) N) ⊤
P : Ideal R
hP : P.IsMaximal
⊢ Eq (α := Submodule.{u_4, u_5} (Rₚ P) (Mₚ P)) (localized' (Rₚ P) P.primeCompl (f P) N)
    (localized' (Rₚ P) P.primeCompl (f P) ⊤)

Tactic:
simpa using h P
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
this : Eq (α := Ideal R) (eqIdeal R x y) ⊤
⊢ x = y

Tactic:
simpa [Module.eqIdeal] using (eq_top_iff_one _).mp this

Premises used: Ideal.eq_top_iff_one, Iff.mp, Module.eqIdeal
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
suffices : Eq (α := Ideal R) (eqIdeal R x y) ⊤
⊢ x = y

Tactic:
suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (eq_top_iff_one _).mp this
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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)
by_contra : ∀ (ne : ¬Eq (α := Ideal R) (eqIdeal R x y) ⊤), False
⊢ Eq (α := Ideal R) (eqIdeal R x y) ⊤

Tactic:
by_contra ne
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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) ⊤
have : ∀ (r : R) (hrs : r ∈ s) (disj : Disjoint (↑(eqIdeal R x y) : Set R) (↑(Submonoid.powers r) : Set R)), False
⊢ False

Tactic:
have ⟨r, hrs, disj⟩ := exists_disjoint_powers_of_span_eq_top s span_eq _ ne
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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
have :
  ∀ (n : ℕ)
    (eq :
      Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯ •
          x =
        Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯ •
          y),
    False
⊢ False

Tactic:
have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalizedModule.eq_iff_exists (.powers r.1) _).mp (h r)
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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
n : ℕ
eq :
  Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
        ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯ •
      x =
    Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
        ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯ •
      y
⊢ False

Tactic:
Set.disjoint_left.mp disj eq ⟨n, rfl⟩

Premises used: Set.disjoint_left, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.LocalProperties.Submodule
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
n : ℕ
eq :
  Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
        ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯ •
      x =
    Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
        ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯ •
      y
⊢ False

Tactic:
exact Set.disjoint_left.mp disj eq ⟨n, rfl⟩

Premises used: Set.disjoint_left, Exists.intro, Iff.mp, rfl