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
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 : M
h : ∀ (r : (↑s : Type u_1)), Eq.{u_5 + 1} (α := Mₚ r) ((f r : (a : M) → Mₚ r) x : Mₚ r) (0 : Mₚ r)
⊢ ∀ (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) 0 : Mₚ r)

Tactic:
simpa only [map_zero] using h

Premises used: map_zero
-- 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) (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
this : I = ⊤
⊢ m ∈ N

Tactic:
simpa [I] using I.eq_top_iff_one.mp this

Premises used: Ideal.eq_top_iff_one, Iff.mp
-- 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) (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
suffices : I = ⊤
⊢ m ∈ N

Tactic:
suffices I = ⊤ by simpa [I] using I.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) (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
by_contra! : ∀ (ne : I ≠ ⊤), False
⊢ I = ⊤

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) (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 ≠ ⊤
have : ∀ (r : R) (hrs : r ∈ s) (disj : Disjoint (↑I : 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) (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
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
⊢ False

Tactic:
obtain ⟨a, ha, t, e⟩ := 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) (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
⊢ ∃ (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

Premises used: IsLocalizedModule.mk'_eq_mk'_iff, IsLocalizedModule.mk'_one, Submonoid.powers, Subtype.val
-- 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) (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
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
⊢ False

Tactic:
have ⟨u, hu⟩ := e
-- 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) (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
u : ↥(Submonoid.powers (↑r : R))
hu : u • t • m = u • HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Submonoid.powers (↑r : R))) 1 a
⊢ (u * t) • m = (u * 1) • a

Tactic:
simp_rw [smul_smul] at hu

Premises used: smul_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
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
u : ↥(Submonoid.powers (↑r : R))
hu : (u * t) • m = (u * 1) • a
⊢ (↑(u * t) : R) ∈ (↑I : Set R)

Tactic:
apply hu ▸ smul_mem _ _ ha
-- 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) (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
u : ↥(Submonoid.powers (↑r : R))
hu : (u * t) • m = (u * 1) • a
⊢ False

Tactic:
exact Set.disjoint_right.mp disj (u * t).2 (by apply hu ▸ smul_mem _ _ ha)

Premises used: HMul.hMul, Set.disjoint_right, Iff.mp, 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
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)
N P : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    localized₀ (Submonoid.powers (↑r : R)) (f r) N ≤ localized₀ (Submonoid.powers (↑r : R)) (f r) P
m : M
hm : m ∈ N
r : (↑s : Type u_1)
⊢ mk' (S := Submonoid.powers (↑r : R)) (f r) m 1 = (f r : (a : M) → Mₚ r) m

Tactic:
simp
-- 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) (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)
N P : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    localized₀ (Submonoid.powers (↑r : R)) (f r) N = localized₀ (Submonoid.powers (↑r : R)) (f r) P
⊢ N = P

Tactic:
le_antisymm (le_of_isLocalized_span s span_eq _ _ fun r ↦ (h r).le)
    (le_of_isLocalized_span s span_eq _ _ fun r ↦ (h r).ge)

Premises used: Eq.ge, Eq.le, Submodule.le_of_isLocalized_span, le_antisymm
-- 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) (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)
N : Submodule R M
h : ∀ (r : (↑s : Type u_1)), localized₀ (Submonoid.powers (↑r : R)) (f r) N = ⊥
x : (↑s : Type u_1)
⊢ localized₀ (Submonoid.powers (↑x : R)) (f x) N = localized₀ (Submonoid.powers (↑x : R)) (f x) ⊥

Tactic:
simp only [h, Submodule.localized₀_bot]

Premises used: Submodule.localized₀_bot
-- 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) (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)
N : Submodule R M
h : ∀ (r : (↑s : Type u_1)), localized₀ (Submonoid.powers (↑r : R)) (f r) N = ⊤
x : (↑s : Type u_1)
⊢ localized₀ (Submonoid.powers (↑x : R)) (f x) N = localized₀ (Submonoid.powers (↑x : R)) (f x) ⊤

Tactic:
simp only [h, Submodule.localized₀_top]

