awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst_2 : CommRing R'
inst_3 : Algebra R R'
inst_4 : IsLocalization M R'
S' : Type u
inst_5 : CommRing S'
inst_6 : Algebra S S'
inst_7 : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this_1 : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
this_2 : IsScalarTower S (Localization (Submonoid.map f M)) S'
this :
  IsLocalization
    (Submonoid.map (F := S →+* Localization (Submonoid.map f M)) (algebraMap S (Localization (Submonoid.map f M))) T) S'
x : R
⊢ Eq (α := S')
    ((@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.map S' f hy) (algebraMap R R') : (a : R) → S') x : S')
    ((@comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
              (algebraMap (Localization (Submonoid.map f M)) S')
              (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))
            (algebraMap R R') :
          (a : R) → S')
        x :
      S')

Tactic:
simp [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst_2 : CommRing R'
inst_3 : Algebra R R'
inst_4 : IsLocalization M R'
S' : Type u
inst_5 : CommRing S'
inst_6 : Algebra S S'
inst_7 : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this_1 : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
this_2 : IsScalarTower S (Localization (Submonoid.map f M)) S'
this :
  IsLocalization
    (Submonoid.map (F := S →+* Localization (Submonoid.map f M)) (algebraMap S (Localization (Submonoid.map f M))) T) S'
⊢ Eq (α := R' →+* S') (IsLocalization.map S' f hy)
    (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))

Tactic:
have heq : IsLocalization.map (S := R') S' f hy =
      (algebraMap _ _).comp
        (IsLocalization.map (M := M) (T := M.map f) (S := R') (Localization (M.map f)) f
          (M.le_comap_map)) := by
    apply IsLocalization.ringHom_ext M
    ext
    simp [← IsScalarTower.algebraMap_apply]
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst_2 : CommRing R'
inst_3 : Algebra R R'
inst_4 : IsLocalization M R'
S' : Type u
inst_5 : CommRing S'
inst_6 : Algebra S S'
inst_7 : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this_1 : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
this_2 : IsScalarTower S (Localization (Submonoid.map f M)) S'
this :
  IsLocalization
    (Submonoid.map (F := S →+* Localization (Submonoid.map f M)) (algebraMap S (Localization (Submonoid.map f M))) T) S'
heq :
  Eq (α := R' →+* S') (IsLocalization.map S' f hy)
    (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))
rw :
  P (R := R')
    (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))
⊢ P (R := R') (IsLocalization.map S' f hy)

Tactic:
rw [heq]
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst_2 : CommRing R'
inst_3 : Algebra R R'
inst_4 : IsLocalization M R'
S' : Type u
inst_5 : CommRing S'
inst_6 : Algebra S S'
inst_7 : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this_1 : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
this_2 : IsScalarTower S (Localization (Submonoid.map f M)) S'
this :
  IsLocalization
    (Submonoid.map (F := S →+* Localization (Submonoid.map f M)) (algebraMap S (Localization (Submonoid.map f M))) T) S'
heq :
  Eq (α := R' →+* S') (IsLocalization.map S' f hy)
    (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))
⊢ P (R := R')
    (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))

Tactic:
hPc _ _ (hPp _ _ _ _ hf) (hPl _ (T.map (algebraMap S (Localization (M.map f)))))

Premises used: Algebra.algebraMap, Localization, Submonoid.map
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
M : Submonoid R
T : Submonoid S
R' : Type u
inst_2 : CommRing R'
inst_3 : Algebra R R'
inst_4 : IsLocalization M R'
S' : Type u
inst_5 : CommRing S'
inst_6 : Algebra S S'
inst_7 : IsLocalization T S'
f : R →+* S
hy : M ≤ Submonoid.comap f T
hf : P f
hle : Submonoid.map f M ≤ T
this_1 : Algebra (Localization (Submonoid.map f M)) S' :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization (Submonoid.map f M)) S' (Submonoid.map f M) T hle
this_2 : IsScalarTower S (Localization (Submonoid.map f M)) S'
this :
  IsLocalization
    (Submonoid.map (F := S →+* Localization (Submonoid.map f M)) (algebraMap S (Localization (Submonoid.map f M))) T) S'
heq :
  Eq (α := R' →+* S') (IsLocalization.map S' f hy)
    (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))
⊢ P (R := R')
    (@comp _ (Localization (Submonoid.map f M)) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (Localization (Submonoid.map f M)) S') (IsLocalization.map (Localization (Submonoid.map f M)) f ⋯))

Tactic:
exact hPc _ _ (hPp _ _ _ _ hf) (hPl _ (T.map (algebraMap S (Localization (M.map f)))))

Premises used: Algebra.algebraMap, Localization, Submonoid.map
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPp : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalization.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
p : Ideal R
inst_2 : p.IsPrime
q : Ideal S
inst_3 : q.IsPrime
f : R →+* S
h : p = Ideal.comap f q
hf : P f
⊢ P (R := Localization.AtPrime p) (S := Localization.AtPrime q) (Localization.localRingHom p q f h)

Tactic:
hPl.isLocalizationMap hPc hPp _ _ hf

Premises used: Localization.localRingHom, RingHom.HoldsForLocalization.isLocalizationMap
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
letI : P f
⊢ P f

Tactic:
letI := f.toAlgebra
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
this : Algebra R S := f.toAlgebra
⊢ LE.le (α := Submonoid R) (Submonoid.powers 1) (IsUnit.submonoid R)

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
this : Algebra R S := f.toAlgebra
⊢ IsLocalization (R := R) (Submonoid.powers 1) R

Tactic:
have := IsLocalization.of_le_isUnit (S := .powers (1 : R)) (by simp)
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
this_1 : Algebra R S := f.toAlgebra
this : IsLocalization (R := R) (Submonoid.powers 1) R
⊢ IsLocalization (R := R) (Submonoid.powers 1) S

Tactic:
have := IsLocalization.isLocalization_of_algEquiv (.powers (1 : R))
    (AlgEquiv.ofBijective (Algebra.ofId R S) hf)
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
this_1 : Algebra R S := f.toAlgebra
this_2 : IsLocalization (R := R) (Submonoid.powers 1) R
this : IsLocalization (R := R) (Submonoid.powers 1) S
⊢ P f

Tactic:
H _ 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
P : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
H : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hf : Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S)
this_1 : Algebra R S := f.toAlgebra
this_2 : IsLocalization (R := R) (Submonoid.powers 1) R
this : IsLocalization (R := R) (Submonoid.powers 1) S
⊢ P f

Tactic:
exact H _ 1

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
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
left :
  StableUnderCompositionWithLocalizationAwaySource.{u}
    fun {R S : Type u} [CommRing R] [CommRing S] {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)
right :
  StableUnderCompositionWithLocalizationAwayTarget.{u}
    fun {R S : Type u} [CommRing R] [CommRing S] {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)
⊢ StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P

Tactic:
constructor
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
r : R
inst_4 : IsLocalization.Away r S
f : S →+* T
hf : (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)) (f.comp (algebraMap R S))

Tactic:
hPc _ _ (hPl S r) hf
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
r : R
inst_4 : IsLocalization.Away r S
f : S →+* T
hf : (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)) (f.comp (algebraMap R S))

Tactic:
exact hPc _ _ (hPl S r) hf
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra S T
s : S
inst_4 : IsLocalization.Away s T
f : R →+* S
hf : (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)) (comp (algebraMap S T) f)

Tactic:
hPc _ _ hf (hPl T s)
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra S T
s : S
inst_4 : IsLocalization.Away s T
f : R →+* S
hf : (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)) (comp (algebraMap S T) f)

Tactic:
exact hPc _ _ hf (hPl T s)
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R : Type u
inst : CommRing R
⊢ P (id R)

Tactic:
hPl.of_bijective _ _ Function.bijective_id

Premises used: Function.bijective_id, RingHom.HoldsForLocalizationAway.of_bijective
-- Module: Mathlib.RingTheory.LocalProperties.Basic
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : HoldsForLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R : Type u
inst : CommRing R
⊢ P (id R)

Tactic:
exact hPl.of_bijective _ _ Function.bijective_id

Premises used: RingHom.HoldsForLocalizationAway.of_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 : 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 : 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 : R →+* S
e : S ≃+* T
hf : P f
this : Algebra S T := e.toRingHom.toAlgebra
⊢ IsLocalization.Away (R := R) 1 R

Tactic:
have : IsLocalization.Away (1 : R) R :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one (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 : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away (R := R) 1 R
⊢ IsUnit (M := S) ((f : (a : R) → S) 1 : S)

Tactic:
simp
-- 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 : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this : IsLocalization.Away (R := R) 1 R
⊢ IsLocalization.Away (R := S) ((f : (a : R) → S) 1 : S) T

Tactic:
have : IsLocalization.Away (f 1) T :=
      IsLocalization.away_of_isUnit_of_bijective _ (by simp) e.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 : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := R) 1 R
this : IsLocalization.Away (R := S) ((f : (a : R) → S) 1 : S) 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 : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := R) 1 R
this : IsLocalization.Away (R := S) ((f : (a : R) → S) 1 : S) T
h : e.toRingHom.comp f = IsLocalization.Away.map R T f 1
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)

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 : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := R) 1 R
this : IsLocalization.Away (R := S) ((f : (a : R) → S) 1 : S) T
trans :
  e.toRingHom.comp f = @comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.map R T f 1) (algebraMap R R)
