awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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₁)
      (HMul.hMul (α := 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₁)
        x)
      ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) =
    HMul.hMul (β := S₁)
      (HMul.hMul (α := 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₁)
        y)
      ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁)
have h : 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)) sorry) :
        S₁) :
      S₁)
    ((algebraMap R S₁ : (a : R) → S₁) r : 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)) sorry) :
        S₁) :
      S₁)
    ((algebraMap R S₁ : (a : R) → S₁) s : S₁)
Tactic: rw [mul_assoc, hr, mul_assoc, hs]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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₁) (β := 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₁) =
    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₁)
have h : 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)) sorry) :
          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)) sorry) :
          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: apply (map_units S₁ ⟨c, hmc⟩).mul_right_cancel
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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₁)
      (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₁)
have 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)) sorry) :
          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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
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ₘ'))
have 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ₙ')
Tactic: refine IsLocalization.ringHom_ext M (RingHom.ext fun x => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
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
⊢ 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ₙ')
have 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ₙ')
Tactic: simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
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
⊢ 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ₙ')
have 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ₙ')
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
    ← AlgEquiv.restrictScalars_apply R, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
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ₙ')
⊢ 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ₙ')
have 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ₙ')
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
    ← AlgEquiv.restrictScalars_apply R, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
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ₙ')
⊢ 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ₙ')
have 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ₙ')
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
    ← AlgEquiv.restrictScalars_apply R, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
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ₙ')
⊢ 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ₙ')
have rw₃ : Eq.{u_7 + 1} (α := Sₙ') ((algebraMap R Sₙ' : (a : R) → Sₙ') x : Sₙ') ((algebraMap R Sₙ' : (a : R) → Sₙ') x : Sₙ')
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
    ← AlgEquiv.restrictScalars_apply R, AlgEquiv.commutes]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
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ₘ
⊢ 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ₙ')
have 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ₙ')
Tactic: rw [algEquiv_comp_algebraMap M Rₘ Sₙ Rₘ']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
x : R
y : ↥M
⊢ (algEquiv M S : (a : Localization M) → S) (mk x y) = mk' S x y
have rw : (algEquiv M S : (a : Localization M) → S) (mk' (Localization (M := R) M) x y) = mk' S x y
Tactic: rw [mk_eq_mk', algEquiv_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
x : R
y : ↥M
rw : (algEquiv M S : (a : Localization M) → S) (mk' (Localization (M := R) M) x y) = mk' S x y
⊢ (algEquiv M S : (a : Localization M) → S) (mk x y) = mk' S x y
have rw₁ : mk' S x y = mk' S x y
Tactic: rw [mk_eq_mk', algEquiv_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
x : R
y : ↥M
⊢ 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)
have 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)
Tactic: rw [mk_eq_mk', algEquiv_symm_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
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)
⊢ 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)
have rw₁ : Eq (α := Localization (M := R) M) (mk' (Localization (M := R) M) x y) (mk' (Localization (M := R) M) x y)
Tactic: rw [mk_eq_mk', algEquiv_symm_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (hypothesis)
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
⊢ Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := Rₘ) (⇑(algebraMap R Rₘ) : (a : R) → Rₘ)
have hM₁ : M ≤ nonZeroDivisors R
Tactic: replace hM := le_nonZeroDivisors_of_noZeroDivisors hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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ₘ)
have refine : ∀ (x : Rₘ), ∃ (a : R), (algebraMap R Rₘ : (a : R) → Rₘ) a = x
Tactic: refine ⟨IsLocalization.injective _ hM, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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ₘ
⊢ ∃ (a : R), (algebraMap R Rₘ : (a : R) → Rₘ) a = x
have 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)
Tactic: obtain ⟨r, ⟨m, hm⟩, rfl⟩ := exists_mk'_eq M x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
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
⊢ ∃ (a : R), (algebraMap R Rₘ : (a : R) → Rₘ) a = mk' Rₘ r (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m hm)
have 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)
Tactic: obtain ⟨n, hn⟩ := hR.mul_inv_cancel (nonZeroDivisors.ne_zero <| hM hm)