mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
⊢ ∀ x ∈ ⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)},
    ∀ y ∈ {g | IsStandardOpenImmersion S (Localization.Away g)},
      x * y ∈ ↑(Ideal.span (Set.range fun i ↦ (algebraMap S T) ↑i.fst * ↑i.snd))

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
⊢ ∀ x ∈ ⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)},
    ∀ y ∈ {g | IsStandardOpenImmersion S (Localization.Away g)},
      x * y ∈ ↑(Ideal.span (Set.range fun i ↦ (algebraMap S T) ↑i.fst * ↑i.snd))
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
X : ModuleCat R
inj : Module.Injective R ↑X
x✝ : Small.{v, u} (Localization S) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Injective (Localization S) ↑((localizedModuleFunctor S).1 X)

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
X : ModuleCat R
inj : Module.Injective R ↑X
x✝ : Small.{v, u} (Localization S) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Injective (Localization S) ↑((localizedModuleFunctor S).1 X)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M 0
injle : Module.Injective R ↑M
⊢ Module.Injective (Localization S) ↑(M.localizedModule S)

Tactic:
]

Goal state after:
case zero
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
S : Submonoid R
this : Small.{v, u} (Localization S)
M : ModuleCat R
inst✝ : HasInjectiveDimensionLE M 0
injle : Module.Injective R ↑M
⊢ Module.Injective (Localization S) ↑(M.localizedModule S)
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝³ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this✝² : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
this✝¹ : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this✝ : IsScalarTower S (Localization.Away x) (T'' g x)
this :
  algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g) =
    algebraMapSubmonoid (Localization.Away x) (Submonoid.powers ((algebraMap S T) g))
⊢ IsLocalization (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers ((algebraMap S T) g))) (T'' g x)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalIso R S
inst✝ : IsLocalIso S T
s : Set S := {g | IsStandardOpenImmersion R (Localization.Away g)}
T' : S → Type u_3 := fun g ↦ Localization.Away ((algebraMap S T) g)
this✝³ : (g : S) → Algebra (Localization.Away g) (T' g) := fun g ↦ localizationAlgebra (Submonoid.powers g) T
T'' : S → T → Type u_3 := fun g x ↦ Localization.Away ((algebraMap T (T' g)) x)
t : S → Set T := fun g ↦ {x | IsStandardOpenImmersion (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : ↑s) × ↑(t ↑i)
this✝² : ∀ (i : ι), IsStandardOpenImmersion (Localization.Away ↑i.fst) (T'' ↑i.fst ↑i.snd)
h1 : Ideal.span (⇑(algebraMap S T) '' {g | IsStandardOpenImmersion R (Localization.Away g)}) = ⊤
g : S
hg : IsStandardOpenImmersion R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion S (Localization.Away x)
this✝¹ : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this✝ : IsScalarTower S (Localization.Away x) (T'' g x)
this :
  algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g) =
    algebraMapSubmonoid (Localization.Away x) (Submonoid.powers ((algebraMap S T) g))
⊢ IsLocalization (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers ((algebraMap S T) g))) (T'' g x)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case zero.refine_1
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : Injective M
m : MaximalSpectrum R
x✝¹ : Small.{v, u} (Localization m.asIdeal.primeCompl) := small_of_surjective Localization.mkHom_surjective
x✝ : Module.Injective R ↑M := Module.injective_module_of_injective_object R ↑M
⊢ Module.Injective (Localization m.asIdeal.primeCompl) ↑(M.localizedModule m.asIdeal.primeCompl)

Tactic:
]

Goal state after:
case zero.refine_1
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : Injective M
m : MaximalSpectrum R
x✝¹ : Small.{v, u} (Localization m.asIdeal.primeCompl) := small_of_surjective Localization.mkHom_surjective
x✝ : Module.Injective R ↑M := Module.injective_module_of_injective_object R ↑M
⊢ Module.Injective (Localization m.asIdeal.primeCompl) ↑(M.localizedModule m.asIdeal.primeCompl)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case zero.refine_2
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
⊢ Module.Injective R ↑M

Tactic:
]

Goal state after:
case zero.refine_2
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
⊢ Module.Injective R ↑M
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this✝ : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
this : Module.Baer (Localization.AtPrime p) ↑(M.localizedModule p.primeCompl)
⊢ Module.Baer (Localization.AtPrime p) (LocalizedModule p.primeCompl ↑M)

Tactic:
]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this✝ : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
this : Module.Baer (Localization.AtPrime p) ↑(M.localizedModule p.primeCompl)
⊢ Module.Baer (Localization.AtPrime p) (LocalizedModule p.primeCompl ↑M)
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalIso R S
⊢ {g | IsStandardOpenImmersion R (Localization.Away g)} ⊆
    ↑(Ideal.comap TensorProduct.includeRight (Ideal.span {g | IsStandardOpenImmersion T (Localization.Away g)}))

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
T : Type u_3
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalIso R S
⊢ {g | IsStandardOpenImmersion R (Localization.Away g)} ⊆
    ↑(Ideal.comap TensorProduct.includeRight (Ideal.span {g | IsStandardOpenImmersion T (Localization.Away g)}))
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization m.asIdeal.primeCompl)) :=
  fun m ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
