awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : ℕ∞
⊢ projectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)
have coe : projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
  LE.le (α := WithBot ℕ∞)
    (⨆ (p : MaximalSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl))
    (↑⊤ : WithBot ℕ∞)
Tactic: induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : ℕ∞
coe :
  projectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑⊤ : WithBot ℕ∞)
⊢ projectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)
have coe₁ : ∀ (n : ℕ),
  projectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑(↑n : ℕ∞) : WithBot ℕ∞)
Tactic: induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
⊢ projectiveDimension M ≤ N ↔
    ⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
have bot : projectiveDimension M ≤ ⊥ ↔
  LE.le (α := WithBot ℕ∞)
    (⨆ (p : MaximalSpectrum R),
      projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
        (M.localizedModule p.asIdeal.primeCompl))
    ⊥
Tactic: induction N with
  | bot =>
    simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.ProjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
inst_3 : Module.Finite.{u, v} R (↑M : Type v)
aux :
  ∀ (n : ℕ),
    projectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (p : MaximalSpectrum R),
          projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
            (M.localizedModule p.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
bot :
  projectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
⊢ projectiveDimension M ≤ N ↔
    ⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
have coe : ∀ (N : ℕ∞),
  projectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : MaximalSpectrum R),
        projectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)
Tactic: induction N with
  | bot =>
    simp only [le_bot_iff, projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp⟩
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (goal)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
⊢ IsReduced S
have eq_zero : ∀ (x : S), IsNilpotent x → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (goal)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
⊢ x = 0
have eq_zero : ∀ (y : R) (m : ↥M)
  (hx :
    HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑(y, m).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (y, m).1),
  x = 0
Tactic: obtain ⟨⟨y, m⟩, hx⟩ := IsLocalization.surj M x
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (hypothesis)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq.{u_1 + 1} (α := S)
  ((fun (x : S) ↦ x ^ n.succ) (HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S)))
  ((fun (x : S) ↦ x ^ n.succ) ((algebraMap R S : (a : R) → S) y)) :=
  ⋯
