awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
a : ↥M₂
ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)
h :
  HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) (↑a : R) : S₁)
      (HMul.hMul (α := S₁) (β := S₁) ((algebraMap R S₁ : (a : R) → S₁) c : S₁)
        ((algebraMap R S₁ : (a : R) → S₁) s : S₁)) =
    HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁) (β := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        ((algebraMap R S₁ : (a : R) → S₁) s : S₁))
      ((algebraMap R S₁ : (a : R) → S₁) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M₁) c hmc) : R) : S₁)
⊢ HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁) (β := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        ((algebraMap R S₁ : (a : R) → S₁) r : S₁))
      ((algebraMap R S₁ : (a : R) → S₁) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M₁) c hmc) : R) : S₁) =
    HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁) (β := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        ((algebraMap R S₁ : (a : R) → S₁) s : S₁))
      ((algebraMap R S₁ : (a : R) → S₁) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M₁) c hmc) : R) : S₁)

Tactic:
rw [← map_mul, ← map_mul, mul_assoc, mul_comm _ c, ha, map_mul, map_mul]

Premises used: mul_assoc, map_mul, mul_comm
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
a : ↥M₂
ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)
⊢ HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) (↑a : R) : S₁)
      (HMul.hMul (α := S₁) (β := S₁) ((algebraMap R S₁ : (a : R) → S₁) c : S₁)
        ((algebraMap R S₁ : (a : R) → S₁) s : S₁)) =
    HMul.hMul (β := S₁)
      (HMul.hMul (α := S₁) (β := S₁)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
            S₁) :
          S₁)
        ((algebraMap R S₁ : (a : R) → S₁) s : S₁))
      ((algebraMap R S₁ : (a : R) → S₁) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M₁) c hmc) : R) : S₁)

Tactic:
ring
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst_3 : CommSemiring Rₘ
inst_4 : CommSemiring Sₙ
inst_5 : CommSemiring Rₘ'
inst_6 : CommSemiring Sₙ'
inst_7 : Algebra R Rₘ
inst_8 : Algebra S Sₙ
inst_9 : Algebra R Rₘ'
inst_10 : Algebra S Sₙ'
inst_11 : Algebra R Sₙ
inst_12 : Algebra Rₘ Sₙ
inst_13 : Algebra Rₘ' Sₙ'
inst_14 : Algebra R Sₙ'
N : Submonoid S
inst_15 : IsLocalization M Rₘ
inst_16 : IsLocalization N Sₙ
inst_17 : IsLocalization M Rₘ'
inst_18 : IsLocalization N Sₙ'
inst_19 : IsScalarTower R Rₘ Sₙ
inst_20 : IsScalarTower R S Sₙ
inst_21 : IsScalarTower R Rₘ' Sₙ'
inst_22 : IsScalarTower R S Sₙ'
⊢ Eq (α := Rₘ →+* Sₙ')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv N Sₙ Sₙ') : Sₙ →+* Sₙ') (algebraMap Rₘ Sₙ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ' Sₙ') (↑(algEquiv M Rₘ Rₘ') : Rₘ →+* Rₘ'))

Tactic:
IsLocalization.ringHom_ext M (RingHom.ext fun x => ?_)

Premises used: RingHom.ext, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst_3 : CommSemiring Rₘ
inst_4 : CommSemiring Sₙ
inst_5 : CommSemiring Rₘ'
inst_6 : CommSemiring Sₙ'
inst_7 : Algebra R Rₘ
inst_8 : Algebra S Sₙ
inst_9 : Algebra R Rₘ'
inst_10 : Algebra S Sₙ'
inst_11 : Algebra R Sₙ
inst_12 : Algebra Rₘ Sₙ
inst_13 : Algebra Rₘ' Sₙ'
inst_14 : Algebra R Sₙ'
N : Submonoid S
inst_15 : IsLocalization M Rₘ
inst_16 : IsLocalization N Sₙ
inst_17 : IsLocalization M Rₘ'
inst_18 : IsLocalization N Sₙ'
inst_19 : IsScalarTower R Rₘ Sₙ
inst_20 : IsScalarTower R S Sₙ
inst_21 : IsScalarTower R Rₘ' Sₙ'
inst_22 : IsScalarTower R S Sₙ'
refine :
  ∀ (x : R),
    Eq.{u_7 + 1} (α := Sₙ')
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv N Sₙ Sₙ') : Sₙ →+* Sₙ')
                (algebraMap Rₘ Sₙ))
              (algebraMap R Rₘ) :
            (a : R) → Sₙ')
          x :
        Sₙ')
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ' Sₙ')
                (↑(algEquiv M Rₘ Rₘ') : Rₘ →+* Rₘ'))
              (algebraMap R Rₘ) :
            (a : R) → Sₙ')
          x :
        Sₙ')
