awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra S R := e.symm.toRingHom.toAlgebra
this : IsLocalization.Away (R := S) 1 R
⊢ IsLocalization.Away (R := T) ((f : (a : S) → T) 1 : T) T

Tactic:
have : IsLocalization.Away (f 1) T :=
      IsLocalization.away_of_isUnit_of_bijective _ (by simp) (Equiv.refl _).bijective
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra S R := e.symm.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := S) 1 R
this : IsLocalization.Away (R := T) ((f : (a : S) → T) 1 : T) T
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R T f 1)

Tactic:
hP f 1 R T hf

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra S R := e.symm.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := S) 1 R
this : IsLocalization.Away (R := T) ((f : (a : S) → T) 1 : T) T
h : f.comp e.toRingHom = IsLocalization.Away.map R T f 1
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)

Tactic:
convert! hP f 1 R T hf

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra S R := e.symm.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := S) 1 R
this : IsLocalization.Away (R := T) ((f : (a : S) → T) 1 : T) T
⊢ RingHomInvPair (↑e : R →+* S) (↑e.symm : S →+* R)

Tactic:
have : RingHomInvPair (e : R →+* S) e.symm := RingHomInvPair.of_ringEquiv _
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra S R := e.symm.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := S) 1 R
this_3 : IsLocalization.Away (R := T) ((f : (a : S) → T) 1 : T) T
this : RingHomInvPair (↑e : R →+* S) (↑e.symm : S →+* R)
⊢ comp (IsLocalization.Away.map R T f 1) e.symm.toRingHom = f

Tactic:
have : (IsLocalization.Away.map R T f 1).comp e.symm.toRingHom = f :=
      IsLocalization.map_comp ..
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra S R := e.symm.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := S) 1 R
this_3 : IsLocalization.Away (R := T) ((f : (a : S) → T) 1 : T) T
this_4 : RingHomInvPair (↑e : R →+* S) (↑e.symm : S →+* R)
this : comp (IsLocalization.Away.map R T f 1) e.symm.toRingHom = f
rw : comp (IsLocalization.Away.map R T f 1) (e.symm.toRingHom.comp e.toRingHom)
| f.comp e.toRingHom

Tactic:
rw [← this, RingHom.comp_assoc]

Premises used: RingHom.comp_assoc
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra S R := e.symm.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := S) 1 R
this_3 : IsLocalization.Away (R := T) ((f : (a : S) → T) 1 : T) T
this_4 : RingHomInvPair (↑e : R →+* S) (↑e.symm : S →+* R)
this : comp (IsLocalization.Away.map R T f 1) e.symm.toRingHom = f
h :
  Eq (α := R →+* T) (comp (IsLocalization.Away.map R T f 1) (e.symm.toRingHom.comp e.toRingHom))
    (IsLocalization.Away.map R T f 1)
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1

Tactic:
conv_lhs => rw [← this, RingHom.comp_assoc]

Premises used: RingHom.comp_assoc
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra S R := e.symm.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := S) 1 R
this_3 : IsLocalization.Away (R := T) ((f : (a : S) → T) 1 : T) T
this_4 : RingHomInvPair (↑e : R →+* S) (↑e.symm : S →+* R)
this : comp (IsLocalization.Away.map R T f 1) e.symm.toRingHom = f
⊢ Eq (α := R →+* T) (comp (IsLocalization.Away.map R T f 1) (e.symm.toRingHom.comp e.toRingHom))
    (IsLocalization.Away.map R T f 1)

Tactic:
simp only [RingEquiv.toRingHom_eq_coe, RingHomCompTriple.comp_eq]

Premises used: RingHomCompTriple.comp_eq, RingEquiv.toRingHom_eq_coe
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
letI : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
⊢ P (e.toRingHom.comp f)

Tactic:
letI := e.toRingHom.toAlgebra
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this : Algebra S T := e.toRingHom.toAlgebra
⊢ IsLocalization.Away (R := S) 1 T

Tactic:
have : IsLocalization.Away (1 : S) T :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away (R := S) 1 T
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)

Tactic:
hP.right T (1 : S) f hf

Premises used: And.right, OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away (R := S) 1 T
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)

Tactic:
exact hP.right T (1 : S) f hf

Premises used: And.right, OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
letI : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)
⊢ P (f.comp e.toRingHom)

Tactic:
letI := e.toRingHom.toAlgebra
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this : Algebra R S := e.toRingHom.toAlgebra
⊢ IsLocalization.Away (R := R) 1 S

