-- Mathlib/RingTheory/RingHom/Unramified.lean
lemma propertyIsLocal :
    PropertyIsLocal 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
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Tactic:
algebraize [f, (algebraMap S S').comp f, IsLocalization.Away.map R' S' 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
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Proof state:
case localizationAwayPreserves

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

Tactic:
intro R S _ _ f r R' S' _ _ _ _ _ _ H

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
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Proof state:
case ofLocalizationSpan

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

Tactic:
exact ofLocalizationSpanTarget.ofLocalizationSpan
  (stableUnderComposition.stableUnderCompositionWithLocalizationAway
      holdsForLocalizationAway).1

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
this : Algebra.FormallyUnramified S S'
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Tactic:
have := Algebra.FormallyUnramified.comp R S S'

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'
⊢ (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))
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

Tactic:
have : IsScalarTower R R' S' := .of_algebraMap_eq' (IsLocalization.map_comp H).symm

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))
this : IsScalarTower R R' S'
⊢ (IsLocalization.Away.map R' S' f r).FormallyUnramified

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

Tactic:
constructor

Result:
case localizationAwayPreserves

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

case ofLocalizationSpanTarget

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

case ofLocalizationSpan

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

case StableUnderCompositionWithLocalizationAwayTarget

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

Proof state:
case StableUnderCompositionWithLocalizationAwayTarget

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

Tactic:
exact (stableUnderComposition.stableUnderCompositionWithLocalizationAway
    holdsForLocalizationAway).2

Result:
no goals

Proof state:
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))

Tactic:
exact ⟨n, by simp⟩

Result:
no goals