⊢ Eq (α := Rₘ →+* Sₙ')
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv N Sₙ Sₙ') : Sₙ →+* Sₙ') (algebraMap Rₘ Sₙ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ' Sₙ') (↑(algEquiv M Rₘ Rₘ') : Rₘ →+* Rₘ'))

Tactic:
refine IsLocalization.ringHom_ext M (RingHom.ext fun x => ?_)

Premises used: RingHom.ext, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst_3 : CommSemiring Rₘ
inst_4 : CommSemiring Sₙ
inst_5 : CommSemiring Rₘ'
inst_6 : CommSemiring Sₙ'
inst_7 : Algebra R Rₘ
inst_8 : Algebra S Sₙ
inst_9 : Algebra R Rₘ'
inst_10 : Algebra S Sₙ'
inst_11 : Algebra R Sₙ
inst_12 : Algebra Rₘ Sₙ
inst_13 : Algebra Rₘ' Sₙ'
inst_14 : Algebra R Sₙ'
N : Submonoid S
inst_15 : IsLocalization M Rₘ
inst_16 : IsLocalization N Sₙ
inst_17 : IsLocalization M Rₘ'
inst_18 : IsLocalization N Sₙ'
inst_19 : IsScalarTower R Rₘ Sₙ
inst_20 : IsScalarTower R S Sₙ
inst_21 : IsScalarTower R Rₘ' Sₙ'
inst_22 : IsScalarTower R S Sₙ'
x : R
simp :
  Eq.{u_7 + 1} (α := Sₙ')
    ((algEquiv N Sₙ Sₙ' : (a : Sₙ) → Sₙ')
        ((algebraMap Rₘ Sₙ : (a : Rₘ) → Sₙ) ((algebraMap R Rₘ : (a : R) → Rₘ) x : Rₘ) : Sₙ) :
      Sₙ')
    ((algebraMap Rₘ' Sₙ' : (a : Rₘ') → Sₙ') ((algebraMap R Rₘ' : (a : R) → Rₘ') x : Rₘ') : Sₙ')
⊢ Eq.{u_7 + 1} (α := Sₙ')
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv N Sₙ Sₙ') : Sₙ →+* Sₙ') (algebraMap Rₘ Sₙ))
            (algebraMap R Rₘ) :
          (a : R) → Sₙ')
        x :
      Sₙ')
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ' Sₙ')
              (↑(algEquiv M Rₘ Rₘ') : Rₘ →+* Rₘ'))
            (algebraMap R Rₘ) :
          (a : R) → Sₙ')
        x :
      Sₙ')

Tactic:
simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes]

Premises used: RingHom.coe_coe, AlgEquiv.commutes, RingHom.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst_3 : CommSemiring Rₘ
inst_4 : CommSemiring Sₙ
inst_5 : CommSemiring Rₘ'
inst_6 : CommSemiring Sₙ'
inst_7 : Algebra R Rₘ
inst_8 : Algebra S Sₙ
inst_9 : Algebra R Rₘ'
inst_10 : Algebra S Sₙ'
inst_11 : Algebra R Sₙ
inst_12 : Algebra Rₘ Sₙ
inst_13 : Algebra Rₘ' Sₙ'
inst_14 : Algebra R Sₙ'
N : Submonoid S
inst_15 : IsLocalization M Rₘ
inst_16 : IsLocalization N Sₙ
inst_17 : IsLocalization M Rₘ'
inst_18 : IsLocalization N Sₙ'
inst_19 : IsScalarTower R Rₘ Sₙ
inst_20 : IsScalarTower R S Sₙ
inst_21 : IsScalarTower R Rₘ' Sₙ'
inst_22 : IsScalarTower R S Sₙ'
x : R
rw :
  Eq.{u_7 + 1} (α := Sₙ') ((algEquiv N Sₙ Sₙ' : (a : Sₙ) → Sₙ') ((algebraMap R Sₙ : (a : R) → Sₙ) x : Sₙ) : Sₙ')
    ((algebraMap Rₘ' Sₙ' : (a : Rₘ') → Sₙ') ((algebraMap R Rₘ' : (a : R) → Rₘ') x : Rₘ') : Sₙ')
rw₁ :
  Eq.{u_7 + 1} (α := Sₙ') ((algEquiv N Sₙ Sₙ' : (a : Sₙ) → Sₙ') ((algebraMap R Sₙ : (a : R) → Sₙ) x : Sₙ) : Sₙ')
    ((algebraMap R Sₙ' : (a : R) → Sₙ') x : Sₙ')
rw₂ :
  Eq.{u_7 + 1} (α := Sₙ')
    ((AlgEquiv.restrictScalars R (algEquiv N Sₙ Sₙ') : (a : Sₙ) → Sₙ') ((algebraMap R Sₙ : (a : R) → Sₙ) x : Sₙ) : Sₙ')
    ((algebraMap R Sₙ' : (a : R) → Sₙ') x : Sₙ')
rw₃ rw₄ :
  Eq.{u_7 + 1} (α := Sₙ') ((algebraMap R Sₙ' : (a : R) → Sₙ') x : Sₙ') ((algebraMap R Sₙ' : (a : R) → Sₙ') x : Sₙ')
⊢ Eq.{u_7 + 1} (α := Sₙ')
    ((algEquiv N Sₙ Sₙ' : (a : Sₙ) → Sₙ')
        ((algebraMap Rₘ Sₙ : (a : Rₘ) → Sₙ) ((algebraMap R Rₘ : (a : R) → Rₘ) x : Rₘ) : Sₙ) :
      Sₙ')
    ((algebraMap Rₘ' Sₙ' : (a : Rₘ') → Sₙ') ((algebraMap R Rₘ' : (a : R) → Rₘ') x : Rₘ') : Sₙ')

Tactic:
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
    ← AlgEquiv.restrictScalars_apply R, AlgEquiv.commutes]

Premises used: AlgEquiv.commutes, AlgEquiv.restrictScalars_apply, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₘ : Type u_4
Sₙ : Type u_5
Rₘ' : Type u_6
Sₙ' : Type u_7
inst_3 : CommSemiring Rₘ
inst_4 : CommSemiring Sₙ
inst_5 : CommSemiring Rₘ'
inst_6 : CommSemiring Sₙ'
inst_7 : Algebra R Rₘ
inst_8 : Algebra S Sₙ
inst_9 : Algebra R Rₘ'
inst_10 : Algebra S Sₙ'
inst_11 : Algebra R Sₙ
inst_12 : Algebra Rₘ Sₙ
inst_13 : Algebra Rₘ' Sₙ'
inst_14 : Algebra R Sₙ'
N : Submonoid S
inst_15 : IsLocalization M Rₘ
inst_16 : IsLocalization N Sₙ
inst_17 : IsLocalization M Rₘ'
inst_18 : IsLocalization N Sₙ'
inst_19 : IsScalarTower R Rₘ Sₙ
inst_20 : IsScalarTower R S Sₙ
inst_21 : IsScalarTower R Rₘ' Sₙ'
inst_22 : IsScalarTower R S Sₙ'
x : Rₘ
rw rw₁ :
  Eq.{u_7 + 1} (α := Sₙ')
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ' Sₙ') (↑(algEquiv M Rₘ Rₘ') : Rₘ →+* Rₘ') :
          (a : Rₘ) → Sₙ')
        x :
      Sₙ')
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ' Sₙ') (↑(algEquiv M Rₘ Rₘ') : Rₘ →+* Rₘ') :
          (a : Rₘ) → Sₙ')
        x :
      Sₙ')
⊢ Eq.{u_7 + 1} (α := Sₙ')
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv N Sₙ Sₙ') : Sₙ →+* Sₙ') (algebraMap Rₘ Sₙ) :
          (a : Rₘ) → Sₙ')
        x :
      Sₙ')
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ' Sₙ') (↑(algEquiv M Rₘ Rₘ') : Rₘ →+* Rₘ') :
          (a : Rₘ) → Sₙ')
        x :
      Sₙ')

Tactic:
rw [algEquiv_comp_algebraMap M Rₘ Sₙ Rₘ']

Premises used: IsLocalization.algEquiv_comp_algebraMap
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
m : ℕ
⊢ Eq.{u_1 + 1} (α := Localization (M := R) M) (mk (↑m : R) 1) (↑m : Localization M)

Tactic:
simpa using mk_algebraMap (R := R) (A := ℕ) _

Premises used: Localization.mk_algebraMap
-- Module: Mathlib.RingTheory.Localization.Basic
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
x : R
y : ↥M
⊢ (algEquiv M S : (a : Localization M) → S) (mk' (Localization (M := R) M) x y) = mk' S x y

Tactic:
algEquiv_mk' _ _

Premises used: IsLocalization.algEquiv_mk'
-- Module: Mathlib.RingTheory.Localization.Basic
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
x : R
y : ↥M
⊢ Eq (α := Localization (M := R) M)
    (((AlgEquiv.symm (algEquiv M S) : S ≃ₐ[R] Localization (M := R) M) : (a : S) → Localization M) (mk' S x y) :
      Localization (M := R) M)
    (mk' (Localization (M := R) M) x y : Localization (M := R) M)

Tactic:
algEquiv_symm_mk' _ _

Premises used: IsLocalization.algEquiv_symm_mk'
-- Module: Mathlib.RingTheory.Localization.Basic
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
x : R
y : ↥M
rw : (algEquiv M S : (a : Localization M) → S) (mk' (Localization (M := R) M) x y) = mk' S x y
rw₁ rw₂ : mk' S x y = mk' S x y
⊢ (algEquiv M S : (a : Localization M) → S) (mk x y) = mk' S x y

Tactic:
rw [mk_eq_mk', algEquiv_mk']

Premises used: Localization.mk_eq_mk', Localization.algEquiv_mk'
-- Module: Mathlib.RingTheory.Localization.Basic
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
x : R
y : ↥M
rw :
  Eq (α := Localization (M := R) M)
    (((AlgEquiv.symm (algEquiv M S) : S ≃ₐ[R] Localization (M := R) M) : (a : S) → Localization M) (mk' S x y) :
      Localization (M := R) M)
    (mk' (Localization (M := R) M) x y : Localization (M := R) M)
rw₁ rw₂ : Eq (α := Localization (M := R) M) (mk' (Localization (M := R) M) x y) (mk' (Localization (M := R) M) x y)
⊢ Eq.{u_1 + 1} (α := Localization (M := R) M)
    (((AlgEquiv.symm (algEquiv M S) : S ≃ₐ[R] Localization (M := R) M) : (a : S) → Localization M) (mk' S x y) :
      Localization (M := R) M)
    (mk x y : Localization (M := R) M)

Tactic:
rw [mk_eq_mk', algEquiv_symm_mk']

Premises used: Localization.mk_eq_mk', Localization.algEquiv_symm_mk'
-- Module: Mathlib.RingTheory.Localization.Basic
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
⊢ Eq (α := RingHom.{u_1, u_2} (Localization (M := R) M) S) (↑(algEquiv M S) : Localization M →+* S)
    (map (M := M) (T := M) S (RingHom.id R) ⋯)

Tactic:
rfl

Premises used: IsLocalization.map, MonoidHomClass.toMonoidHom, IsLocalization.lift, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
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
⊢ Eq (α := RingHom.{u_2, u_1} S (Localization (M := R) M)) (↑(AlgEquiv.symm (algEquiv M S)) : S →+* Localization M)
    (map (M := M) (T := M) (Localization (M := R) M) (RingHom.id R) ⋯)

Tactic:
rfl

Premises used: IsLocalization.map, MonoidHomClass.toMonoidHom, IsLocalization.lift, RingHomClass.toRingHom, OreLocalization.liftExpand, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hM : 0 ∉ M
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
⊢ M ≤ nonZeroDivisors R

Tactic:
replace hM := le_nonZeroDivisors_of_noZeroDivisors hM
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
⊢ Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := Rₘ) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ)

Tactic:
⟨IsLocalization.injective _ hM, fun x => ?_⟩

Premises used: IsLocalization.injective, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
refine : ∀ (x : Rₘ), ∃ (a : R), (algebraMap R Rₘ : (a : R) → Rₘ) a = x
⊢ Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := Rₘ) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ)

Tactic:
refine ⟨IsLocalization.injective _ hM, fun x => ?_⟩
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
x : Rₘ
obtain :
  ∀ (r m : R) (hm : m ∈ M),
    ∃ (a : R), (algebraMap R Rₘ : (a : R) → Rₘ) a = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
⊢ ∃ (a : R), (algebraMap R Rₘ : (a : R) → Rₘ) a = x

Tactic:
obtain ⟨r, ⟨m, hm⟩, rfl⟩ := exists_mk'_eq M x

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
obtain :
  ∀ (n : R) (hn : m * n = 1),
    ∃ (a : R), (algebraMap R Rₘ : (a : R) → Rₘ) a = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
⊢ ∃ (a : R), (algebraMap R Rₘ : (a : R) → Rₘ) a = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)

Tactic:
obtain ⟨n, hn⟩ := hR.mul_inv_cancel (nonZeroDivisors.ne_zero <| hM hm)

Premises used: nonZeroDivisors.ne_zero, IsField.mul_inv_cancel
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
rw :
  HMul.hMul (α := Rₘ) (β := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n) : Rₘ)
      ((algebraMap R Rₘ : (a : R) → Rₘ) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) : Rₘ) =
    (algebraMap R Rₘ : (a : R) → Rₘ) r
rw₁ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R)) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₂ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * (n * (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R))) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₃ :
  Eq.{u_5 + 1} (α := Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) (r * ((↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm) : R) * n)) : Rₘ)
    ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₄ : Eq.{u_5 + 1} (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) (r * 1) : Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
rw₅ rw₆ : Eq.{u_5 + 1} (α := Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ) ((algebraMap R Rₘ : (a : R) → Rₘ) r : Rₘ)
⊢ (algebraMap R Rₘ : (a : R) → Rₘ) (r * n) = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)

Tactic:
rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]

Premises used: mul_assoc, map_mul, mul_comm, mul_one, IsLocalization.eq_mk'_iff_mul_eq
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
Rₘ : Type u_5
inst : CommRing R
inst_1 : CommRing Rₘ
M : Submonoid R
hR : IsField R
inst_2 : Algebra R Rₘ
inst_3 : IsLocalization M Rₘ
this : Field R := hR.toField
hM : M ≤ nonZeroDivisors R
r m : R
hm : m ∈ M
n : R
hn : m * n = 1
⊢ ∃ (a : R), (algebraMap R Rₘ : (a : R) → Rₘ) a = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)

Tactic:
exact ⟨r * n, by rw [eq_mk'_iff_mul_eq, ← map_mul, mul_assoc, _root_.mul_comm n, hn, mul_one]⟩
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
K : Type u_4
Kₘ : Type u_5
inst : Field K
inst_1 : CommRing Kₘ
M : Submonoid K
hM : 0 ∉ M
inst_2 : Algebra K Kₘ
inst_3 : IsLocalization M Kₘ
⊢ Bijective.{u_4 + 1, u_5 + 1} (α := K) (β := Kₘ) (⇑(algebraMap K Kₘ) : (a : K) → Kₘ)

Tactic:
(Field.toIsField K).localization_map_bijective hM

Premises used: IsField.localization_map_bijective, Field.toIsField
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst_3 : CommSemiring Rₘ
inst_4 : CommSemiring Sₘ
inst_5 : Algebra R Rₘ
inst_6 : IsLocalization M Rₘ
inst_7 : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_8 : Algebra R Sₘ
inst_9 : IsScalarTower R S Sₘ
this : Algebra Rₘ Sₘ := localizationAlgebra M S
⊢ Eq (α := R →+* Sₘ) (algebraMap R Sₘ)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Rₘ Sₘ) (algebraMap R Rₘ))

Tactic:
simp [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_eq R S Sₘ]

Premises used: IsScalarTower.algebraMap_eq, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M N : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
Rₘ : Type u_4
Sₘ : Type u_5
inst_4 : CommSemiring Rₘ
inst_5 : CommSemiring Sₘ
inst_6 : Algebra R Rₘ
inst_7 : IsLocalization M Rₘ
inst_8 : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
⊢ IsScalarTower.{u_1, u_1, u_2} R (Localization (M := R) M) (Localization (M := S) (Algebra.algebraMapSubmonoid S M))

Tactic:
isScalarTower_localizationAlgebra _ _

Premises used: isScalarTower_localizationAlgebra
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Sₘ : Type u_5
inst_3 : CommSemiring Sₘ
inst_4 : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
y : ↥M
rw : IsUnit.{u_5} (M := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) (↑y : R) : S) : Sₘ)
⊢ IsUnit.{u_5} (M := Sₘ) ((algebraMap R Sₘ : (a : R) → Sₘ) (↑y : R) : Sₘ)

Tactic:
rw [IsScalarTower.algebraMap_apply _ S]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
Sₘ : Type u_5
inst_3 : CommSemiring Sₘ
inst_4 : Algebra S Sₘ
i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
y : ↥M
⊢ IsUnit.{u_5} (M := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) ((algebraMap R S : (a : R) → S) (↑y : R) : S) : Sₘ)

Tactic:
IsLocalization.map_units Sₘ ⟨algebraMap R S y, Algebra.mem_algebraMapSubmonoid_of_mem y⟩

Premises used: Algebra.algebraMap, Subtype.mk, IsLocalization.map_units, Subtype.val, DFunLike.coe, Algebra.mem_algebraMapSubmonoid_of_mem