Tactic:
have : IsLocalization.Away (1 : R) S :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra R S := e.toRingHom.toAlgebra
this : IsLocalization.Away (R := R) 1 S
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)

Tactic:
hP.left S (1 : R) f hf

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : P f
this_1 : Algebra R S := e.toRingHom.toAlgebra
this : IsLocalization.Away (R := R) 1 S
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)

Tactic:
exact hP.left S (1 : R) f hf

Premises used: And.left, OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal @P
⊢ RespectsIso @P

Tactic:
hP.localizationAwayPreserves.respectsIso

Premises used: RingHom.PropertyIsLocal.localizationAwayPreserves, RingHom.LocalizationAwayPreserves.respectsIso
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
_ :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_2 : CommRing R']
    [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_2 : CommRing R']
    [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
_ :
  ∀ [inst_1 : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_2 : CommRing R'] [inst_3 : CommRing S']
    [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst_1 : CommRing S] (f : R →+* S) (r : R) (R' S' : Type u) [inst_2 : CommRing R'] [inst_3 : CommRing S']
    [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
_ :
  ∀ [inst_2 : CommRing R'] [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S']
    [inst_6 : IsLocalization.Away r R'] [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst_2 : CommRing R'] [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S']
    [inst_6 : IsLocalization.Away r R'] [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
_ :
  ∀ [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst_3 : CommRing S'] [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
_ :
  ∀ [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst_4 : Algebra R R'] [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
_ :
  ∀ [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst_5 : Algebra S S'] [inst_6 : IsLocalization.Away r R']
    [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_6 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
_ :
  ∀ [inst_6 : IsLocalization.Away r R'] [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst_6 : IsLocalization.Away r R'] [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_7 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
_ :
  ∀ [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)
⊢ ∀ [inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'],
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (IsLocalization.Away.map R' S' f r)

Tactic:
_
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
hf : P f
rw : IsLocalization (R := S) (Submonoid.powers ((f : (a : R) → S) r) : Submonoid S) S'
⊢ IsLocalization (Submonoid.map f (Submonoid.powers r)) S'

Tactic:
rw [Submonoid.map_powers]

Premises used: Submonoid.map_powers
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
hf : P f
⊢ IsLocalization (R := S) (Submonoid.powers ((f : (a : R) → S) r) : Submonoid S) S'

Tactic:
assumption
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
hf : P f
have : ∀ (this : IsLocalization (Submonoid.map f (Submonoid.powers r)) S'), P (IsLocalization.Away.map R' S' f r)
⊢ P (IsLocalization.Away.map R' S' f r)

Tactic:
have : IsLocalization ((Submonoid.powers r).map f) S' := by rw [Submonoid.map_powers]; assumption
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
hf : P f
this : IsLocalization (Submonoid.map f (Submonoid.powers r)) S'
⊢ P (IsLocalization.Away.map R' S' f r)

Tactic:
H f (Submonoid.powers r) R' S' hf

Premises used: IsLocalization.map, Submonoid.copy, setOf, Submonoid.map, IsLocalization.Away.map, Submonoid.powers, Set.image, Set.range
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves @P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization.Away r R'
inst_7 : IsLocalization.Away (R := S) ((f : (a : R) → S) r : S) S'
hf : P f
this : IsLocalization (Submonoid.map f (Submonoid.powers r)) S'
⊢ P (IsLocalization.Away.map R' S' f r)

Tactic:
exact H f (Submonoid.powers r) R' S' hf

Premises used: Submonoid.powers
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal @P
hPi : ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
⊢ Eq (α := R →+* S) (algebraMap R S) (comp (algebraMap R S) (id R))

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal @P
hPi : ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
have : ∀ (this : Eq (α := R →+* S) (algebraMap R S) (comp (algebraMap R S) (id R))), P (algebraMap R S)
⊢ P (algebraMap R S)

Tactic:
have : algebraMap R S = (algebraMap R S).comp (RingHom.id R) := by simp
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal @P
hPi : ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
this : Eq (α := R →+* S) (algebraMap R S) (comp (algebraMap R S) (id R))
rw : P (comp (algebraMap R S) (id R))
⊢ P (algebraMap R S)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hP : PropertyIsLocal @P
hPi : ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
this : Eq (α := R →+* S) (algebraMap R S) (comp (algebraMap R S) (id R))
a : P (id R)
⊢ P (comp (algebraMap R S) (id R))

Tactic:
apply hP.StableUnderCompositionWithLocalizationAwayTarget S r

Premises used: RingHom.PropertyIsLocal.StableUnderCompositionWithLocalizationAwayTarget