-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma ofLocalizationPrime :
    OfLocalizationPrime FormallyUnramified

Proof state:
⊢ OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] => FormallyUnramified

Tactic:
intros R S _ _ f H

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
⊢ f.FormallyUnramified

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
⊢ x ∈ Algebra.unramifiedLocus R S

Tactic:
let Sₓ := Localization.AtPrime x.asIdeal

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
⊢ x ∈ Algebra.unramifiedLocus R S

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this✝² : Algebra.FormallyUnramified R Rₓ
this✝¹ : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
this✝ : IsScalarTower R Rₓ Sₓ
this : Algebra.FormallyUnramified Rₓ Sₓ
⊢ x ∈ Algebra.unramifiedLocus R S

Tactic:
exact Algebra.FormallyUnramified.comp R Rₓ Sₓ

Result:
no goals

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.FormallyUnramified

Tactic:
rw [FormallyUnramified, ← Algebra.unramifiedLocus_eq_univ_iff, Set.eq_univ_iff_forall]

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (x : PrimeSpectrum S), x ∈ Algebra.unramifiedLocus R S

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this✝ : Algebra.FormallyUnramified R Rₓ
this : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
⊢ x ∈ Algebra.unramifiedLocus R S

Tactic:
have : IsScalarTower R Rₓ Sₓ := .of_algebraMap_eq
  fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this✝¹ : Algebra.FormallyUnramified R Rₓ
this✝ : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
this : IsScalarTower R Rₓ Sₓ
⊢ x ∈ Algebra.unramifiedLocus R S

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this✝¹ : Algebra.FormallyUnramified R Rₓ
this✝ : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
this : IsScalarTower R Rₓ Sₓ
⊢ x ∈ Algebra.unramifiedLocus R S

Tactic:
have : Algebra.FormallyUnramified Rₓ Sₓ := H _ _

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this✝² : Algebra.FormallyUnramified R Rₓ
this✝¹ : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
this✝ : IsScalarTower R Rₓ Sₓ
this : Algebra.FormallyUnramified Rₓ Sₓ
⊢ x ∈ Algebra.unramifiedLocus R S

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
⊢ x ∈ Algebra.unramifiedLocus R S

Tactic:
have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := Rₓ) (x.asIdeal.comap f).primeCompl

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this : Algebra.FormallyUnramified R Rₓ
⊢ x ∈ Algebra.unramifiedLocus R S

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this : Algebra.FormallyUnramified R Rₓ
⊢ x ∈ Algebra.unramifiedLocus R S

Tactic:
letI : Algebra Rₓ Sₓ := (Localization.localRingHom _ _ _ rfl).toAlgebra

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this✝ : Algebra.FormallyUnramified R Rₓ
this : Algebra Rₓ Sₓ := (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯).toAlgebra
⊢ x ∈ Algebra.unramifiedLocus R S