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 * v
⊢ a M * v ∈ (↑I : Submodule R A) * (R ∙ v)

Tactic:
have := Submodule.mul_mem_mul (ha M hM) (Submodule.mem_span_singleton_self v)
-- 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_2 : ∀ 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 * v
this : a M * v ∈ (↑I : Submodule R A) * (R ∙ v)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Membership.mem (α := A) ((↑I : Submodule R A) * (R ∙ v)) ((algebraMap R A : (a : R) → A) c : A)),
    c ∈
      (↑(Submodule.comap (Algebra.linearMap R A)
            ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v))) :
        Set R)
⊢ c ∈
    (↑(Submodule.comap (Algebra.linearMap R A)
          ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v))) :
      Set R)

Tactic:
rwa [← hc] at this
-- 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
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * v)

Tactic:
have hmem : a M * v ∈ IsLocalization.coeSubmodule A M := by
    obtain ⟨c, hc⟩ := this _ (ha M hM) v hv
    refine IsLocalization.coeSubmodule_mono _ hJM ⟨c, ?_, hc⟩
    have := Submodule.mul_mem_mul (ha M hM) (Submodule.mem_span_singleton_self v)
    rwa [← hc] at this
-- 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) (a M * v)
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (∑ x ∈ s, u x • (a M * b x))

Tactic:
simp_rw [v, Finset.mul_sum, mul_smul_comm] at hmem

Premises used: Finset.mul_sum, mul_smul_comm
-- 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) (∑ x ∈ s, u x • (a M * b x))
rw :
  ∀ (hmem : Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A) (u M • (a M * b M))),
    False
a₁ :
  ∀
    (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))
⊢ False

Tactic:
rw [← s.add_sum_erase _ hM, Submodule.add_mem_iff_left] at hmem

Premises used: Finset.add_sum_erase, Submodule.add_mem_iff_left
-- 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 : Submodule R A) (u M • (a M * b M))
⊢ False

Tactic:
hm M hM ?_
-- 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 : Submodule R A) (u M • (a M * b M))
refine : Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * b M)
⊢ False

Tactic:
refine hm M hM ?_
-- 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 : Submodule R A) (u M • (a M * b M))
obtain :
  ∀ (c : R) (hc : (algebraMap R A : (a : R) → A) c = a M * b M),
    Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * b M)
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * b M)

Tactic:
obtain ⟨c, hc : algebraMap R A c = a M * b M⟩ := this _ (ha M hM) _ (hb M hM)
-- 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 : Submodule R A) (u M • (a M * b M))
c : R
hc : (algebraMap R A : (a : R) → A) c = a M * b M
rw :
  ∀
    (hmem :
      Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A)
        (HSMul.hSMul (β := A) (u M) ((algebraMap R A : (a : R) → A) c : A)))
    (hc : (algebraMap R A : (a : R) → A) c = a M * b M),
    Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
      ((algebraMap R A : (a : R) → A) c : A)
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * b M)

Tactic:
rw [← hc] at hmem ⊢
-- 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
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A)
    (HSMul.hSMul (β := A) (u M) ((algebraMap R A : (a : R) → A) c : A))
hc : (algebraMap R A : (a : R) → A) c = a M * b M
⊢ Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A)
    ((algebraMap R A : (a : R) → A) (u M * c) : A)

Tactic:
rw [Algebra.smul_def, ← map_mul] at hmem

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
c : R
hmem :
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A)
    (HSMul.hSMul (β := A) (u M) ((algebraMap R A : (a : R) → A) c : A))
hc : (algebraMap R A : (a : R) → A) c = a M * b M
hmem₁ :
  Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A)
    ((algebraMap R A : (a : R) → A) (u M * c) : A)
⊢ (algebraMap R A : (a : R) → A) c = a M * b M

Tactic:
rw [Algebra.smul_def, ← map_mul] at hmem

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
c : R
hmem :
  Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A)
    ((algebraMap R A : (a : R) → A) (u M * c) : A)
hc : (algebraMap R A : (a : R) → A) c = a M * b M
obtain :
  ∀ (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)),
    Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
      ((algebraMap R A : (a : R) → A) c : A)
⊢ Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M) ((algebraMap R A : (a : R) → A) c : A)

Tactic:
obtain ⟨d, hdM, he⟩ := hmem
-- 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)
⊢ u M * c ∈ (↑M : Set R)

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

Premises used: IsLocalization.injective