awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M)
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
c : R
hc : (algebraMap R A : (a : R) → A) c = a M * b M
d : R
hdM : d ∈ (↑M : Set R)
he : Eq.{u_2 + 1} (α := A) ((Algebra.linearMap R A : (a : R) → A) d : A) ((algebraMap R A : (a : R) → A) (u M * c) : A)
hdM₁ : u M * c ∈ (↑M : Set R)
⊢ Eq.{u_2 + 1} (α := A) ((Algebra.linearMap R A : (a : R) → A) d : A) ((algebraMap R A : (a : R) → A) (u M * c) : A)

Tactic:
rw [IsLocalization.injective _ hS he] at hdM

Premises used: IsLocalization.injective
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M)
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
c : R
hc : (algebraMap R A : (a : R) → A) c = a M * b M
d : R
hdM : u M * c ∈ (↑M : Set R)
he : Eq.{u_2 + 1} (α := A) ((Algebra.linearMap R A : (a : R) → A) d : A) ((algebraMap R A : (a : R) → A) (u M * c) : A)
⊢ Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M) ((algebraMap R A : (a : R) → A) c : A)

Tactic:
Submodule.mem_map_of_mem <|
        ((hf.mem_toFinset.1 hM).isPrime.mem_or_mem hdM).resolve_left <| hum M hM

Premises used: Set.Mem, Set.Finite.mem_toFinset, Or.resolve_left, Ideal.IsMaximal.isPrime, Ideal.IsPrime.mem_or_mem, Iff.mp, Submodule.mem_map_of_mem
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M)
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
c : R
hc : (algebraMap R A : (a : R) → A) c = a M * b M
d : R
hdM : u M * c ∈ (↑M : Set R)
he : Eq.{u_2 + 1} (α := A) ((Algebra.linearMap R A : (a : R) → A) d : A) ((algebraMap R A : (a : R) → A) (u M * c) : A)
⊢ Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M) ((algebraMap R A : (a : R) → A) c : A)

Tactic:
exact Submodule.mem_map_of_mem <|
        ((hf.mem_toFinset.1 hM).isPrime.mem_or_mem hdM).resolve_left <| hum M hM

Premises used: Set.Finite.mem_toFinset, Or.resolve_left, Ideal.IsMaximal.isPrime, Ideal.IsPrime.mem_or_mem, Iff.mp, Submodule.mem_map_of_mem
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M)
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    (u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x))
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A)
    (∑ x ∈ s.erase M, u x • (a M * b x))

Tactic:
Submodule.sum_mem _ fun M' hM' => ?_

Premises used: Set.Mem, Submodule.sum_mem
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M)
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    (u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x))
a₁ :
  ∀ (M' : Ideal R) (hM' : M' ∈ s.erase M),
    Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (u M' • (a M * b M'))
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A)
    (∑ x ∈ s.erase M, u x • (a M * b x))

Tactic:
refine Submodule.sum_mem _ fun M' hM' => ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M)
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    (u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x))
M' : Ideal R
hM' : M' ∈ s.erase M
⊢ M' ≠ M ∧ M' ∈ s

Tactic:
rw [Finset.mem_erase] at hM'

Premises used: Finset.mem_erase
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M)
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    (u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x))
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
a₁ :
  ∀ (c : R) (hc : (algebraMap R A : (a : R) → A) c = a M * b M'),
    Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (u M' • (a M * b M'))
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (u M' • (a M * b M'))

Tactic:
obtain ⟨c, hc⟩ := this _ (ha M hM) _ (hb M' hM'.2)

Premises used: And.right
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M)
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    (u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x))
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A : (a : R) → A) c = a M * b M'
a₁ :
  Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    ((algebraMap R A : (a : R) → A) (u M' * c) : A)
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (u M' • (a M * b M'))

Tactic:
rw [← hc, Algebra.smul_def, ← map_mul]

Premises used: map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hu : ∀ (M : Ideal R) (hM : M ∈ s), Membership.mem (γ := Ideal R) (⨅ M' ∈ s.erase M, M') (u M)
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    (u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x))
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A : (a : R) → A) c = a M * b M'
⊢ Membership.mem (γ := Ideal R) (⨅ M'_1 ∈ s.erase M', M'_1) (u M')

