-- Mathlib/RingTheory/Smooth/Locus.lean
lemma smoothLocus_comap_of_isLocalization {Af : Type u} [CommRing Af] [Algebra A Af] [Algebra R Af]
    [IsScalarTower R A Af] (f : A) [IsLocalization.Away f Af] :
    PrimeSpectrum.comap (algebraMap A Af) ⁻¹' smoothLocus R A = smoothLocus R Af

Proof state:
case h
R A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
⊢ p ∈ ⇑(PrimeSpectrum.comap (algebraMap A Af)) ⁻¹' smoothLocus R A ↔ p ∈ smoothLocus R Af

Tactic:
let q := PrimeSpectrum.comap (algebraMap A Af) p

Result:
case h
R A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := (PrimeSpectrum.comap (algebraMap A Af)) p
⊢ p ∈ ⇑(PrimeSpectrum.comap (algebraMap A Af)) ⁻¹' smoothLocus R A ↔ p ∈ smoothLocus R Af

Proof state:
case h
R A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := (PrimeSpectrum.comap (algebraMap A Af)) p
⊢ p ∈ ⇑(PrimeSpectrum.comap (algebraMap A Af)) ⁻¹' smoothLocus R A ↔ p ∈ smoothLocus R Af

Tactic:
have : IsLocalization.AtPrime (Localization.AtPrime p.asIdeal) q.asIdeal :=
  IsLocalization.isLocalization_isLocalization_atPrime_isLocalization (.powers f) _ p.asIdeal

Result:
case h
R A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := (PrimeSpectrum.comap (algebraMap A Af)) p
this : IsLocalization.AtPrime (Localization.AtPrime p.asIdeal) q.asIdeal
⊢ p ∈ ⇑(PrimeSpectrum.comap (algebraMap A Af)) ⁻¹' smoothLocus R A ↔ p ∈ smoothLocus R Af

Proof state:
R A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
⊢ ⇑(PrimeSpectrum.comap (algebraMap A Af)) ⁻¹' smoothLocus R A = smoothLocus R Af

Tactic:
ext p

Result:
case h
R A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
⊢ p ∈ ⇑(PrimeSpectrum.comap (algebraMap A Af)) ⁻¹' smoothLocus R A ↔ p ∈ smoothLocus R Af

Proof state:
case h
R A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := (PrimeSpectrum.comap (algebraMap A Af)) p
this : IsLocalization.AtPrime (Localization.AtPrime p.asIdeal) q.asIdeal
⊢ p ∈ ⇑(PrimeSpectrum.comap (algebraMap A Af)) ⁻¹' smoothLocus R A ↔ p ∈ smoothLocus R Af

Tactic:
refine Algebra.FormallySmooth.iff_of_equiv ?_

Result:
case h
R A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := (PrimeSpectrum.comap (algebraMap A Af)) p
this : IsLocalization.AtPrime (Localization.AtPrime p.asIdeal) q.asIdeal
⊢ Localization.AtPrime ((PrimeSpectrum.comap (algebraMap A Af)) p).asIdeal ≃ₐ[R] Localization.AtPrime p.asIdeal

Proof state:
case h
R A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
Af : Type u
inst✝⁴ : CommRing Af
inst✝³ : Algebra A Af
inst✝² : Algebra R Af
inst✝¹ : IsScalarTower R A Af
f : A
inst✝ : IsLocalization.Away f Af
p : PrimeSpectrum Af
q : PrimeSpectrum A := (PrimeSpectrum.comap (algebraMap A Af)) p
this : IsLocalization.AtPrime (Localization.AtPrime p.asIdeal) q.asIdeal
⊢ Localization.AtPrime ((PrimeSpectrum.comap (algebraMap A Af)) p).asIdeal ≃ₐ[R] Localization.AtPrime p.asIdeal

Tactic:
exact (IsLocalization.algEquiv q.asIdeal.primeCompl _ _).restrictScalars R

Result:
no goals