-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma ofLocalizationSpanTarget :
    OfLocalizationSpanTarget FormallyUnramified

Proof state:
case a
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔ ((algebraMap S (Localization.Away r)).comp f).FormallyUnramified

Tactic:
rw [← algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq,
  formallyUnramified_algebraMap]

Result:
no goals

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ ∀ (x : PrimeSpectrum S), x ∈ Algebra.unramifiedLocus R S

Tactic:
intro x

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
⊢ x ∈ Algebra.unramifiedLocus R S

Proof state:
case intro.intro
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ Algebra.FormallyUnramified R (Localization.Away r)

Tactic:
convert H ⟨r, hr⟩

Result:
case a
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑⟨r, hr⟩)).comp f)

Proof state:
case a
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔
    (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑⟨r, hr⟩)).comp f)

Tactic:
dsimp

Result:
case a
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔ ((algebraMap S (Localization.Away r)).comp f).FormallyUnramified

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp 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
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp 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
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
⊢ x ∈ Algebra.unramifiedLocus R S

Tactic:
obtain ⟨r, hr, hrx⟩ : ∃ r ∈ s, x ∈ PrimeSpectrum.basicOpen r := by
  simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge
    (TopologicalSpace.Opens.mem_top x)

Result:
case intro.intro
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ x ∈ Algebra.unramifiedLocus R S

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ f.FormallyUnramified

Tactic:
algebraize [f]

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
⊢ f.FormallyUnramified

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

Tactic:
intros R S _ _ f s hs H

Result:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
⊢ f.FormallyUnramified

Proof state:
case intro.intro
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ x ∈ Algebra.unramifiedLocus R S

Tactic:
refine Algebra.basicOpen_subset_unramifiedLocus_iff.mpr ?_ hrx

Result:
case intro.intro
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : x ∈ PrimeSpectrum.basicOpen r
⊢ Algebra.FormallyUnramified R (Localization.Away r)

Proof state:
R S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hs : Ideal.span s = ⊤
H :
  ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] => FormallyUnramified) ((algebraMap S (Localization.Away ↑r)).comp f)
algInst✝ : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
⊢ ∃ r ∈ s, x ∈ PrimeSpectrum.basicOpen r

Tactic:
simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge
  (TopologicalSpace.Opens.mem_top x)

Result:
no goals