awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_4
L : Type u_5
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra R K
inst_8 : Algebra R L
inst_9 : Algebra S L
inst_10 : Algebra.IsAlgebraic R S
inst_11 : IsFractionRing S L
inst_12 : Algebra K L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
h : (↑(Ideal.span {a}) : Set S) ⊆ (↑(Submodule.span R b) : Set S)
y' : S
z' : ↥(S⁰ : Submonoid S)
hx :
  HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) a : L) (mk' L y' z') ∈
    (↑(Ideal.span (singleton (α := L) ((algebraMap S L : (a : S) → L) a : L))) : Set L)
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = (↑z' : S) * y
injRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
hz0' : Membership.mem (α := S) (γ := Submonoid S) S⁰ ((algebraMap R S : (a : R) → S) z : S)
mk_yz_eq :
  mk' L y' z' =
    mk' (M := S⁰) L y
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (S⁰ : Submonoid S) x)
        ((algebraMap R S : (a : R) → S) z) hz0')
rw :
  Membership.mem (α := L)
    (↑(Submodule.map
          ((↑R :
              {S M : Type u_2} →
                {M₂ : Type u_5} →
                  [inst : Semiring R] →
                    [inst_15 : Semiring S] →
                      [inst_16 : AddCommMonoid M] →
                        [inst_17 : AddCommMonoid M₂] →
                          [inst_18 : Module R M] →
                            [inst_19 : Module R M₂] →
                              [inst_20 : Module S M] →
                                [inst_21 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Algebra.linearMap S L))
          (Submodule.span R b)) :
      Set L)
    ((algebraMap S L : (a : S) → L) (a * y) : L)
⊢ Membership.mem (α := L) (↑(Submodule.span R ((⇑(algebraMap S L) : (a : S) → L) '' b)) : Set L)
    ((algebraMap S L : (a : S) → L) (a * y) : L)

Tactic:
rw [Submodule.span_algebraMap_image_of_tower]

Premises used: Submodule.span_algebraMap_image_of_tower
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_4
L : Type u_5
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra R K
inst_8 : Algebra R L
inst_9 : Algebra S L
inst_10 : Algebra.IsAlgebraic R S
inst_11 : IsFractionRing S L
inst_12 : Algebra K L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
h : (↑(Ideal.span {a}) : Set S) ⊆ (↑(Submodule.span R b) : Set S)
y' : S
z' : ↥(S⁰ : Submonoid S)
hx :
  HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) a : L) (mk' L y' z') ∈
    (↑(Ideal.span (singleton (α := L) ((algebraMap S L : (a : S) → L) a : L))) : Set L)
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = (↑z' : S) * y
injRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
hz0' : Membership.mem (α := S) (γ := Submonoid S) S⁰ ((algebraMap R S : (a : R) → S) z : S)
mk_yz_eq :
  mk' L y' z' =
    mk' (M := S⁰) L y
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (S⁰ : Submonoid S) x)
        ((algebraMap R S : (a : R) → S) z) hz0')
⊢ Membership.mem (α := L)
    (↑(Submodule.map
          ((↑R :
              {S M : Type u_2} →
                {M₂ : Type u_5} →
                  [inst : Semiring R] →
                    [inst_15 : Semiring S] →
                      [inst_16 : AddCommMonoid M] →
                        [inst_17 : AddCommMonoid M₂] →
                          [inst_18 : Module R M] →
                            [inst_19 : Module R M₂] →
                              [inst_20 : Module S M] →
                                [inst_21 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Algebra.linearMap S L))
          (Submodule.span R b)) :
      Set L)
    ((algebraMap S L : (a : S) → L) (a * y) : L)

Tactic:
Submodule.mem_map_of_mem (f := LinearMap.restrictScalars _ _)
    (h (Ideal.mem_span_singleton.mpr ⟨y, rfl⟩))

Premises used: Iff.mpr, Set.Mem, Exists.intro, Submodule.mem_map_of_mem, Ideal.mem_span_singleton, rfl
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_4
L : Type u_5
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra R K
inst_8 : Algebra R L
inst_9 : Algebra S L
inst_10 : Algebra.IsAlgebraic R S
inst_11 : IsFractionRing S L
inst_12 : Algebra K L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
a : S
b : Set S
inj : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
h : (↑(Ideal.span {a}) : Set S) ⊆ (↑(Submodule.span R b) : Set S)
y' : S
z' : ↥(S⁰ : Submonoid S)
hx :
  HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) a : L) (mk' L y' z') ∈
    (↑(Ideal.span (singleton (α := L) ((algebraMap S L : (a : S) → L) a : L))) : Set L)
y : S
z : R
hz0 : z ≠ 0
yz_eq : z • y' = (↑z' : S) * y
injRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
hz0' : Membership.mem (α := S) (γ := Submonoid S) S⁰ ((algebraMap R S : (a : R) → S) z : S)
mk_yz_eq :
  mk' L y' z' =
    mk' (M := S⁰) L y
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (S⁰ : Submonoid S) x)
        ((algebraMap R S : (a : R) → S) z) hz0')
