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

Goal state before:
pp: case refine_1
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ ↑I = 0

Tactic:
;

Goal state after:
case refine_1
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
hx' : ↑I = spanSingleton R⁰ x
x_eq : x = 0
⊢ ↑I = 0
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R

pp: case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1

Tactic:
;

Goal state after:
case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R

case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1

pp: case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R

Tactic:
;

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1

case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
a✝ : IsPrincipalIdealRing R
⊢ Fintype.card (ClassGroup R) = 1

Tactic:
;

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
a✝ : IsPrincipalIdealRing R
⊢ Fintype.card (ClassGroup R) = 1
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
I✝ : ClassGroup R
hI✝ : ∀ (y : ClassGroup R), y = I✝
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : I = ⊥
⊢ Submodule.IsPrincipal ⊥

Tactic:
;

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
I✝ : ClassGroup R
hI✝ : ∀ (y : ClassGroup R), y = I✝
eq_one : ∀ (J : ClassGroup R), J = 1
I : Ideal R
hI : I = ⊥
⊢ Submodule.IsPrincipal ⊥
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (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_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (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 : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : Rₚ P ≃+* Localization.AtPrime P :=
  (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
⊢ ∀ (m : Rₚ P) (x : Mₚ P),
    (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun (m • x) =
      ↑e m • (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun x

Tactic:
intro r

Goal state after:
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (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_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (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 : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
hP : P.IsMaximal
e : Rₚ P ≃+* Localization.AtPrime P :=
  (IsLocalization.algEquiv P.primeCompl (Rₚ P) (Localization.AtPrime P)).toRingEquiv
r : Rₚ P
⊢ ∀ (x : Mₚ P),
    (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun (r • x) =
      ↑e r • (↑(IsLocalizedModule.linearEquiv P.primeCompl (f P) (LocalizedModule.mkLinearMap P.primeCompl M))).toFun x
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous[inst✝¹, inst✝] f
s : Set Z
⊢ IsOpen[inst✝¹] (g ∘ f ⁻¹' s)

Tactic:
rw [Set.preimage_comp]
  exact hf.isOpen_preimage _ (hg _)

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ (range f).Finite

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
this : TopologicalSpace Y := ⊥
⊢ (range f).Finite
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
toFun✝¹ : X → Y
isLocallyConstant✝¹ : IsLocallyConstant toFun✝¹
toFun✝ : X → Y
isLocallyConstant✝ : IsLocallyConstant toFun✝
a✝ :
  { toFun := toFun✝¹, isLocallyConstant := isLocallyConstant✝¹ }.toFun =
    { toFun := toFun✝, isLocallyConstant := isLocallyConstant✝ }.toFun
⊢ { toFun := toFun✝¹, isLocallyConstant := isLocallyConstant✝¹ } =
    { toFun := toFun✝, isLocallyConstant := isLocallyConstant✝ }

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
toFun✝¹ : X → Y
isLocallyConstant✝¹ : IsLocallyConstant toFun✝¹
toFun✝ : X → Y
isLocallyConstant✝ : IsLocallyConstant toFun✝
a✝ :
  { toFun := toFun✝¹, isLocallyConstant := isLocallyConstant✝¹ }.toFun =
    { toFun := toFun✝, isLocallyConstant := isLocallyConstant✝ }.toFun
⊢ { toFun := toFun✝¹, isLocallyConstant := isLocallyConstant✝¹ } =
    { toFun := toFun✝, isLocallyConstant := isLocallyConstant✝ }
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
x✝ : X
⊢ x✝ ∈ (fun x a ↦ (f a) x) ⁻¹' {g} ↔ x✝ ∈ ⋂ a, ⇑(f a) ⁻¹' {g a}

Tactic:
;

Goal state after:
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
x✝ : X
⊢ x✝ ∈ (fun x a ↦ (f a) x) ⁻¹' {g} ↔ x✝ ∈ ⋂ a, ⇑(f a) ⁻¹' {g a}
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ (comap f x✝¹) x✝ = (const X (x✝¹ y)) x✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
x✝¹ : LocallyConstant Y Z
x✝ : X
⊢ (comap f x✝¹) x✝ = (const X (x✝¹ y)) x✝
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝ : LocallyConstant X Y
⊢ map (⇑e.symm) (map (⇑e) x✝) = x✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝ : LocallyConstant X Y
⊢ map (⇑e.symm) (map (⇑e) x✝) = x✝
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝¹ : LocallyConstant X Y
x✝ : X
⊢ (map (⇑e.symm) (map (⇑e) x✝¹)) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝¹ : LocallyConstant X Y
x✝ : X
⊢ (map (⇑e.symm) (map (⇑e) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝ : LocallyConstant X Z
⊢ map (⇑e) (map (⇑e.symm) x✝) = x✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝ : LocallyConstant X Z
⊢ map (⇑e) (map (⇑e.symm) x✝) = x✝
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝¹ : LocallyConstant X Z
x✝ : X
⊢ (map (⇑e) (map (⇑e.symm) x✝¹)) x✝ = x✝¹ x✝

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
x✝¹ : LocallyConstant X Z
x✝ : X
⊢ (map (⇑e) (map (⇑e.symm) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case refine_2.true
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
⊢ Continuous[instTopologicalSpaceSubtype, dZ]
    ((bif true then C₁ else C₂).domRestrict fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩)

Tactic:
· simp only [cond_true, domRestrict_dite, Subtype.coe_eta]
        exact hf

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst✝⁵ : (i : ι) → AddCommMonoid (N i)
inst✝⁴ : (i : ι) → Module R (N i)
P : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (P i)
inst✝² : (i : ι) → Module R (P i)
inst✝¹ : (i : ι) → Module S (P i)
inst✝ : ∀ (i : ι), IsScalarTower R S (P i)
ε : (i : ι) → N i →ₗ[R] P i
ibc : ∀ (i : ι), IsBaseChange S (ε i)
x✝ : ⨁ (i : ι), N i
⊢ (directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ ⋯.equiv) (1 ⊗ₜ[R] x✝) = (lmap ε) x✝

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst✝⁵ : (i : ι) → AddCommMonoid (N i)
inst✝⁴ : (i : ι) → Module R (N i)
P : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (P i)
inst✝² : (i : ι) → Module R (P i)
inst✝¹ : (i : ι) → Module S (P i)
inst✝ : ∀ (i : ι), IsScalarTower R S (P i)
ε : (i : ι) → N i →ₗ[R] P i
ibc : ∀ (i : ι), IsBaseChange S (ε i)
x✝ : ⨁ (i : ι), N i
⊢ (directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ ⋯.equiv) (1 ⊗ₜ[R] x✝) = (lmap ε) x✝
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
e : Localization.AtPrime p.asIdeal ≃+* Rₚ :=
  (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
⊢ ∀ (m : Localization.AtPrime p.asIdeal) (x : LocalizedModule p.asIdeal.primeCompl M),
    (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f)).toFun (m • x) =
      ↑e m • (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f)).toFun x

Tactic:
intro r

Goal state after:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
e : Localization.AtPrime p.asIdeal ≃+* Rₚ :=
  (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
r : Localization.AtPrime p.asIdeal
⊢ ∀ (x : LocalizedModule p.asIdeal.primeCompl M),
    (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f)).toFun (r • x) =
      ↑e r • (↑(IsLocalizedModule.iso p.asIdeal.primeCompl f)).toFun x
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : ↑(comap (algebraMap R S) ⁻¹' {p})
x : S
⊢ x ∈
      (↑((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩)
            ((fun q ↦
                {
                  asIdeal :=
                    RingHom.ker
                      (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                          (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
                  isPrime := ⋯ })
              q))).asIdeal ↔
    x ∈ (↑q).asIdeal

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : ↑(comap (algebraMap R S) ⁻¹' {p})
x : S
⊢ x ∈
      (↑((fun q ↦ ⟨comap includeRight.toRingHom q, ⋯⟩)
            ((fun q ↦
                {
                  asIdeal :=
                    RingHom.ker
                      (Algebra.TensorProduct.lift (Ideal.ResidueField.mapₐ p.asIdeal (↑q).asIdeal (ofId R S) ⋯)
                          (IsScalarTower.toAlgHom R S (↑q).asIdeal.ResidueField) ⋯).toRingHom,
                  isPrime := ⋯ })
              q))).asIdeal ↔
    x ∈ (↑q).asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝¹ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝ : IsScalarTower R (Localization S) Rₚ
this : IsLocalization (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl) Rₚ
x : R
hx : x ∈ ↑p'.primeCompl
⊢ (algebraMap R (Localization S)) x ∈ p.asIdeal.primeCompl

Tactic:
;

Goal state after:
case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝¹ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝ : IsScalarTower R (Localization S) Rₚ
this : IsLocalization (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl) Rₚ
x : R
hx : x ∈ ↑p'.primeCompl
⊢ (algebraMap R (Localization S)) x ∈ p.asIdeal.primeCompl
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝² : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝¹ : IsScalarTower R (Localization S) Rₚ
this✝ : IsLocalization.AtPrime Rₚ p.asIdeal
this : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
r : R
r' : Localization S
m : Mₚ
⊢ r •
      (algebraMap (Localization S) (Localization.AtPrime (Ideal.comap (algebraMap R (Localization S)) p.asIdeal))) r' •
        m =
    r • r' • m

Tactic:
;

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝² : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝¹ : IsScalarTower R (Localization S) Rₚ
this✝ : IsLocalization.AtPrime Rₚ p.asIdeal
this : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
r : R
r' : Localization S
m : Mₚ
⊢ r •
      (algebraMap (Localization S) (Localization.AtPrime (Ideal.comap (algebraMap R (Localization S)) p.asIdeal))) r' •
        m =
    r • r' • m
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝³ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝² : IsScalarTower R (Localization S) Rₚ
this✝¹ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this : IsScalarTower R (Localization S) Mₚ
r : Localization S
r' : Rₚ
m : Mₚ
⊢ (r • r') • m = (algebraMap (Localization S) Rₚ) r • r' • m

Tactic:
← mul_smul,

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝³ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝² : IsScalarTower R (Localization S) Rₚ
this✝¹ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this : IsScalarTower R (Localization S) Mₚ
r : Localization S
r' : Rₚ
m : Mₚ
⊢ (r • r') • m = ((algebraMap (Localization S) Rₚ) r * r') • m
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁶ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝⁵ : IsScalarTower R (Localization S) Rₚ
this✝⁴ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝³ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝² : IsScalarTower R (Localization S) Mₚ
this✝¹ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this✝ : IsLocalizedModule p'.primeCompl (↑R l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l
x : R
hx : x ∈ ↑p'.primeCompl
⊢ (algebraMap R (Localization S)) x ∈ p.asIdeal.primeCompl

Tactic:
;

Goal state after:
case h
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝⁶ : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝⁵ : IsScalarTower R (Localization S) Rₚ
this✝⁴ : IsLocalization.AtPrime Rₚ p.asIdeal
this✝³ : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
this✝² : IsScalarTower R (Localization S) Mₚ
this✝¹ : IsScalarTower (Localization S) Rₚ Mₚ
l : LocalizedModule S M →ₗ[Localization S] LocalizedModule p'.primeCompl M :=
  LinearMap.extendScalarsOfIsLocalization S (Localization S)
    (IsLocalizedModule.liftOfLE S p'.primeCompl hp' (LocalizedModule.mkLinearMap S M)
      (LocalizedModule.mkLinearMap p'.primeCompl M))
this✝ : IsLocalizedModule p'.primeCompl (↑R l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l
x : R
hx : x ∈ ↑p'.primeCompl
⊢ (algebraMap R (Localization S)) x ∈ p.asIdeal.primeCompl