trans₁ :
  Eq (α := R →+* T) (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.map R T f 1) (algebraMap R R))
    (IsLocalization.Away.map R T f 1)
⊢ e.toRingHom.comp f = IsLocalization.Away.map R T f 1

Tactic:
trans (IsLocalization.Away.map R T f 1).comp (algebraMap R R)

Premises used: Algebra.algebraMap, RingHom.comp, IsLocalization.Away.map, 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 : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := R) 1 R
this : IsLocalization.Away (R := S) ((f : (a : R) → S) 1 : S) T
rw : e.toRingHom.comp f = comp (algebraMap S T) f
⊢ e.toRingHom.comp f = @comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.map R T f 1) (algebraMap R R)

Tactic:
rw [IsLocalization.Away.map, IsLocalization.map_comp]

Premises used: IsLocalization.map_comp, IsLocalization.Away.map
-- 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 : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := R) 1 R
this : IsLocalization.Away (R := S) ((f : (a : R) → S) 1 : S) T
⊢ e.toRingHom.comp f = comp (algebraMap S T) f

Tactic:
rfl
-- 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 : R →+* S
e : S ≃+* T
hf : P f
this_1 : Algebra S T := e.toRingHom.toAlgebra
this_2 : IsLocalization.Away (R := R) 1 R
this : IsLocalization.Away (R := S) ((f : (a : R) → S) 1 : S) T
⊢ Eq (α := R →+* T) (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.map R T f 1) (algebraMap R R))
    (IsLocalization.Away.map R T f 1)

Tactic:
rfl
-- 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
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.symm.toRingHom.toAlgebra
-- 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 : Algebra S R := e.symm.toRingHom.toAlgebra
⊢ IsLocalization.Away (R := S) 1 R

Tactic:
have : IsLocalization.Away (1 : S) R :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.symm.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 : IsLocalization.Away (R := S) 1 R
⊢ IsUnit (M := T) ((f : (a : S) → T) 1 : T)

Tactic:
simp