awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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
have refine : Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * b M)
Tactic: refine hm M hM ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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))
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * b M)
have 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)
Tactic: obtain ⟨c, hc : algebraMap R A c = a M * b M⟩ := this _ (ha M hM) _ (hb M hM)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * b M)
have 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)
Tactic: rw [← hc] at hmem ⊢
Cleared hypotheses: hmem, hc
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
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) ((algebraMap R A : (a : R) → A) c : A)
have hmem₁ : 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
Cleared hypotheses: hmem, hc
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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
⊢ Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M) ((algebraMap R A : (a : R) → A) c : A)
have 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)
Tactic: obtain ⟨d, hdM, he⟩ := hmem
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
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)
⊢ Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M) ((algebraMap R A : (a : R) → A) c : A)
have hdM₁ : u M * c ∈ (↑M : Set R)
Tactic: rw [IsLocalization.injective _ hS he] at hdM
Cleared hypotheses: hdM, he
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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))
have a₁ : ∀ (M' : Ideal R) (hM' : M' ∈ s.erase M),
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (u M' • (a M * b M'))
Tactic: refine Submodule.sum_mem _ fun M' hM' => ?_
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
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
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (u M' • (a M * b M'))
have hM'₁ : M' ≠ M ∧ M' ∈ s
Tactic: rw [Finset.mem_erase] at hM'
Cleared hypotheses: hM'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (u M' • (a M * b M'))
have 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'))
Tactic: obtain ⟨c, hc⟩ := this _ (ha M hM) _ (hb M' hM'.2)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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 (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (u M' • (a M * b M'))
have a₁ : Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
  ((algebraMap R A : (a : R) → A) (u M' * c) : A)
Tactic: rw [← hc, Algebra.smul_def, ← map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
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 (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    ((algebraMap R A : (a : R) → A) (u M' * c) : A)
have hu₁ : Membership.mem (γ := Ideal R) (⨅ M'_1 ∈ s.erase M', M'_1) (u M')
Tactic: specialize hu M' hM'.2
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (hypothesis)
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')
⊢ Membership.mem (α := A) (γ := Submodule R A) (IsLocalization.coeSubmodule A M)
    ((algebraMap R A : (a : R) → A) (u M' * c) : A)
have hu₁ : ∀ (i : Ideal R) (i_1 : i ≠ M' ∧ i ∈ s), u M' ∈ i
Tactic: simp_rw [Ideal.mem_iInf, Finset.mem_erase] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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
⊢ Submodule.IsPrincipal I
have inl : Submodule.IsPrincipal.{u_1, u_1} (R := R) (M := R) ⊥
Tactic: obtain rfl | hI := eq_or_ne I ⊥
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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) ⊥
⊢ Submodule.IsPrincipal I
have inr : ∀ (hI : I ≠ ⊥), Submodule.IsPrincipal I
Tactic: obtain rfl | hI := eq_or_ne I ⊥
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.PID (goal)
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 ≠ ⊥
⊢ Submodule.IsPrincipal I
have inr : IsUnit (M := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
Tactic: apply Ideal.IsPrincipal.of_finite_maximals_of_isUnit h