⊢ x = 0
have hx'₁ : Eq (α := S) (0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
Tactic: simp only [mul_pow, e, zero_mul, ← map_pow] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (hypothesis)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) (0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
⊢ x = 0
have hx'₁ : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
Tactic: rw [← (algebraMap R S).map_zero] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (goal)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
⊢ x = 0
have eq_zero : ∀ (m' : ↥M) (hm' : (↑m' : R) * 0 = (↑m' : R) * y ^ n.succ), x = 0
Tactic: obtain ⟨m', hm'⟩ := (IsLocalization.eq_iff_exists M S).mp hx'
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (hypothesis)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : (↑m' : R) * 0 = (↑m' : R) * y ^ n.succ
⊢ x = 0
have hm'₁ : (↑m' : R) * 0 * (↑m' : R) ^ n = (↑m' : R) * y ^ n.succ * (↑m' : R) ^ n
Tactic: apply_fun (· * (m' : R) ^ n) at hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (hypothesis)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : (↑m' : R) * 0 * (↑m' : R) ^ n = (↑m' : R) * y ^ n.succ * (↑m' : R) ^ n
⊢ x = 0
have hm'₁ : 0 = (↑m' : R) * (y ^ n.succ * (↑m' : R) ^ n)
Tactic: simp only [mul_assoc, zero_mul, mul_zero] at hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (hypothesis)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : 0 = (↑m' : R) * (y ^ n.succ * (↑m' : R) ^ n)
⊢ x = 0
have hm'₁ : 0 = (y * (↑m' : R)) ^ n.succ
Tactic: rw [← mul_left_comm, ← pow_succ', ← mul_pow] at hm'
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (hypothesis)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : 0 = (y * (↑m' : R)) ^ n.succ
⊢ x = 0
have hm'₁ : y * (↑m' : R) = 0
Tactic: replace hm' := IsNilpotent.eq_zero ⟨_, hm'.symm⟩
Cleared hypotheses: hm'
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (goal)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : y * (↑m' : R) = 0
⊢ x = 0
have eq_zero : ∃ (m : ↥M), (↑m : R) * y = 0
Tactic: rw [← (IsLocalization.map_units S m).mul_left_inj, hx, zero_mul,
    IsLocalization.map_eq_zero_iff M]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (goal)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : y * (↑m' : R) = 0
⊢ (↑m' : R) * y = 0
have rw : (↑m' : R) * y = y * (↑m' : R)
Tactic: rw [← hm', mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (goal)
Goal:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst : Algebra R S
inst_1 : IsLocalization M S
h : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : HMul.hMul (β := S) x ((algebraMap R S : (a : R) → S) (↑m : R) : S) = (algebraMap R S : (a : R) → S) y
hx' : Eq (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) (y ^ n.succ) : S)
m' : ↥M
hm' : y * (↑m' : R) = 0
rw : (↑m' : R) * y = y * (↑m' : R)
⊢ (↑m' : R) * y = 0
have rw₁ : y * (↑m' : R) = y * (↑m' : R)
Tactic: rw [← hm', mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (goal)
Goal:
R : Type u_1
inst : CommRing R
h :
  ∀ (J : Ideal R) (x : J.IsMaximal),
    (fun (R : Type u_1) (x : CommRing R) ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
⊢ IsReduced R
have eq_zero : ∀ (x : R), IsNilpotent x → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (goal)
Goal:
R : Type u_1
inst : CommRing R
h :
  ∀ (J : Ideal R) (x : J.IsMaximal),
    (fun (R : Type u_1) (x : CommRing R) ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
⊢ x = 0
have eq_zero : ∀ (J : Ideal R) (x_1 : J.IsMaximal),
  Eq (α := Localization.AtPrime J)
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x : Localization.AtPrime J)
    (0 : Localization.AtPrime J)
Tactic: apply eq_zero_of_localization
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Reduced (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
h :
  ∀ (J : Ideal R) (x : J.IsMaximal),
    (fun (R : Type u_1) (x : CommRing R) ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
x : R
hx : IsNilpotent x
J : Ideal R
hJ : J.IsMaximal
⊢ Eq (α := Localization.AtPrime J)
    ((algebraMap R (Localization.AtPrime J) : (a : R) → Localization.AtPrime J) x : Localization.AtPrime J)
    (0 : Localization.AtPrime J)
have h₁ : IsReduced.{u_1} (Localization.AtPrime J)
Tactic: specialize h J hJ
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_5 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_3, u_4} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_12 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) M (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) (Mₚ P)
⊢ Module.Finite R M
have have : ∀ (this : Fintype (MaximalSpectrum R)), Module.Finite R M
Tactic: have : Fintype (MaximalSpectrum R) := Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_5 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_3, u_4} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_12 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) M (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
⊢ Module.Finite R M
have choose : ∀ (s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal))
  (hs :
    ∀ (P : MaximalSpectrum R),
      Eq (α := Submodule.{u_3, u_4} (Rₚ P.asIdeal) (Mₚ P.asIdeal))
        (Submodule.span (Rₚ P.asIdeal) (↑(s P) : Set (Mₚ P.asIdeal))) ⊤),
  Module.Finite R M
Tactic: choose s hs using fun P : MaximalSpectrum R ↦ (H P.1).fg_top
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_5 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_3, u_4} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_12 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) M (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs :
  ∀ (P : MaximalSpectrum R),
    Eq (α := Submodule.{u_3, u_4} (Rₚ P.asIdeal) (Mₚ P.asIdeal))
      (Submodule.span (Rₚ P.asIdeal) (↑(s P) : Set (Mₚ P.asIdeal))) ⊤
⊢ Module.Finite R M
have choose : ∀ (frac : (P : MaximalSpectrum R) → (y : Mₚ P.asIdeal) → Prod.{u_2, u_1} M ↥P.asIdeal.primeCompl)
  (hfrac :
    ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal),
      (frac P y).2 • y = (f P.asIdeal : (a : M) → Mₚ P.asIdeal) (frac P y).1),
  Module.Finite R M
Tactic: choose frac hfrac using fun P : MaximalSpectrum R ↦ IsLocalizedModule.surj P.1.primeCompl (f P.1)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_5 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_3, u_4} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_12 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) M (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs :
  ∀ (P : MaximalSpectrum R),
    Eq (α := Submodule.{u_3, u_4} (Rₚ P.asIdeal) (Mₚ P.asIdeal))
      (Submodule.span (Rₚ P.asIdeal) (↑(s P) : Set (Mₚ P.asIdeal))) ⊤
frac : (P : MaximalSpectrum R) → (y : Mₚ P.asIdeal) → Prod.{u_2, u_1} M ↥P.asIdeal.primeCompl
hfrac :
  ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal : (a : M) → Mₚ P.asIdeal) (frac P y).1
⊢ Module.Finite R M
have h : Eq (α := Submodule R M)
  (Submodule.span R
    (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
          Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
      Set M))
  ⊤
Tactic: use Finset.biUnion Finset.univ fun P ↦ Finset.image (frac P · |>.1) (s P)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Semilocal (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
M : Type u_2
inst_2 : AddCommMonoid M
inst_3 : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst_4 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst_5 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Algebra.{u_1, u_3} R (Rₚ P)
inst_6 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalization.AtPrime.{u_1, u_3} (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst_7 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst_8 : (P : Ideal R) → [inst_12 : P.IsMaximal] → Module.{u_1, u_4} R (Mₚ P)
inst_9 : (P : Ideal R) → [inst : P.IsMaximal] → Module.{u_3, u_4} (Rₚ P) (Mₚ P)
inst_10 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsScalarTower.{u_1, u_3, u_4} R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst_12 : P.IsMaximal] → LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id R) M (Mₚ P)
inst_11 : ∀ (P : Ideal R) [inst_12 : P.IsMaximal], IsLocalizedModule (M' := Mₚ P) P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite.{u_3, u_4} (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs :
  ∀ (P : MaximalSpectrum R),
    Eq (α := Submodule.{u_3, u_4} (Rₚ P.asIdeal) (Mₚ P.asIdeal))
      (Submodule.span (Rₚ P.asIdeal) (↑(s P) : Set (Mₚ P.asIdeal))) ⊤
frac : (P : MaximalSpectrum R) → (y : Mₚ P.asIdeal) → Prod.{u_2, u_1} M ↥P.asIdeal.primeCompl
hfrac :
  ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal : (a : M) → Mₚ P.asIdeal) (frac P y).1
⊢ Eq (α := Submodule R M)
    (Submodule.span R
      (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
            Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
        Set M))
    ⊤
have h : ∀ (P : Ideal R) (hP : P.IsMaximal),
  Eq (α := Submodule.{u_3, u_4} (Rₚ P) (Mₚ P))
    (Submodule.localized' (Rₚ P) P.primeCompl (f P)
      (Submodule.span R
        (↑(Finset.biUnion Finset.univ fun (P : MaximalSpectrum R) ↦
              Finset.image (fun (x : Mₚ P.asIdeal) ↦ (frac P x).1) (s P)) :
          Set M)))
    ⊤
Tactic: refine Submodule.eq_top_of_localization_maximal Rₚ Mₚ f _ fun P hP ↦ ?_