⊢ Membership.mem (α := L)
    (↑(Submodule.map
          ((↑R :
              {S M : Type u_2} →
                {M₂ : Type u_5} →
                  [inst : Semiring R] →
                    [inst_15 : Semiring S] →
                      [inst_16 : AddCommMonoid M] →
                        [inst_17 : AddCommMonoid M₂] →
                          [inst_18 : Module R M] →
                            [inst_19 : Module R M₂] →
                              [inst_20 : Module S M] →
                                [inst_21 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            (Algebra.linearMap S L))
          (Submodule.span R b)) :
      Set L)
    ((algebraMap S L : (a : S) → L) (a * y) : L)

Tactic:
exact Submodule.mem_map_of_mem (f := LinearMap.restrictScalars _ _)
    (h (Ideal.mem_span_singleton.mpr ⟨y, rfl⟩))

Premises used: Iff.mpr, Exists.intro, Submodule.mem_map_of_mem, Ideal.mem_span_singleton, rfl
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
isAlgebraic : ∀ (x : L), IsAlgebraic K x
⊢ Algebra.IsAlgebraic K L

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : L
isAlgebraic : ∀ (x : S) (s : ↥(S⁰ : Submonoid S)), IsAlgebraic K (mk' L x s)
⊢ IsAlgebraic K x

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S⁰ x

Premises used: nonZeroDivisors, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
isAlgebraic : IsIntegral K (mk' L x s)
⊢ IsAlgebraic K (mk' L x s)

Tactic:
apply IsIntegral.isAlgebraic

Premises used: IsIntegral.isAlgebraic
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
isAlgebraic : IsIntegral K (HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) x : L) (mk' L 1 s))
⊢ IsIntegral K (mk' L x s)

Tactic:
rw [IsLocalization.mk'_eq_mul_mk'_one]

Premises used: IsLocalization.mk'_eq_mul_mk'_one
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
isAlgebraic : RingHom.IsIntegralElem (algebraMap K L) ((algebraMap S L : (a : S) → L) x)
isAlgebraic₁ : RingHom.IsIntegralElem (algebraMap K L) (mk' L 1 s)
⊢ IsIntegral K (HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) x : L) (mk' L 1 s))

Tactic:
apply RingHom.IsIntegralElem.mul

Premises used: RingHom.IsIntegralElem.mul
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
isAlgebraic : IsIntegral.{u_5, u_8} R (A := L) ((algebraMap S L : (a : S) → L) x : L)
⊢ RingHom.IsIntegralElem (algebraMap K L) ((algebraMap S L : (a : S) → L) x)

Tactic:
apply IsIntegral.tower_top (R := R)

Premises used: IsIntegral.tower_top
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
isAlgebraic : IsIntegral R x
⊢ IsIntegral.{u_5, u_8} R (A := L) ((algebraMap S L : (a : S) → L) x : L)

Tactic:
apply IsIntegral.map (IsScalarTower.toAlgHom R S L)

Premises used: IsScalarTower.toAlgHom, IsIntegral.map
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
⊢ IsIntegral R x

Tactic:
Algebra.IsIntegral.isIntegral x

Premises used: Algebra.IsIntegral.isIntegral
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
⊢ IsIntegral R x

Tactic:
exact Algebra.IsIntegral.isIntegral x

Premises used: Algebra.IsIntegral.isIntegral
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
isAlgebraic : IsIntegral K (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (mk' L 1 s) _)
⊢ IsIntegral K (mk' L 1 s)

Tactic:
rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral]

Premises used: IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
isAlgebraic : IsIntegral R (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (mk' L 1 s) _)
⊢ IsIntegral K (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (mk' L 1 s) _)

Tactic:
apply IsIntegral.tower_top (R := R)

Premises used: IsIntegral.tower_top
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
isAlgebraic : IsIntegral R (↑s : S)
⊢ IsIntegral R (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (mk' L 1 s) _)

Tactic:
apply IsIntegral.map (IsScalarTower.toAlgHom R S L)

Premises used: IsScalarTower.toAlgHom, IsIntegral.map
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
⊢ IsIntegral R (↑s : S)

Tactic:
Algebra.IsIntegral.isIntegral (s : S)

Premises used: Algebra.IsIntegral.isIntegral, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Integral
Goal:
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Field K
inst_3 : CommRing L
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : Algebra S L
inst_8 : Algebra K L
inst_9 : IsScalarTower R S L
inst_10 : IsScalarTower R K L
inst_11 : IsFractionRing S L
inst_12 : Algebra.IsIntegral R S
x : S
s : ↥(S⁰ : Submonoid S)
⊢ IsIntegral R (↑s : S)

Tactic:
exact Algebra.IsIntegral.isIntegral (s : S)

Premises used: Algebra.IsIntegral.isIntegral, Subtype.val
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : R
ha : a ∈ (↑M : Set R)
⊢ Membership.mem (α := S) (γ := Submonoid S) (IsUnit.submonoid S) ((algebraMap R S : (a : R) → S) a : S)

Tactic:
IsLocalization.map_units S ⟨_, ha⟩

Premises used: Set.Mem, setOf, IsUnit, Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
a : R
ha : a ∈ (↑M : Set R)
⊢ Membership.mem (α := S) (γ := Submonoid S) (IsUnit.submonoid S) ((algebraMap R S : (a : R) → S) a : S)

Tactic:
exact IsLocalization.map_units S ⟨_, ha⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := ↥M) (β := ↥(invSubmonoid M S))
    (⇑(toInvSubmonoid M S) : (a : ↥M) → ↥(invSubmonoid M S))

Tactic:
Function.Surjective.comp (β := M.map (algebraMap R S))
    (Equiv.surjective (equivInvSubmonoid _ _).toEquiv) (MonoidHom.submonoidMap_surjective _ _)

Premises used: IsLocalization.equivInvSubmonoid, MulEquiv.toEquiv, Function.Surjective.comp, Equiv.surjective, MonoidHom.submonoidMap_surjective
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
⊢ HMul.hMul (α := S) (β := S)
      ((↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) :
          S) :
        S)
      ((algebraMap R S : (a : R) → S) (↑m : R) : S) =
    1

Tactic:
Submonoid.leftInvEquiv_symm_mul _ (submonoid_map_le_is_unit _ _) _

Premises used: Submonoid.leftInvEquiv_symm_mul
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      ((↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) :
          S) :
        S) =
    1

Tactic:
Submonoid.mul_leftInvEquiv_symm _ (submonoid_map_le_is_unit _ _) ⟨_, _⟩

Premises used: Subtype.mk, Submonoid.mul_leftInvEquiv_symm
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      ((↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) :
          S) :
        S) =
    1

Tactic:
mul_toInvSubmonoid M S m

Premises used: IsLocalization.mul_toInvSubmonoid
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
h : Eq (α := S → S) (HSMul.hSMul m) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S))
⊢ HSMul.hSMul (β := S) m
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S) =
    1

Tactic:
convert! mul_toInvSubmonoid M S m

Premises used: IsLocalization.mul_toInvSubmonoid
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
h : ∀ (x : S), m • x = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S) x
⊢ Eq (α := S → S) (HSMul.hSMul m) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S))

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
x : S
h : m • x = (↑m : R) • x
⊢ m • x = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S) x

Tactic:
rw [← Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
x : S
⊢ m • x = (↑m : R) • x

Tactic:
rfl
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
rcases :
  ∀ (r : R) (m : ↥M)
    (e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) r),
    ∃ (r : R) (m : ↥M),
      z =
        HSMul.hSMul (β := S) r
          (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) :
            S)
⊢ ∃ (r : R) (m : ↥M),
    z =
      HSMul.hSMul (β := S) r
        (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S)

Tactic:
rcases IsLocalization.surj M z with ⟨⟨r, m⟩, e : z * _ = algebraMap R S r⟩

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
r : R
m : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) r
⊢ ∃ (r : R) (m : ↥M),
    z =
      HSMul.hSMul (β := S) r
        (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S)

Tactic:
⟨r, m, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
r : R
m : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) r
refine :
  z =
    HSMul.hSMul (β := S) r
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S)
⊢ ∃ (r : R) (m : ↥M),
    z =
      HSMul.hSMul (β := S) r
        (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S)

Tactic:
refine ⟨r, m, ?_⟩
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
r : R
m : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) r
rw :
  z =
    z *
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)
        ((↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) :
            S) :
          S)
⊢ z =
    HSMul.hSMul (β := S) r
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S)

Tactic:
rw [Algebra.smul_def, ← e, mul_assoc]

Premises used: mul_assoc, Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.InvSubmonoid
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
r : R
m : ↥M
e : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) r
⊢ z =
    z *
      HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)
        ((↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) :
            S) :
          S)

Tactic:
simp