Sp_exact : ∀ (m : MaximalSpectrum R), (Sp m).ShortExact
ih' :
  HasInjectiveDimensionLT S.X₃ (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLT (S.X₃.localizedModule m.asIdeal.primeCompl) (n + 1)
⊢ (∀ (m : MaximalSpectrum R), HasInjectiveDimensionLT (S.X₃.localizedModule m.asIdeal.primeCompl) (n + 1)) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLT (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)

Tactic:
]

Goal state after:
case succ
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
n : ℕ
ih :
  ∀ (M : ModuleCat R),
    HasInjectiveDimensionLE M n ↔
      ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLE (M.localizedModule m.asIdeal.primeCompl) n
M : ModuleCat R
ei : EnoughInjectives (ModuleCat R)
I : ModuleCat R
inj : Injective I
f : M ⟶ I
monof : Mono f
S : ShortComplex (ModuleCat R) := { X₁ := M, X₂ := I, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
S_exact : S.ShortExact
Sp : (m : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization m.asIdeal.primeCompl)) :=
  fun m ↦ S.map (localizedModuleFunctor m.asIdeal.primeCompl)
Sp_exact : ∀ (m : MaximalSpectrum R), (Sp m).ShortExact
ih' :
  HasInjectiveDimensionLT S.X₃ (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLT (S.X₃.localizedModule m.asIdeal.primeCompl) (n + 1)
⊢ (∀ (m : MaximalSpectrum R), HasInjectiveDimensionLT (S.X₃.localizedModule m.asIdeal.primeCompl) (n + 1)) ↔
    ∀ (m : MaximalSpectrum R), HasInjectiveDimensionLT (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X : ModuleCat R
proj : Module.Projective R ↑X
this : Small.{v, u} (Localization S)
⊢ Module.Projective (Localization S) ↑((localizedModuleFunctor S).1 X)

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
S : Submonoid R
X : ModuleCat R
proj : Module.Projective R ↑X
this : Small.{v, u} (Localization S)
⊢ Module.Projective (Localization S) ↑((localizedModuleFunctor S).1 X)
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
inst✝² : IsInvariant A B G
P Q : Ideal B
inst✝¹ : P.IsPrime
inst✝ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
F : OpenNormalSubgroup G ⥤ Type u :=
  { obj := fun N ↦ { g // Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P },
    map := fun {N N'} f ↦
      ↾fun x ↦ ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩,
    map_id := ⋯, map_comp := ⋯ }
this✝ : ∀ (N : OpenNormalSubgroup G), Nonempty (F.obj N)
s : (j : OpenNormalSubgroup G) → F.obj j
hs : s ∈ F.sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑(s N)
N : OpenNormalSubgroup G
x : ↥(B' ↥↑N.toOpenSubgroup)
hN : ↑N ⊆ ↑(MulAction.stabilizer G ↑x)
⊢ x ∈ ↑(s N) • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P ↔ x ∈ Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) (a • P)

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
inst✝² : IsInvariant A B G
P Q : Ideal B
inst✝¹ : P.IsPrime
inst✝ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
F : OpenNormalSubgroup G ⥤ Type u :=
  { obj := fun N ↦ { g // Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P },
    map := fun {N N'} f ↦
      ↾fun x ↦ ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩,
    map_id := ⋯, map_comp := ⋯ }
this✝ : ∀ (N : OpenNormalSubgroup G), Nonempty (F.obj N)
s : (j : OpenNormalSubgroup G) → F.obj j
hs : s ∈ F.sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑(s N)
N : OpenNormalSubgroup G
x : ↥(B' ↥↑N.toOpenSubgroup)
hN : ↑N ⊆ ↑(MulAction.stabilizer G ↑x)
⊢ x ∈ ↑(s N) • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P ↔ x ∈ Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) (a • P)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization S)
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M 0
projle : Module.Projective R ↑M
⊢ Module.Projective (Localization S) ↑(M.localizedModule S)

Tactic:
]

Goal state after:
case zero
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
S : Submonoid R
this : Small.{v, u} (Localization S)
M : ModuleCat R
inst✝ : HasProjectiveDimensionLE M 0
projle : Module.Projective R ↑M
⊢ Module.Projective (Localization S) ↑(M.localizedModule S)
Module: Mathlib.RingTheory.LocalProperties.Semilocal

Goal state before:
pp: case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
⊢ ↑(s { asIdeal := P, isMaximal := hP }) ⊆
    ↑(Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))))

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Finite (MaximalSpectrum R)
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_3
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (P : Ideal R) [inst : P.IsMaximal], Module.Finite (Rₚ P) (Mₚ P)
this : Fintype (MaximalSpectrum R)
s : (P : MaximalSpectrum R) → Finset (Mₚ P.asIdeal)
hs : ∀ (P : MaximalSpectrum R), Submodule.span (Rₚ P.asIdeal) ↑(s P) = ⊤
frac : (P : MaximalSpectrum R) → Mₚ P.asIdeal → M × ↥P.asIdeal.primeCompl
hfrac : ∀ (P : MaximalSpectrum R) (y : Mₚ P.asIdeal), (frac P y).2 • y = (f P.asIdeal) (frac P y).1
P : Ideal R
hP : P.IsMaximal
⊢ ↑(s { asIdeal := P, isMaximal := hP }) ⊆
    ↑(Submodule.span (Rₚ P) (⇑(f P) '' ↑(Finset.univ.biUnion fun P ↦ Finset.image (fun x ↦ (frac P x).1) (s P))))
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case zero.refine_1
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : Projective M
p : MaximalSpectrum R
this : Small.{v, u} (Localization p.asIdeal.primeCompl) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Projective (Localization p.asIdeal.primeCompl) ↑(M.localizedModule p.asIdeal.primeCompl)

Tactic:
]