Tactic:
specialize hu M' hM'.2

Premises used: And.right
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    (u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x))
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A : (a : R) → A) c = a M * b M'
hu : Membership.mem (γ := Ideal R) (⨅ M'_1 ∈ s.erase M', M'_1) (u M')
⊢ ∀ (i : Ideal R) (i_1 : i ≠ M' ∧ i ∈ s), u M' ∈ i

Tactic:
simp_rw [Ideal.mem_iInf, Finset.mem_erase] at hu

Premises used: Finset.mem_erase, Ideal.mem_iInf
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    (u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x))
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A : (a : R) → A) c = a M * b M'
hu : ∀ (i : Ideal R) (i_1 : i ≠ M' ∧ i ∈ s), u M' ∈ i
⊢ Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    ((algebraMap R A : (a : R) → A) (u M' * c) : A)

Tactic:
Submodule.mem_map_of_mem <| M.mul_mem_right _ <| hu M ⟨hM'.1.symm, hM⟩

Premises used: Set.Mem, Ne.symm, And.left, Ideal.mul_mem_right, And.intro, Submodule.mem_map_of_mem
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
S : Submonoid R
inst_3 : IsLocalization S A
hS : S ≤ R⁰
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I I' : FractionalIdeal S A
hinv : (↑I : Submodule R A) * (↑I' : Submodule R A) = (↑1 : Submodule R A)
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this_1 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : (M : Ideal R) → A
ha : ∀ M ∈ s, a M ∈ I
b : (M : Ideal R) → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : (M : Ideal R) → R
hum : ∀ (M : Ideal R) (hM : M ∈ s), u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h :
  ¬Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
      ⊤
M : Ideal R
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
hM : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
this : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    (u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x))
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A : (a : R) → A) c = a M * b M'
hu : ∀ (i : Ideal R) (i_1 : i ≠ M' ∧ i ∈ s), u M' ∈ i
⊢ Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    ((algebraMap R A : (a : R) → A) (u M' * c) : A)

Tactic:
exact Submodule.mem_map_of_mem <| M.mul_mem_right _ <| hu M ⟨hM'.1.symm, hM⟩

Premises used: Ne.symm, And.left, Ideal.mul_mem_right, And.intro, Submodule.mem_map_of_mem
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
hf : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
⊢ Submodule.IsPrincipal I

Tactic:
(IsLocalization.coeSubmodule_isPrincipal _ le_rfl).mp
    (FractionalIdeal.isPrincipal.of_finite_maximals_of_inv le_rfl hf I
      (↑hI.unit⁻¹ : FractionalIdeal R⁰ (FractionRing R)) hI.unit.mul_inv)

Premises used: Units.val, le_rfl, Units.mul_inv, Inv.inv, FractionalIdeal.isPrincipal.of_finite_maximals_of_inv, Iff.mp, IsUnit.unit, FractionalIdeal.coeIdeal, IsLocalization.coeSubmodule_isPrincipal
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
h : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
inl : Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥
inr : ∀ (hI : I ≠ ⊥), Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal I

Tactic:
obtain rfl | hI := eq_or_ne I ⊥

Premises used: Bot.bot, eq_or_ne, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
h : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
⊢ Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥

Tactic:
bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
h : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
⊢ Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥

Tactic:
exact bot_isPrincipal

Premises used: bot_isPrincipal
-- Module: Mathlib.RingTheory.DedekindDomain.PID
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
h : Set.Finite.{u_1} (α := Ideal R) {I : Ideal R | I.IsMaximal}
I : Ideal R
hI : I ≠ ⊥
inr : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
⊢ Submodule.IsPrincipal I

Tactic:
apply Ideal.IsPrincipal.of_finite_maximals_of_isUnit h

Premises used: Ideal.IsPrincipal.of_finite_maximals_of_isUnit