Premises used: Submodule.localized₀_top
-- 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) (Ideal.span s) ⊤
Rₚ : (↑s : Type u_1) → Type u_4
inst_3 : (r : (↑s : Type u_1)) → CommSemiring (Rₚ r)
inst_4 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑r : R) (Rₚ r)
Mₚ : (↑s : Type u_1) → Type u_5
inst_6 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_7 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
inst_8 : (r : (↑s : Type u_1)) → Module.{u_4, u_5} (Rₚ r) (Mₚ r)
inst_9 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_5} R (Rₚ 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_10 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
N P : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Eq (α := Submodule.{u_4, u_5} (Rₚ r) (Mₚ r)) (localized' (Rₚ r) (Submonoid.powers (↑r : R)) (f r) N)
      (localized' (Rₚ r) (Submonoid.powers (↑r : R)) (f r) P)
⊢ N = P

Tactic:
eq_of_isLocalized₀_span s span_eq _ f fun r ↦ congr(restrictScalars _ $(h r))

Premises used: congrArg, Submodule.restrictScalars, id, Submodule.eq_of_isLocalized₀_span
-- 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) (Ideal.span s) ⊤
Rₚ : (↑s : Type u_1) → Type u_4
inst_3 : (r : (↑s : Type u_1)) → CommSemiring (Rₚ r)
inst_4 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑r : R) (Rₚ r)
Mₚ : (↑s : Type u_1) → Type u_5
inst_6 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_7 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
inst_8 : (r : (↑s : Type u_1)) → Module.{u_4, u_5} (Rₚ r) (Mₚ r)
inst_9 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_5} R (Rₚ 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_10 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
N : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Eq (α := Submodule.{u_4, u_5} (Rₚ r) (Mₚ r)) (localized' (Rₚ r) (Submonoid.powers (↑r : R)) (f r) N) ⊥
x : (↑s : Type u_1)
⊢ Eq (α := Submodule.{u_4, u_5} (Rₚ x) (Mₚ x)) (localized' (Rₚ x) (Submonoid.powers (↑x : R)) (f x) N)
    (localized' (Rₚ x) (Submonoid.powers (↑x : R)) (f x) ⊥)

Tactic:
simp only [h, Submodule.localized'_bot]

Premises used: Submodule.localized'_bot
-- 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) (Ideal.span s) ⊤
Rₚ : (↑s : Type u_1) → Type u_4
inst_3 : (r : (↑s : Type u_1)) → CommSemiring (Rₚ r)
inst_4 : (r : (↑s : Type u_1)) → Algebra.{u_1, u_4} R (Rₚ r)
inst_5 : ∀ (r : (↑s : Type u_1)), IsLocalization.Away.{u_1, u_4} (↑r : R) (Rₚ r)
Mₚ : (↑s : Type u_1) → Type u_5
inst_6 : (r : (↑s : Type u_1)) → AddCommMonoid (Mₚ r)
inst_7 : (r : (↑s : Type u_1)) → Module.{u_1, u_5} R (Mₚ r)
inst_8 : (r : (↑s : Type u_1)) → Module.{u_4, u_5} (Rₚ r) (Mₚ r)
inst_9 : ∀ (r : (↑s : Type u_1)), IsScalarTower.{u_1, u_4, u_5} R (Rₚ 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_10 : ∀ (r : (↑s : Type u_1)), IsLocalizedModule.Away (↑r : R) (f r)
N : Submodule R M
h :
  ∀ (r : (↑s : Type u_1)),
    Eq (α := Submodule.{u_4, u_5} (Rₚ r) (Mₚ r)) (localized' (Rₚ r) (Submonoid.powers (↑r : R)) (f r) N) ⊤
x : (↑s : Type u_1)
⊢ Eq (α := Submodule.{u_4, u_5} (Rₚ x) (Mₚ x)) (localized' (Rₚ x) (Submonoid.powers (↑x : R)) (f x) N)
    (localized' (Rₚ x) (Submonoid.powers (↑x : R)) (f x) ⊤)

Tactic:
simp only [h, Submodule.localized'_top]

Premises used: Submodule.localized'_top
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
h : ∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b
⊢ IsLocalRing R

Tactic:
⟨fun {a b} hab => h a b <| hab.symm ▸ isUnit_one⟩

Premises used: Eq.rec, IsLocalRing.of_is_unit_or_is_unit_of_add_one, isUnit_one, Eq.symm
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
h : ∃! I : Ideal R, I.IsMaximal
⊢ IsLocalRing R

Tactic:
@of_nonunits_add _ _
    (nontrivial_of_ne (0 : R) 1 <|
      let ⟨I, Imax, _⟩ := h
      fun H : 0 = 1 => Imax.1.1 <| I.eq_top_iff_one.2 <| H ▸ I.zero_mem)
    fun x y hx hy H =>
    let ⟨I, Imax, Iuniq⟩ := h
    let ⟨Ix, Ixmax, Hx⟩ := exists_max_ideal_of_mem_nonunits hx
    let ⟨Iy, Iymax, Hy⟩ := exists_max_ideal_of_mem_nonunits hy
    have xmemI : x ∈ I := Iuniq Ix Ixmax ▸ Hx
    have ymemI : y ∈ I := Iuniq Iy Iymax ▸ Hy
    Imax.1.1 <| I.eq_top_of_isUnit_mem (I.add_mem xmemI ymemI) H

Premises used: False, Ideal.eq_top_of_isUnit_mem, Eq.rec, Ideal.add_mem, _private.0.IsLocalRing.of_unique_max_ideal.match_1, exists_max_ideal_of_mem_nonunits, IsLocalRing.of_nonunits_add, Ideal.IsMaximal.out, And.left, _private.0.IsLocalRing.of_unique_max_ideal.match_2
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
h : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime
rcases :
  ∀ (P : Ideal R) (hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P) (hPnonzero : P ≠ ⊥)
    (hPnot_top : P ≠ ⊤), (∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P) → ∃! I : Ideal R, I.IsMaximal
⊢ ∃! I : Ideal R, I.IsMaximal

Tactic:
rcases h with ⟨P, ⟨hPnonzero, hPnot_top, _⟩, hPunique⟩
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∃! I : Ideal R, I.IsMaximal

Tactic:
⟨P, ⟨⟨hPnot_top, ?_⟩⟩, fun M hM => hPunique _ ⟨?_, Ideal.IsMaximal.isPrime hM⟩⟩

Premises used: Ideal.IsMaximal.isPrime, Ideal.IsMaximal.mk, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
refine_1 : ∀ (b : Ideal R), P < b → b = ⊤
refine_2 : ∀ (M : Ideal R) (hM : (fun (I : Ideal R) ↦ I.IsMaximal) M), M ≠ ⊥
⊢ ∃! I : Ideal R, I.IsMaximal

Tactic:
refine ⟨P, ⟨⟨hPnot_top, ?_⟩⟩, fun M hM => hPunique _ ⟨?_, Ideal.IsMaximal.isPrime hM⟩⟩
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤

Tactic:
Ideal.maximal_of_no_maximal fun M hPM hM => ne_of_lt hPM ?_

Premises used: Ideal.maximal_of_no_maximal, ne_of_lt
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
refine_1 : ∀ (M : Ideal R) (hPM : P < M) (hM : M.IsMaximal), P = M
⊢ ∀ (b : Ideal R), P < b → b = ⊤

Tactic:
refine Ideal.maximal_of_no_maximal fun M hPM hM => ne_of_lt hPM ?_

Premises used: Ideal.maximal_of_no_maximal, ne_of_lt
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hPM : P < M
hM : M.IsMaximal
⊢ P = M

Tactic:
(hPunique _ ⟨ne_bot_of_gt hPM, Ideal.IsMaximal.isPrime hM⟩).symm

Premises used: Ideal.IsMaximal.isPrime, And.intro, Eq.symm, ne_bot_of_gt
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
M : Ideal R
hPM : P < M
hM : M.IsMaximal
⊢ P = M

Tactic:
exact (hPunique _ ⟨ne_bot_of_gt hPM, Ideal.IsMaximal.isPrime hM⟩).symm

Premises used: Ideal.IsMaximal.isPrime, And.intro, Eq.symm, ne_bot_of_gt
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
hM : Ideal.IsMaximal.{u_1} (α := R) ⊥
⊢ False

Tactic:
hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero))

Premises used: Iff.mpr, bot_lt_iff_ne_bot, And.right, Ideal.IsMaximal.out
-- Module: Mathlib.RingTheory.LocalRing.Basic
Goal:
R : Type u_1
inst : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun (P : Ideal R) ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem' : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
hM : Ideal.IsMaximal.{u_1} (α := R) ⊥
⊢ False

Tactic:
exact hPnot_top (hM.1.2 P (bot_lt_iff_ne_bot.2 hPnonzero))

Premises used: Iff.mpr, bot_lt_iff_ne_bot, And.right, Ideal.IsMaximal.out