awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
x y : S
⊢ ZeroHom.toFun
      (↑(Submonoid.LocalizationMap.lift₀.{u_1, u_2, u_3} (M := R) (S := M) (toLocalizationMap M S) g.toMonoidWithZeroHom
            hg) :
        ZeroHom S P)
      (x + y) =
    HAdd.hAdd (α := P)
      (ZeroHom.toFun
        (↑(Submonoid.LocalizationMap.lift₀.{u_1, u_2, u_3} (M := R) (S := M) (toLocalizationMap M S)
              g.toMonoidWithZeroHom hg) :
          ZeroHom S P)
        x)
      (ZeroHom.toFun
        (↑(Submonoid.LocalizationMap.lift₀.{u_1, u_2, u_3} (M := R) (S := M) (toLocalizationMap M S)
              g.toMonoidWithZeroHom hg) :
          ZeroHom S P)
        y)
have dsimp : (Submonoid.LocalizationMap.lift₀.{u_1, u_2, u_3} (M := R) (S := M) (toLocalizationMap M S) g.toMonoidWithZeroHom hg :
      (a : S) → P)
    (x + y) =
  HAdd.hAdd (α := P) (β := P)
    ((Submonoid.LocalizationMap.lift₀.{u_1, u_2, u_3} (M := R) (S := M) (toLocalizationMap M S) g.toMonoidWithZeroHom
            hg :
          (a : S) → P)
        x :
      P)
    ((Submonoid.LocalizationMap.lift₀.{u_1, u_2, u_3} (M := R) (S := M) (toLocalizationMap M S) g.toMonoidWithZeroHom
            hg :
          (a : S) → P)
        y :
      P)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
x y : S
⊢ (Submonoid.LocalizationMap.lift₀.{u_1, u_2, u_3} (M := R) (S := M) (toLocalizationMap M S) g.toMonoidWithZeroHom hg :
        (a : S) → P)
      (x + y) =
    HAdd.hAdd (α := P) (β := P)
      ((Submonoid.LocalizationMap.lift₀.{u_1, u_2, u_3} (M := R) (S := M) (toLocalizationMap M S) g.toMonoidWithZeroHom
              hg :
            (a : S) → P)
          x :
        P)
      ((Submonoid.LocalizationMap.lift₀.{u_1, u_2, u_3} (M := R) (S := M) (toLocalizationMap M S) g.toMonoidWithZeroHom
              hg :
            (a : S) → P)
          y :
        P)
have rw : HMul.hMul (α := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 : P)
      (HMul.hMul (α := P) (β := P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P)
        (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) :
          P)) +
    HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
      (HMul.hMul (α := P) (β := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 : P)
        (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) :
          P)) =
  HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
    (HMul.hMul (α := P) (β := P)
      ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P)
      (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
          (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1 :
        P))
Tactic: rw [(toLocalizationMap M S).lift₀_def, (toLocalizationMap M S).lift_spec,
        mul_add, mul_comm, eq_comm, lift_spec_mul_add, add_comm, mul_comm, mul_assoc, mul_comm,
        mul_assoc, lift_spec_mul_add]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
x y : S
⊢ HMul.hMul (α := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 : P)
        (HMul.hMul (α := P) (β := P)
          ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P)
          (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
              (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) :
            P)) +
      HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
        (HMul.hMul (α := P) (β := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 : P)
          (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
              (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) :
            P)) =
    HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
      (HMul.hMul (α := P) (β := P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P)
        (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
            (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1 :
          P))
have simp_rw : HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 : P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P))
      (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) :
        P) +
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
        ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 : P))
      (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) :
        P) =
  HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P)
      ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
      ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P))
    (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
        (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1 :
      P)
Tactic: simp_rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
x y : S
⊢ HMul.hMul (β := P)
        (HMul.hMul (α := P) (β := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 : P)
          ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P))
        (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) :
          P) +
      HMul.hMul (β := P)
        (HMul.hMul (α := P) (β := P)
          ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
          ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 : P))
        (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) :
          P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P))
      (((↑g.toMonoidWithZeroHom : R →* P) : (a : R) → P)
          (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1 :
        P)
have change : HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 : P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P))
      ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) : P) +
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
        ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 : P))
      ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) : P) =
  HMul.hMul (β := P)
    (HMul.hMul (α := P) (β := P)
      ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
      ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P))
    ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1 : P)
