awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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 ⋯))
have h : Eq (α := R →+* S') (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.map S' f hy) (algebraMap R R'))
  (@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 sorry))
    (algebraMap R R'))
Tactic: apply IsLocalization.ringHom_ext M
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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') (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.map S' f hy) (algebraMap R R'))
    (@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'))
have h : ∀ (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 sorry))
            (algebraMap R R') :
          (a : R) → S')
        x :
      S')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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'
⊢ P (R := R') (IsLocalization.map S' f hy)
have 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 sorry))
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]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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') (IsLocalization.map S' f hy)
have 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 sorry))
Tactic: rw [heq]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ P f
have this₁ : IsLocalization (R := R) (Submonoid.powers 1) R
Tactic: have := IsLocalization.of_le_isUnit (S := .powers (1 : R)) (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ P f
have this₁ : IsLocalization (R := R) (Submonoid.powers 1) S
Tactic: have := IsLocalization.isLocalization_of_algEquiv (.powers (1 : R))
    (AlgEquiv.ofBijective (Algebra.ofId R S) hf)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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
⊢ StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
have left : StableUnderCompositionWithLocalizationAwaySource.{u}
  fun {R S : Type u} [CommRing R] [CommRing S] {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)
⊢ StableUnderCompositionWithLocalizationAway.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
have right : StableUnderCompositionWithLocalizationAwayTarget.{u}
  fun {R S : Type u} [CommRing R] [CommRing S] {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
have this₁ : IsLocalization.Away (R := R) 1 R
Tactic: have : IsLocalization.Away (1 : R) R :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one (Equiv.refl _).bijective
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)) (e.toRingHom.comp f)
have h : e.toRingHom.comp f = IsLocalization.Away.map R T f 1
Tactic: convert! hP f 1 R T hf
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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 = IsLocalization.Away.map R T f 1
have trans : e.toRingHom.comp f = @comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.map R T f 1) (algebraMap R R)
Tactic: trans (IsLocalization.Away.map R T f 1).comp (algebraMap R R)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)
⊢ e.toRingHom.comp f = IsLocalization.Away.map R T f 1
have trans₁ : Eq (α := R →+* T) (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.map R T f 1) (algebraMap R R))
  (IsLocalization.Away.map R T f 1)
Tactic: trans (IsLocalization.Away.map R T f 1).comp (algebraMap R R)
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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 _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.map R T f 1) (algebraMap R R)
have rw : e.toRingHom.comp f = comp (algebraMap S T) f
Tactic: rw [IsLocalization.Away.map, IsLocalization.map_comp]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)
have this₁ : IsLocalization.Away (R := S) 1 R
Tactic: have : IsLocalization.Away (1 : S) R :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.symm.bijective
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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)) (f.comp e.toRingHom)
have h : f.comp e.toRingHom = IsLocalization.Away.map R T f 1
Tactic: convert! hP f 1 R T hf
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1
have this₁ : RingHomInvPair (↑e : R →+* S) (↑e.symm : S →+* R)
Tactic: have : RingHomInvPair (e : R →+* S) e.symm := RingHomInvPair.of_ringEquiv _
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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)
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1
have this₁ : 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 ..
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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
| f.comp e.toRingHom
have rw : comp (IsLocalization.Away.map R T f 1) (e.symm.toRingHom.comp e.toRingHom)
Tactic: rw [← this, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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
⊢ f.comp e.toRingHom = IsLocalization.Away.map R T f 1
have 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)
Tactic: conv_lhs => rw [← this, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
have this₁ : IsLocalization.Away (R := S) 1 T
Tactic: have : IsLocalization.Away (1 : S) T :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (hypothesis)
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
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)
have this₁ : IsLocalization.Away (R := R) 1 S
Tactic: have : IsLocalization.Away (1 : R) S :=
      IsLocalization.away_of_isUnit_of_bijective _ isUnit_one e.bijective
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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 (Submonoid.map f (Submonoid.powers r)) S'
have rw : IsLocalization (R := S) (Submonoid.powers ((f : (a : R) → S) r) : Submonoid S) S'
Tactic: rw [Submonoid.map_powers]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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
⊢ P (IsLocalization.Away.map R' S' f r)
have have : ∀ (this : IsLocalization (Submonoid.map f (Submonoid.powers r)) S'), P (IsLocalization.Away.map R' S' f r)
Tactic: have : IsLocalization ((Submonoid.powers r).map f) S' := by rw [Submonoid.map_powers]; assumption
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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
⊢ P (algebraMap R S)
have have : ∀ (this : Eq (α := R →+* S) (algebraMap R S) (comp (algebraMap R S) (id R))), P (algebraMap R S)
Tactic: have : algebraMap R S = (algebraMap R S).comp (RingHom.id R) := by simp
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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))
⊢ P (algebraMap R S)
have rw : P (comp (algebraMap R S) (id R))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.LocalProperties.Basic (goal)
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))
⊢ P (comp (algebraMap R S) (id R))
have a : P (id R)
Tactic: apply hP.StableUnderCompositionWithLocalizationAwayTarget S r