awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ injectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
have bot : Subsingleton.{v + 1} (↑M : Type v) ↔
  ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
Tactic: simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
⊢ Subsingleton.{v + 1} (↑M : Type v) ↔
    ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
have bot : ∀ (h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))),
  Subsingleton.{v + 1} (↑M : Type v)
Tactic: refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
h : ∀ (i : MaximalSpectrum R), Subsingleton (LocalizedModule.{u, v} i.asIdeal.primeCompl (↑M : Type v))
⊢ Subsingleton.{v + 1} (↑M : Type v)
have bot : ∀ (P : Ideal R) [inst_3 : P.IsMaximal], Subsingleton (LocalizedModule.{u, v} P.primeCompl (↑M : Type v))
Tactic: apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : ℕ∞
⊢ injectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)
have coe : injectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
  LE.le (α := WithBot ℕ∞)
    (⨆ (p : MaximalSpectrum R),
      injectiveDimension (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.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : ℕ∞
coe :
  injectiveDimension M ≤ (↑⊤ : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      (↑⊤ : WithBot ℕ∞)
⊢ injectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      (↑N : WithBot ℕ∞)
have coe₁ : ∀ (n : ℕ),
  injectiveDimension M ≤ (↑(↑n : ℕ∞) : WithBot ℕ∞) ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        injectiveDimension (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.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
⊢ injectiveDimension M ≤ N ↔
    ⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
have bot : injectiveDimension M ≤ ⊥ ↔
  LE.le (α := WithBot ℕ∞)
    (⨆ (p : MaximalSpectrum R),
      injectiveDimension (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, injectiveDimension_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.InjectiveDimension (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
inst_2 : IsNoetherianRing R
M : ModuleCat.{v, u} R
aux :
  ∀ (n : ℕ),
    injectiveDimension M ≤ (↑n : WithBot ℕ∞) ↔
      LE.le (α := WithBot ℕ∞)
        (⨆ (m : MaximalSpectrum R),
          injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) m.asIdeal.primeCompl))
            (M.localizedModule m.asIdeal.primeCompl))
        (↑n : WithBot ℕ∞)
N : WithBot ℕ∞
bot :
  injectiveDimension M ≤ ⊥ ↔
    LE.le (α := WithBot ℕ∞)
      (⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl))
      ⊥
⊢ injectiveDimension M ≤ N ↔
    ⨆ (p : MaximalSpectrum R),
        injectiveDimension (C := ModuleCat.{v, u} (Localization (M := R) p.asIdeal.primeCompl))
          (M.localizedModule p.asIdeal.primeCompl) ≤
      N
have coe : ∀ (N : ℕ∞),
  injectiveDimension M ≤ (↑N : WithBot ℕ∞) ↔
    ⨆ (p : MaximalSpectrum R),
        injectiveDimension (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, injectiveDimension_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.IntegrallyClosed (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
⊢ IsIntegrallyClosed.{u_2} ↥(⨅ (i : ι), S i)
have refine : ∀ {x : K} (hx : IsIntegral (↥(⨅ (i : ι), S i)) x) (i : ι), x ∈ S i
Tactic: refine (isIntegrallyClosed_iff K).mpr (fun {x} hx ↦ CanLift.prf x (Algebra.mem_iInf.mpr ?_))
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
x : K
hx : IsIntegral (↥(⨅ (i : ι), S i)) x
i : ι
⊢ x ∈ S i
have le : ⨅ (i : ι), S i ≤ S i
Tactic: have le : (⨅ i : ι, S i : Subalgebra R K) ≤ S i := iInf_le S i
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
x : K
hx : IsIntegral (↥(⨅ (i : ι), S i)) x
i : ι
le : ⨅ (i : ι), S i ≤ S i
algInst : Algebra ↥(⨅ (i : ι), S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
⊢ x ∈ S i
have this : IsScalarTower (↥(⨅ (i : ι), S i)) (↥(S i)) K
Tactic: have : IsScalarTower ↥(⨅ i, S i) (S i) K := Subalgebra.inclusion.isScalarTower_right le K
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
x : K
hx : IsIntegral (↥(⨅ (i : ι), S i)) x
i : ι
le : ⨅ (i : ι), S i ≤ S i
algInst : Algebra ↥(⨅ (i : ι), S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
this : IsScalarTower (↥(⨅ (i : ι), S i)) (↥(S i)) K
⊢ x ∈ S i
have rcases : ∀ (val : K) (hin : val ∈ S i)
  (hy : (algebraMap (↥(S i)) K : (a : ↥(S i)) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ S i) val hin) = x), x ∈ S i
Tactic: rcases (isIntegrallyClosed_iff K).mp (h i) hx.tower_top with ⟨⟨_, hin⟩, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
K : Type u_2
inst : CommRing R
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
ι : Type u_3
S : ι → Subalgebra R K
h : ∀ (i : ι), IsIntegrallyClosed.{u_2} ↥(S i)
x : K
hx : IsIntegral (↥(⨅ (i : ι), S i)) x
i : ι
le : ⨅ (i : ι), S i ≤ S i
algInst : Algebra ↥(⨅ (i : ι), S i) ↥(S i) := (Subalgebra.inclusion le).toAlgebra
this : IsScalarTower (↥(⨅ (i : ι), S i)) (↥(S i)) K
val : K
hin : val ∈ S i
hy : (algebraMap (↥(S i)) K : (a : ↥(S i)) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ S i) val hin) = x
⊢ x ∈ S i
have rwa : Membership.mem (α := K) (S i)
  ((algebraMap (↥(S i)) K : (a : ↥(S i)) → K) (Subtype.mk (p := fun (x : K) ↦ x ∈ S i) val hin) : K)
Tactic: rwa [← hy]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Set (PrimeSpectrum R)
h : ∀ p ∈ S, IsIntegrallyClosed.{u_1} (Localization.AtPrime p.asIdeal)
hs : Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R)) (⨅ p ∈ S, subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯) ⊥
⊢ IsIntegrallyClosed R
have apply : Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
  (⨅ (i : (↑S : Type u_1)), subalgebra (FractionRing R) (↑i : PrimeSpectrum R).asIdeal.primeCompl sorry) ⊥
Tactic: apply IsIntegrallyClosed.of_localization_submonoid (fun p : S ↦ p.1.1.primeCompl)
    (fun p ↦ p.1.1.primeCompl_le_nonZeroDivisors) (fun p ↦ h p.1 p.2)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
S : Set (PrimeSpectrum R)
h : ∀ p ∈ S, IsIntegrallyClosed.{u_1} (Localization.AtPrime p.asIdeal)
hs : Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R)) (⨅ p ∈ S, subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯) ⊥
⊢ Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (i : (↑S : Type u_1)), subalgebra (FractionRing R) (↑i : PrimeSpectrum R).asIdeal.primeCompl ⋯) ⊥
have h₁ : ∀ (x : FractionRing R),
  Membership.mem (γ := Subalgebra R (FractionRing R))
      (⨅ (i : (↑S : Type u_1)), subalgebra (FractionRing R) (↑i : PrimeSpectrum R).asIdeal.primeCompl sorry) x ↔
    Membership.mem (γ := Subalgebra R (FractionRing R)) ⊥ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