Tactic: change g _ * g _ * g _ + g _ * g _ * g _ = g _ * g _ * g _
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
x y : S
⊢ HMul.hMul (β := P)
        (HMul.hMul (α := P) (β := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 : P)
          ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P))
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) : P) +
      HMul.hMul (β := P)
        (HMul.hMul (α := P) (β := P)
          ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
          ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 : P))
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) : P) =
    HMul.hMul (β := P)
      (HMul.hMul (α := P) (β := P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) : P)
        ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) : P))
      ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1 : P)
have simp_rw : Eq.{u_3 + 1} (α := P)
  ((g : (a : R) → P)
      ((Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 *
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) *
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) +
        (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) *
            (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 *
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R)) :
    P)
  ((g : (a : R) → P)
      ((↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) *
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) *
        (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1) :
    P)
Tactic: simp_rw [← map_mul g, ← map_add g]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
x y : S
⊢ Eq.{u_3 + 1} (α := P)
    ((g : (a : R) → P)
        ((Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 *
              (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) *
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) +
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) *
              (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 *
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R)) :
      P)
    ((g : (a : R) → P)
        ((↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) *
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) *
          (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1) :
      P)
have apply : Eq.{u_2 + 1} (α := S)
  ((algebraMap R S : (a : R) → S)
      ((Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 *
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) *
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) +
        (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) *
            (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 *
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R)) :
    S)
  ((algebraMap R S : (a : R) → S)
      ((↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) *
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) *
        (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1) :
    S)
Tactic: apply eq_of_eq (S := S) hg
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
x y : S
⊢ Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        ((Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).1 *
              (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) *
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R) +
          (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) *
              (Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).1 *
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).2 : R)) :
      S)
    ((algebraMap R S : (a : R) → S)
        ((↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) y).2 : R) *
            (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) x).2 : R) *
          (Submonoid.LocalizationMap.sec (toLocalizationMap M S) (x + y)).1) :
      S)
have simp : HMul.hMul (β := S)
      (HMul.hMul (β := S) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑(sec M y).2 : R) : S) y)
        ((algebraMap R S : (a : R) → S) (↑(sec M x).2 : R) : S))
      ((algebraMap R S : (a : R) → S) (↑(sec M (x + y)).2 : R) : S) +
    HMul.hMul (β := S)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑(sec M y).2 : R) : S)
        (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑(sec M x).2 : R) : S) x))
      ((algebraMap R S : (a : R) → S) (↑(sec M (x + y)).2 : R) : S) =
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑(sec M y).2 : R) : S)
      ((algebraMap R S : (a : R) → S) (↑(sec M x).2 : R) : S) *
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑(sec M (x + y)).2 : R) : S) (x + y)
Tactic: simp only [sec_spec', toLocalizationMap_sec, map_add, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
P : Type u_4
inst_4 : Monoid P
j k : S → P
hj1 : j 1 = 1
hk1 : k 1 = 1
hjm : ∀ (a b : S), j (a * b) = j a * j b
hkm : ∀ (a b : S), k (a * b) = k a * k b
h : ∀ (a : R), j ((algebraMap R S : (a : R) → S) a) = k ((algebraMap R S : (a : R) → S) a)
j' : S →* P := { toFun := j, map_one' := hj1, map_mul' := hjm }
k' : S →* P := { toFun := k, map_one' := hk1, map_mul' := hkm }
this : j' = k'
⊢ (↑j' : OneHom S P).toFun = (↑k' : OneHom S P).toFun
have rw : (↑k' : OneHom S P).toFun = (↑k' : OneHom S P).toFun
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommSemiring T
f : S →+* T
⊢ Injective.{u_2 + 1, u_4 + 1} (α := S) (β := T) (⇑f : (a : S) → T) ↔
    ∀ (x y : R),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
        Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
          ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)
