awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
⊢ (↑I : Submodule R A).IsPrincipal
have hv : v ∈ I'
Tactic: have hv : v ∈ I' := Submodule.sum_mem _ fun M hM => Submodule.smul_mem _ _ <| 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 : 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'
⊢ (↑I : Submodule R A).IsPrincipal
have I₁ : ∀
  (h :
    ¬Submodule.comap (Algebra.linearMap R A)
          ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) =
        ⊤),
  False
Tactic: refine
    FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top
      (Units.mkOfMulEqOne I I' hinv') hv (of_not_not fun h => ?_)
-- 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 : 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)) =
      ⊤
⊢ False
have obtain : ∀ (M : Ideal R) (hM : M.IsMaximal)
  (hJM :
    Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
      M),
  False
Tactic: obtain ⟨M, hM, hJM⟩ := Ideal.exists_le_maximal _ h
-- 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 : 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
hM : M.IsMaximal
hJM :
  Submodule.comap (Algebra.linearMap R A)
      ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v)) ≤
    M
⊢ False
have hM₁ : M ∈ hf.toFinset (s := {I : Ideal R | I.IsMaximal})
Tactic: replace hM := hf.mem_toFinset.2 hM
Cleared hypotheses: 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 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a_1 : (M : Ideal R) → A
ha_1 : ∀ M ∈ s, a_1 M ∈ I
b_1 : (M : Ideal R) → A
hb_1 : ∀ M ∈ s, b_1 M ∈ I'
hm : ∀ M ∈ s, a_1 M * b_1 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_1 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})
a : A
ha : a ∈ I
b : A
hb : b ∈ I'
⊢ ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
have hi : (↑I : Submodule R A) * (↑I' : Submodule R A) ≤ (↑1 : Submodule R A)
Tactic: have hi := hinv.le
-- 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 : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a_1 : (M : Ideal R) → A
ha_1 : ∀ M ∈ s, a_1 M ∈ I
b_1 : (M : Ideal R) → A
hb_1 : ∀ M ∈ s, b_1 M ∈ I'
hm : ∀ M ∈ s, a_1 M * b_1 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_1 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})
a : A
ha : a ∈ I
b : A
hb : b ∈ I'
hi : (↑I : Submodule R A) * (↑I' : Submodule R A) ≤ (↑1 : Submodule R A)
⊢ ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
have obtain : ∀ (c : R) (hc : (Algebra.linearMap R A : (a : R) → A) c = a * b), ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
Tactic: obtain ⟨c, -, hc⟩ := hi (Submodule.mul_mem_mul ha hb)
-- 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 : 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})
⊢ False
have this₁ : ∀ a ∈ I, ∀ b ∈ I', ∃ (c : R), (algebraMap R A : (a : R) → A) c = a * b
Tactic: have : ∀ a ∈ I, ∀ b ∈ I', ∃ c, algebraMap R _ c = a * b := by
    intro a ha b hb; have hi := hinv.le
    obtain ⟨c, -, hc⟩ := hi (Submodule.mul_mem_mul ha hb)
    exact ⟨c, 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
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * v)
have obtain : ∀ (c : R) (hc : (algebraMap R A : (a : R) → A) c = a M * v),
  Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * v)
Tactic: obtain ⟨c, hc⟩ := this _ (ha M hM) v hv
-- 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
hc : (algebraMap R A : (a : R) → A) c = a M * v
⊢ Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M) (a M * v)
have refine : c ∈
  (↑(Submodule.comap (Algebra.linearMap R A)
        ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v))) :
    Set R)
Tactic: refine IsLocalization.coeSubmodule_mono _ hJM ⟨c, ?_, 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
hc : (algebraMap R A : (a : R) → A) c = a M * v
⊢ c ∈
    (↑(Submodule.comap (Algebra.linearMap R A)
          ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v))) :
      Set R)
have this₁ : a M * v ∈ (↑I : Submodule R A) * (R ∙ v)
Tactic: have := Submodule.mul_mem_mul (ha M hM) (Submodule.mem_span_singleton_self v)
-- 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_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)
⊢ c ∈
    (↑(Submodule.comap (Algebra.linearMap R A)
          ((↑(↑(Units.mkOfMulEqOne I I' hinv') : FractionalIdeal S A) : Submodule R A) * (R ∙ v))) :
      Set R)
have 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)
Tactic: rwa [← hc] at this
Cleared hypotheses: this
-- 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
⊢ False
have hmem : 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
-- 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) (a M * v)
⊢ False
have hmem₁ : 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
Cleared hypotheses: hmem
-- 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) (∑ x ∈ s, u x • (a M * b x))
⊢ False
have rw : ∀ (hmem : Membership.mem (γ := Submodule R A) (IsLocalization.coeSubmodule A M : Submodule R A) (u M • (a M * b M))),
  False
Tactic: rw [← s.add_sum_erase _ hM, Submodule.add_mem_iff_left] at hmem
Cleared hypotheses: hmem
-- 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) (∑ 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
⊢ False
have 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))
Tactic: rw [← s.add_sum_erase _ hM, Submodule.add_mem_iff_left] at hmem
Cleared hypotheses: hmem