-- Mathlib/RingTheory/RingHom/Locally.lean
/-- If `f` satisfies `P`, then in particular it satisfies `Locally P`. -/
lemma locally_of (hP : RespectsIso P) (f : R →+* S) (hf : P f) : Locally P f

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
hf : P f
⊢ ∃ (_ : Ideal.span {1} = ⊤),
    ∀ t ∈ {1}, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)

Tactic:
let e : S ≃+* Localization.Away (1 : S) :=
  (IsLocalization.atUnits S (Submonoid.powers 1) (by simp)).toRingEquiv

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
hf : P f
e : S ≃+* Localization.Away 1 := (IsLocalization.atUnits S (Submonoid.powers 1) ⋯).toRingEquiv
⊢ ∃ (_ : Ideal.span {1} = ⊤),
    ∀ t ∈ {1}, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
hf : P f
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid S

Tactic:
simp

Result:
no goals

Proof state:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
hf : P f
⊢ Locally (fun {R S} [CommRing R] [CommRing S] => P) f

Tactic:
use {1}

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
hf : P f
⊢ ∃ (_ : Ideal.span {1} = ⊤),
    ∀ t ∈ {1}, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
hf : P f
e : S ≃+* Localization.Away 1 := (IsLocalization.atUnits S (Submonoid.powers 1) ⋯).toRingEquiv
⊢ ∃ (_ : Ideal.span {1} = ⊤),
    ∀ t ∈ {1}, (fun {R S} [CommRing R] [CommRing S] => P) ((algebraMap S (Localization.Away t)).comp f)

Tactic:
simp only [Set.mem_singleton_iff, forall_eq, Ideal.span_singleton_one, exists_const]

Result:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
hf : P f
e : S ≃+* Localization.Away 1 := (IsLocalization.atUnits S (Submonoid.powers 1) ⋯).toRingEquiv
⊢ P ((algebraMap S (Localization.Away 1)).comp f)

Proof state:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] => P
f : R →+* S
hf : P f
e : S ≃+* Localization.Away 1 := (IsLocalization.atUnits S (Submonoid.powers 1) ⋯).toRingEquiv
⊢ P ((algebraMap S (Localization.Away 1)).comp f)

Tactic:
exact hP.left f e hf

Result:
no goals