awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
P : Type u_3
inst_1 : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
y : ↥M
w z₁ z₂ : P
rw :
  w + HMul.hMul (α := P) ((((↑g : R →* P).restrict M : MonoidHom.{u_1, u_3} (↥M) P) : (a : ↥M) → P) y : P) z₁ =
      HMul.hMul (α := P) ((((↑g : R →* P).restrict M : MonoidHom.{u_1, u_3} (↥M) P) : (a : ↥M) → P) y : P) z₂ ↔
    w + HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₁ = HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₂
⊢ w * (↑((IsUnit.liftRight ((↑g : R →* P).restrict M) h : (a : ↥M) → Pˣ) y)⁻¹ : P) + z₁ = z₂ ↔
    w + HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₁ = HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₂

Tactic:
rw [mul_comm, ← one_mul z₁, ← Units.inv_mul (IsUnit.liftRight (g.toMonoidHom.restrict M) h y),
    mul_assoc, ← mul_add, Units.inv_mul_eq_iff_eq_mul, Units.inv_mul_cancel_left,
    IsUnit.coe_liftRight]

Premises used: IsUnit.liftRight, mul_assoc, Units.inv_mul, MonoidHom.restrict, IsUnit.coe_liftRight, mul_comm, mul_add, RingHom.toMonoidHom, Units.inv_mul_eq_iff_eq_mul, DFunLike.coe, one_mul, Units.inv_mul_cancel_left
-- Module: Mathlib.RingTheory.Localization.Defs
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
P : Type u_3
inst_1 : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
y : ↥M
w z₁ z₂ : P
⊢ w + HMul.hMul (α := P) ((((↑g : R →* P).restrict M : MonoidHom.{u_1, u_3} (↥M) P) : (a : ↥M) → P) y : P) z₁ =
      HMul.hMul (α := P) ((((↑g : R →* P).restrict M : MonoidHom.{u_1, u_3} (↥M) P) : (a : ↥M) → P) y : P) z₂ ↔
    w + HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₁ = HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₂

Tactic:
simp [RingHom.toMonoidHom_eq_coe, MonoidHom.restrict_apply]

Premises used: RingHom.toMonoidHom_eq_coe, MonoidHom.restrict_apply
-- Module: Mathlib.RingTheory.Localization.Defs
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)
z : S
w w' v : P
rw :
  HMul.hMul (α := P) (((↑g : R →* P) : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).1 : P) w +
        HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P)
          w' =
      HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) v ↔
    HMul.hMul (α := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).1 : P) w +
        HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P)
          w' =
      HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) v
⊢ HMul.hMul (α := P) ((Submonoid.LocalizationMap.lift (toLocalizationMap M S) hg : (a : S) → P) z : P) w + w' = v ↔
    HMul.hMul (α := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).1 : P) w +
        HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P)
          w' =
      HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) v

Tactic:
rw [mul_comm, Submonoid.LocalizationMap.lift_apply, ← mul_assoc, mul_add_inv_left hg,
    mul_comm]

Premises used: IsLocalization.mul_add_inv_left, mul_assoc, Submonoid.LocalizationMap.lift_apply, mul_comm
-- Module: Mathlib.RingTheory.Localization.Defs
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)
z : S
w w' v : P
⊢ HMul.hMul (α := P) (((↑g : R →* P) : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).1 : P) w +
        HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P)
          w' =
      HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) v ↔
    HMul.hMul (α := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).1 : P) w +
        HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P)
          w' =
      HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) v

Tactic:
rfl
-- Module: Mathlib.RingTheory.Localization.Defs
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
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)
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Localization.Defs
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
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))
⊢ (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:
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]

Premises used: Submonoid.LocalizationMap.lift_spec, IsLocalization.lift_spec_mul_add, mul_assoc, eq_comm, add_comm, IsLocalization.toLocalizationMap, mul_comm, mul_add, Submonoid.LocalizationMap.lift₀_def
-- Module: Mathlib.RingTheory.Localization.Defs
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
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)
⊢ 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:
simp_rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Localization.Defs
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
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)
⊢ 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:
change g _ * g _ * g _ + g _ * g _ * g _ = g _ * g _ * g _

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Defs
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
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)
⊢ 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:
simp_rw [← map_mul g, ← map_add g]

Premises used: map_add, map_mul
-- Module: Mathlib.RingTheory.Localization.Defs
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
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)
⊢ 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:
apply eq_of_eq (S := S) hg

Premises used: IsLocalization.eq_of_eq
-- Module: Mathlib.RingTheory.Localization.Defs
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
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)
⊢ 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:
simp only [sec_spec', toLocalizationMap_sec, map_add, map_mul]

Premises used: map_add, IsLocalization.sec_spec', map_mul, IsLocalization.toLocalizationMap_sec
-- Module: Mathlib.RingTheory.Localization.Defs
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 (β := 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:
ring
-- Module: Mathlib.RingTheory.Localization.Defs
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 : R
y : ↥M
⊢ (lift hg : (a : S) → P) (mk' S x y) =
    HMul.hMul (α := P) (β := P) ((g : (a : R) → P) x : P)
      ((↑((IsUnit.liftRight ((↑g : R →* P).restrict M) hg : (a : ↥M) → Pˣ) y)⁻¹ : P) : P)

Tactic:
(toLocalizationMap M S).lift_mk' _ _ _

Premises used: Submonoid.LocalizationMap.lift_mk', IsLocalization.mk', IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
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 : R
v : P
y : ↥M
⊢ (lift hg : (a : S) → P) (mk' S x y) = v ↔ (g : (a : R) → P) x = HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) v

Tactic:
(toLocalizationMap M S).lift_mk'_spec _ _ _ _

Premises used: IsLocalization.mk', IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.lift_mk'_spec
-- Module: Mathlib.RingTheory.Localization.Defs
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 : R
⊢ Eq.{u_3 + 1} (α := P) ((lift hg : (a : S) → P) ((algebraMap R S : (a : R) → S) x : S) : P) ((g : (a : R) → P) x : P)

Tactic:
(toLocalizationMap M S).lift_eq _ _

Premises used: IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.lift_eq