-- Mathlib/RingTheory/RingHomProperties.lean
theorem RespectsIso.is_localization_away_iff (hP : RingHom.RespectsIso @P) {R S : Type u}
    (R' S' : Type u) [CommRing R] [CommRing S] [CommRing R'] [CommRing S'] [Algebra R R']
    [Algebra S S'] (f : R →+* S) (r : R) [IsLocalization.Away r R'] [IsLocalization.Away (f r) S'] :
    P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
⊢ Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r))

Tactic:
rintro x ⟨n, rfl⟩

Result:
case intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
n : ℕ
⊢ (fun x => r ^ x) n ∈ Submonoid.comap f (Submonoid.powers (f r))

Proof state:
case e_x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)
⊢ e = IsLocalization.Away.map R' S' f r

Tactic:
apply IsLocalization.ringHom_ext (Submonoid.powers r) _

Result:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)
⊢ e.comp (algebraMap R R') = (IsLocalization.Away.map R' S' f r).comp (algebraMap R R')

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)
this : e = IsLocalization.Away.map R' S' f r
⊢ (CommRingCat.Hom.hom e₂.toCommRingCatIso.hom).comp
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          {
            toFun :=
              ⇑(CommRingCat.Hom.hom
                    (CommRingCat.ofHom
                      {
                        toFun :=
                          (↑((IsLocalization.toLocalizationWithZeroMap (Submonoid.powers r) (Localization.Away r)).lift
                                ((algebraMap S (Localization.Away (f r))).comp f).toMonoidWithZeroHom ⋯)).toFun,
                        map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) ∘
                ⇑(CommRingCat.Hom.hom e₁.toCommRingCatIso.hom),
            map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) =
    IsLocalization.Away.map R' S' f r

Tactic:
convert this

Result:
no goals

Proof state:
case a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)
x : R
⊢ (IsLocalization.map S' (id S) ⋯)
      ((IsLocalization.map (Localization.Away (f r)) f ⋯)
        ((IsLocalization.map (Localization.Away r) (id R) ⋯) ((algebraMap R R') x))) =
    (IsLocalization.map S' f ⋯) ((algebraMap R R') x)

Tactic:
simp only [IsLocalization.map_eq, id_apply, RingHomCompTriple.comp_apply]

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)
⊢ e.comp (algebraMap R R') = (IsLocalization.Away.map R' S' f r).comp (algebraMap R R')

Tactic:
ext1 x

Result:
case a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
e : R' →+* S' := (↑e₂).comp ((IsLocalization.map (Localization.Away (f r)) f ⋯).comp ↑e₁)
x : R
⊢ (e.comp (algebraMap R R')) x = ((IsLocalization.Away.map R' S' f r).comp (algebraMap R R')) x