-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma propertyIsLocal :
    PropertyIsLocal FormallyUnramified

Proof state:
R S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : f.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
algInst✝ : Algebra R' S' := (IsLocalization.Away.map R' S' f r).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
algebraizeInst✝ : Algebra.FormallyUnramified R S
this✝ : Algebra.FormallyUnramified S S'
this : Algebra.FormallyUnramified R S'
n : ℕ
⊢ (fun x => f r ^ x) n = f ((fun x => r ^ x) n)

Tactic:
simp

Result:
no goals

Proof state:
case localizationAwayPreserves
R S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : f.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
algInst✝ : Algebra R' S' := (IsLocalization.Away.map R' S' f r).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
algebraizeInst✝ : Algebra.FormallyUnramified R S
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Tactic:
have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := S') (.powers (f r))

Result:
case localizationAwayPreserves
R S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : f.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
algInst✝ : Algebra R' S' := (IsLocalization.Away.map R' S' f r).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
algebraizeInst✝ : Algebra.FormallyUnramified R S
this : Algebra.FormallyUnramified S S'
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Proof state:
case ofLocalizationSpanTarget

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

Tactic:
exact ofLocalizationSpanTarget

Result:
no goals

Proof state:
R S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : f.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
algInst✝ : Algebra R' S' := (IsLocalization.Away.map R' S' f r).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
algebraizeInst✝ : Algebra.FormallyUnramified R S
this✝ : Algebra.FormallyUnramified S S'
this : Algebra.FormallyUnramified R S'
⊢ Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r))

Tactic:
rintro x ⟨n, rfl⟩

Result:
case intro
R S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : f.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
algInst✝ : Algebra R' S' := (IsLocalization.Away.map R' S' f r).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
algebraizeInst✝ : Algebra.FormallyUnramified R S
this✝ : Algebra.FormallyUnramified S S'
this : Algebra.FormallyUnramified R S'
n : ℕ
⊢ (fun x => r ^ x) n ∈ Submonoid.comap f (Submonoid.powers (f r))

Proof state:
case localizationAwayPreserves
R S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H : f.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
algInst✝ : Algebra R' S' := (IsLocalization.Away.map R' S' f r).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
algebraizeInst✝ : Algebra.FormallyUnramified R S
this✝ : Algebra.FormallyUnramified S S'
this : Algebra.FormallyUnramified R S'
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Tactic:
have H : Submonoid.powers r ≤ (Submonoid.powers (f r)).comap f := by
  rintro x ⟨n, rfl⟩; exact ⟨n, by simp⟩

Result:
case localizationAwayPreserves
R S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H✝ : f.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
algInst✝ : Algebra R' S' := (IsLocalization.Away.map R' S' f r).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
algebraizeInst✝ : Algebra.FormallyUnramified R S
this✝ : Algebra.FormallyUnramified S S'
this : Algebra.FormallyUnramified R S'
H : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r))
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Proof state:
case localizationAwayPreserves
R S : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u_3
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
H✝ : f.FormallyUnramified
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra R S' := ((algebraMap S S').comp f).toAlgebra
algInst✝ : Algebra R' S' := (IsLocalization.Away.map R' S' f r).toAlgebra
scalarTowerInst✝ : IsScalarTower R S S' := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R S'))
algebraizeInst✝ : Algebra.FormallyUnramified R S
this✝¹ : Algebra.FormallyUnramified S S'
this✝ : Algebra.FormallyUnramified R S'
H : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r))
this : IsScalarTower R R' S'
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Tactic:
exact Algebra.FormallyUnramified.of_comp R R' S'

Result:
no goals