-- Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
lemma comap_freeLocus_le {A} [CommRing A] [Algebra R A] :
    comap (algebraMap R A) ⁻¹' freeLocus R M ≤ freeLocus A (A ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : p ∈ ⇑(comap (algebraMap R A)) ⁻¹' freeLocus R M
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)

Tactic:
let Aₚ := Localization.AtPrime p.asIdeal

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : p ∈ ⇑(comap (algebraMap R A)) ⁻¹' freeLocus R M
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  (Localization.localRingHom ((comap (algebraMap R A)) p).asIdeal p.asIdeal (algebraMap R A) ⋯).toAlgebra
this : IsScalarTower R Rₚ Aₚ
⊢ Free Aₚ (Aₚ ⊗[A] A ⊗[R] M)

Tactic:
let e := AlgebraTensorModule.cancelBaseChange R Rₚ Aₚ Aₚ M ≪≫ₗ
  (AlgebraTensorModule.cancelBaseChange R A Aₚ Aₚ M).symm

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  (Localization.localRingHom ((comap (algebraMap R A)) p).asIdeal p.asIdeal (algebraMap R A) ⋯).toAlgebra
this : IsScalarTower R Rₚ Aₚ
e : Aₚ ⊗[Rₚ] Rₚ ⊗[R] M ≃ₗ[Aₚ] Aₚ ⊗[A] A ⊗[R] M :=
  AlgebraTensorModule.cancelBaseChange R Rₚ Aₚ Aₚ M ≪≫ₗ (AlgebraTensorModule.cancelBaseChange R A Aₚ Aₚ M).symm
⊢ Free Aₚ (Aₚ ⊗[A] A ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : p ∈ ⇑(comap (algebraMap R A)) ⁻¹' freeLocus R M
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)

Tactic:
rw [Set.mem_preimage, mem_freeLocus_iff_tensor _ Rₚ] at hp

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ Free Aₚ (Aₚ ⊗[A] A ⊗[R] M)

Tactic:
letI algebra : Algebra Rₚ Aₚ := (Localization.localRingHom
  (comap (algebraMap R A) p).asIdeal p.asIdeal (algebraMap R A) rfl).toAlgebra

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  (Localization.localRingHom ((comap (algebraMap R A)) p).asIdeal p.asIdeal (algebraMap R A) ⋯).toAlgebra
⊢ Free Aₚ (Aₚ ⊗[A] A ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ ⇑(comap (algebraMap R A)) ⁻¹' freeLocus R M ≤ freeLocus A (A ⊗[R] M)

Tactic:
intro p hp

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : p ∈ ⇑(comap (algebraMap R A)) ⁻¹' freeLocus R M
⊢ p ∈ freeLocus A (A ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  (Localization.localRingHom ((comap (algebraMap R A)) p).asIdeal p.asIdeal (algebraMap R A) ⋯).toAlgebra
⊢ algebraMap R Aₚ = (algebraMap Rₚ Aₚ).comp (algebraMap R Rₚ)

Tactic:
simp [Rₚ, Aₚ, algebra, RingHom.algebraMap_toAlgebra, Localization.localRingHom,
← IsScalarTower.algebraMap_eq]

Result:
no goals

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)

Tactic:
rw [mem_freeLocus_iff_tensor _ Aₚ]

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ Free Aₚ (Aₚ ⊗[A] A ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  (Localization.localRingHom ((comap (algebraMap R A)) p).asIdeal p.asIdeal (algebraMap R A) ⋯).toAlgebra
⊢ Free Aₚ (Aₚ ⊗[A] A ⊗[R] M)

Tactic:
have : IsScalarTower R Rₚ Aₚ := IsScalarTower.of_algebraMap_eq'
  (by simp [Rₚ, Aₚ, algebra, RingHom.algebraMap_toAlgebra, Localization.localRingHom,
      ← IsScalarTower.algebraMap_eq])

Result:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  (Localization.localRingHom ((comap (algebraMap R A)) p).asIdeal p.asIdeal (algebraMap R A) ⋯).toAlgebra
this : IsScalarTower R Rₚ Aₚ
⊢ Free Aₚ (Aₚ ⊗[A] A ⊗[R] M)

Proof state:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
Rₚ : Type uR := Localization.AtPrime ((comap (algebraMap R A)) p).asIdeal
hp : Free Rₚ (Rₚ ⊗[R] M)
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
algebra : Algebra Rₚ Aₚ :=
  (Localization.localRingHom ((comap (algebraMap R A)) p).asIdeal p.asIdeal (algebraMap R A) ⋯).toAlgebra
this : IsScalarTower R Rₚ Aₚ
e : Aₚ ⊗[Rₚ] Rₚ ⊗[R] M ≃ₗ[Aₚ] Aₚ ⊗[A] A ⊗[R] M :=
  AlgebraTensorModule.cancelBaseChange R Rₚ Aₚ Aₚ M ≪≫ₗ (AlgebraTensorModule.cancelBaseChange R A Aₚ Aₚ M).symm
⊢ Free Aₚ (Aₚ ⊗[A] A ⊗[R] M)

Tactic:
exact .of_equiv e

Result:
no goals