⊢ IsIntegrallyClosed R
have pos : ∀ (hf : IsField R), IsIntegrallyClosed R
Tactic: by_cases hf : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
pos : ∀ (hf : IsField R), IsIntegrallyClosed R
⊢ IsIntegrallyClosed R
have neg : ∀ (hf : ¬IsField R), IsIntegrallyClosed R
Tactic: by_cases hf : IsField R
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
⊢ IsIntegrallyClosed R
have neg : ∀ (x : PrimeSpectrum R),
  Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range MaximalSpectrum.toPrimeSpectrum) x →
    IsIntegrallyClosed.{u_1} (Localization.AtPrime x.asIdeal)
Tactic: refine of_localization (.range MaximalSpectrum.toPrimeSpectrum) (fun _ ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
neg :
  ∀ (x : PrimeSpectrum R),
    Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range MaximalSpectrum.toPrimeSpectrum) x →
      IsIntegrallyClosed.{u_1} (Localization.AtPrime x.asIdeal)
⊢ IsIntegrallyClosed R
have neg₁ : Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
  (⨅ (p : PrimeSpectrum R),
    ⨅ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range MaximalSpectrum.toPrimeSpectrum) p),
      subalgebra (FractionRing R) p.asIdeal.primeCompl sorry)
  ⊥
Tactic: refine of_localization (.range MaximalSpectrum.toPrimeSpectrum) (fun _ ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
⊢ Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (p : PrimeSpectrum R),
      ⨅ (_ : Membership.mem (γ := Set (PrimeSpectrum R)) (Set.range MaximalSpectrum.toPrimeSpectrum) p),
        subalgebra (FractionRing R) p.asIdeal.primeCompl ⋯)
    ⊥
have neg : Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
  (⨅ (i : MaximalSpectrum R), subalgebra (FractionRing R) i.toPrimeSpectrum.asIdeal.primeCompl sorry) ⊥
Tactic: rw [iInf_range]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
⊢ Eq.{u_1 + 1} (α := Subalgebra R (FractionRing R))
    (⨅ (i : MaximalSpectrum R), subalgebra (FractionRing R) i.toPrimeSpectrum.asIdeal.primeCompl ⋯) ⊥
have h₁ : ∀ (x : MaximalSpectrum R),
  Eq (α := Subalgebra R (FractionRing R))
    (subalgebra (FractionRing R) x.toPrimeSpectrum.asIdeal.primeCompl sorry : Subalgebra R (FractionRing R))
    (subalgebra.ofField (FractionRing R) x.asIdeal.primeCompl sorry : Subalgebra R (FractionRing R))
Tactic: convert! MaximalSpectrum.iInf_localization_eq_bot R (FractionRing R)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
x : MaximalSpectrum R
⊢ Eq (α := Subalgebra R (FractionRing R))
    (subalgebra (FractionRing R) x.toPrimeSpectrum.asIdeal.primeCompl ⋯ : Subalgebra R (FractionRing R))
    (subalgebra.ofField (FractionRing R) x.asIdeal.primeCompl ⋯ : Subalgebra R (FractionRing R))