Goal state after:
case zero.refine_1
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : Projective M
p : MaximalSpectrum R
this : Small.{v, u} (Localization p.asIdeal.primeCompl) := small_of_surjective Localization.mkHom_surjective
⊢ Module.Projective (Localization p.asIdeal.primeCompl) ↑(M.localizedModule p.asIdeal.primeCompl)
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case zero.refine_2
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)
⊢ Module.Projective R ↑M

Tactic:
]

Goal state after:
case zero.refine_2
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
h : ∀ (m : MaximalSpectrum R), Projective (M.localizedModule m.asIdeal.primeCompl)
⊢ Module.Projective R ↑M
Module: Mathlib.RingTheory.LocalProperties.ProjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
ih :
  HasProjectiveDimensionLT (of R ↥f.ker) (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT ((of R ↥f.ker).localizedModule m.asIdeal.primeCompl) (n + 1)
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
Sp : (p : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization p.asIdeal.primeCompl)) :=
  fun p ↦ S.map (localizedModuleFunctor p.asIdeal.primeCompl)
Sp_exact : ∀ (p : MaximalSpectrum R), (Sp p).ShortExact
projp : ∀ (p : MaximalSpectrum R), Projective (Sp p).X₂
⊢ (∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT ((of R ↥f.ker).localizedModule m.asIdeal.primeCompl) (n + 1)) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)

Tactic:
]

Goal state after:
case succ
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
P : Type v
w✝³ : AddCommGroup P
w✝² : Module R P
w✝¹ : Module.Free R P
w✝ : Module.Finite R P
f : P →ₗ[R] ↑M
ih :
  HasProjectiveDimensionLT (of R ↥f.ker) (n + 1) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT ((of R ↥f.ker).localizedModule m.asIdeal.primeCompl) (n + 1)
surjf : Function.Surjective ⇑f
S : ShortComplex (ModuleCat R) := f.shortComplexKer
S_exact : f.shortComplexKer.ShortExact
proj : Projective S.X₂
Sp : (p : MaximalSpectrum R) → ShortComplex (ModuleCat (Localization p.asIdeal.primeCompl)) :=
  fun p ↦ S.map (localizedModuleFunctor p.asIdeal.primeCompl)
Sp_exact : ∀ (p : MaximalSpectrum R), (Sp p).ShortExact
projp : ∀ (p : MaximalSpectrum R), Projective (Sp p).X₂
⊢ (∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT ((of R ↥f.ker).localizedModule m.asIdeal.primeCompl) (n + 1)) ↔
    ∀ (m : MaximalSpectrum R), HasProjectiveDimensionLT (M.localizedModule m.asIdeal.primeCompl) (n + 1 + 1)