have rw : (∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
      Eq.{u_4 + 1} (α := T) ((f.comp (algebraMap R S) : (a : R) → T) x : T)
        ((f.comp (algebraMap R S) : (a : R) → T) y : T)) ↔
  ∀ (x y : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
      Eq.{u_4 + 1} (α := T)
        ((lift (g := f.comp (algebraMap R S)) sorry : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
        ((lift (g := f.comp (algebraMap R S)) sorry : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)
Tactic: rw [← IsLocalization.lift_of_comp (M := M) f, IsLocalization.lift_injective_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst_8 : CommSemiring A
U : Submonoid A
W : Type u_6
inst_9 : CommSemiring W
inst_10 : Algebra A W
inst_11 : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ Eq.{u_6 + 1} (α := W) ((map W l hl : (a : Q) → W) ((map Q g hy : (a : S) → Q) x : Q) : W)
    ((map (M := M) (T := U) W (l.comp g) ⋯ : (a : S) → W) x : W)
have rw : Eq.{u_6 + 1} (α := W) ((map W l hl : (a : Q) → W) ((map Q g hy : (a : S) → Q) x : Q) : W)
  ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map W l hl) (map Q g hy) : (a : S) → W) x : W)
Tactic: rw [← map_comp_map (Q := Q) hy hl]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (map Q g hy : (a : S) → Q) (z • x) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)
have rw : (map Q g hy : (a : S) → Q) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x) =
  HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)
Tactic: rw [Algebra.smul_def, Algebra.smul_def, map_mul, map_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
rw :
  (map Q g hy : (a : S) → Q) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)
⊢ (map Q g hy : (a : S) → Q) (z • x) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)
have rw₁ : (map Q g hy : (a : S) → Q) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x) =
  HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
    ((map Q g hy : (a : S) → Q) x : Q)
Tactic: rw [Algebra.smul_def, Algebra.smul_def, map_mul, map_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
rw :
  (map Q g hy : (a : S) → Q) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)
rw₁ :
  (map Q g hy : (a : S) → Q) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x) =
    HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
      ((map Q g hy : (a : S) → Q) x : Q)
⊢ (map Q g hy : (a : S) → Q) (z • x) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)
have rw₂ : HMul.hMul (α := Q) (β := Q) ((map Q g hy : (a : S) → Q) ((algebraMap R S : (a : R) → S) z : S) : Q)
    ((map Q g hy : (a : S) → Q) x : Q) =
  HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
    ((map Q g hy : (a : S) → Q) x : Q)
Tactic: rw [Algebra.smul_def, Algebra.smul_def, map_mul, map_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
rw :
  (map Q g hy : (a : S) → Q) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)
rw₁ :
  (map Q g hy : (a : S) → Q) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x) =
    HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
      ((map Q g hy : (a : S) → Q) x : Q)
rw₂ :
  HMul.hMul (α := Q) (β := Q) ((map Q g hy : (a : S) → Q) ((algebraMap R S : (a : R) → S) z : S) : Q)
      ((map Q g hy : (a : S) → Q) x : Q) =
    HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
      ((map Q g hy : (a : S) → Q) x : Q)
⊢ (map Q g hy : (a : S) → Q) (z • x) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)
have rw₃ : HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
    ((map Q g hy : (a : S) → Q) x : Q) =
  HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
    ((map Q g hy : (a : S) → Q) x : Q)
Tactic: rw [Algebra.smul_def, Algebra.smul_def, map_mul, map_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ Submonoid.map h.symm.toMonoidHom T = M
have rw : Eq (α := Submonoid R) (Submonoid.map (h.symm.toMonoidHom.comp h.toMonoidHom) M)
  (Submonoid.map (F := R →* R) (MonoidHom.id R) M)
Tactic: rw [← M.map_id, ← H, Submonoid.map_map]