have h₁ : Eq (α := Subalgebra R (FractionRing R)) (subalgebra (FractionRing R) x.toPrimeSpectrum.asIdeal.primeCompl sorry)
  (subalgebra (FractionRing R) x.asIdeal.primeCompl sorry)
Tactic: rw [subalgebra.ofField_eq, MaximalSpectrum.toPrimeSpectrum]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
h : ∀ (p : Ideal R), p ≠ ⊥ → ∀ [inst_2 : p.IsMaximal], IsIntegrallyClosed.{u_1} (Localization.AtPrime p)
hf : ¬IsField R
x : MaximalSpectrum R
h₁ :
  Eq (α := Subalgebra R (FractionRing R)) (subalgebra (FractionRing R) x.toPrimeSpectrum.asIdeal.primeCompl ⋯)
    (subalgebra (FractionRing R) x.asIdeal.primeCompl ⋯)
⊢ Eq (α := Subalgebra R (FractionRing R))
    (subalgebra (FractionRing R) x.toPrimeSpectrum.asIdeal.primeCompl ⋯ : Subalgebra R (FractionRing R))
    (subalgebra.ofField (FractionRing R) x.asIdeal.primeCompl ⋯ : Subalgebra R (FractionRing R))
have h₂ : Eq (α := Subalgebra R (FractionRing R))
  (subalgebra (FractionRing R) { asIdeal := x.asIdeal, isPrime := sorry }.asIdeal.primeCompl sorry)
  (subalgebra (FractionRing R) x.asIdeal.primeCompl sorry)
Tactic: rw [subalgebra.ofField_eq, MaximalSpectrum.toPrimeSpectrum]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
⊢ Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{uM', uM} (Module.rank R M)
have a : Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
  Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))
Tactic: apply Cardinal.lift_injective.{max uM' uR'}
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (hypothesis)
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))
have this : Nontrivial R
Tactic: have := (algebraMap R Rₛ).domain_nontrivial
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (hypothesis)
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
this : Nontrivial R
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))
have this₁ : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) =
  Cardinal.lift.{uM', max uM uR'} (Module.rank Rₛ (TensorProduct R Rₛ M))
Tactic: have := (IsLocalizedModule.isBaseChange S Rₛ f).equiv.lift_rank_eq.symm
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
this_1 : Nontrivial R
this :
  Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) =
    Cardinal.lift.{uM', max uM uR'} (Module.rank Rₛ (TensorProduct R Rₛ M))
⊢ Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM, uM'} (Module.rank Rₛ Mₛ)) =
    Cardinal.lift.{max uM' uR', max uM uM'} (Cardinal.lift.{uM', uM} (Module.rank R M))
have a : ∀ (this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)),
  Cardinal.lift.{max uM uM' uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uM' uR', uM} (Module.rank R M)
Tactic: simp only [rank_tensorProduct, rank_self,
    Cardinal.lift_one, one_mul, Cardinal.lift_lift] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
Goal:
R : Type u_1
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Rₛ : Type uR'
Mₛ : Type uM'
inst_3 : AddCommGroup Mₛ
inst_4 : Module R Mₛ
inst_5 : CommRing Rₛ
inst_6 : Algebra R Rₛ
inst_7 : Module Rₛ Mₛ
inst_8 : IsScalarTower R Rₛ Mₛ
S : Submonoid R
f : M →ₗ[R] Mₛ
inst_9 : IsLocalization S Rₛ
inst_10 : IsLocalizedModule S f
inst_11 : Free R M
inst_12 : Nontrivial Rₛ
this_1 : Nontrivial R
this : Cardinal.lift.{max uM uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uR' uM', uM} (Module.rank R M)
⊢ Cardinal.lift.{max uM uM' uR', uM'} (Module.rank Rₛ Mₛ) = Cardinal.lift.{max uM' uR', uM} (Module.rank R M)
have h : Cardinal.lift.{max uM uM' uR', uM'} = Cardinal.lift.{max uM uR', uM'}
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Projective (goal)
Goal:
R : Type u_1
N : Type u_2
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
inst_5 : Module.FinitePresentation R N
H :
  ∀ (I : Ideal R) (x : I.IsMaximal),
    ∃ (g :
      LinearMap (R := Localization.AtPrime I) (RingHom.id (Localization.AtPrime I)) (LocalizedModule I.primeCompl N)
        (LocalizedModule I.primeCompl M)),
      (LocalizedModule.map I.primeCompl :
              (a : M →ₗ[R] N) →
                LocalizedModule I.primeCompl M →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N)
            f ∘ₗ
          g =
        id
⊢ ∃ (g : N →ₗ[R] M), f ∘ₗ g = id
have change : Membership.mem (γ := Submodule R (N →ₗ[R] N))
  (range (R := R) (M := N →ₗ[R] M) (τ₁₂ := RingHom.id R)
    ((llcomp R N M N : (a : M →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] N →ₗ[R] N) f))
  id
Tactic: change LinearMap.id ∈ LinearMap.range (LinearMap.llcomp R N M N f)