awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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')
hy :
  Membership.mem.{u_5, u_5} (α := L) (γ := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b))
    ((algebraMap S L : (a : S) → L) (a * y) : L)
⊢ HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) a : L) (mk' L y' z') ∈
    (↑(Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) : Set L)
have rw : HSMul.hSMul.{u_4, u_5, u_5} (α := K) (β := L) (((algebraMap R K : (a : R) → K) z)⁻¹ : K)
    ((algebraMap S L : (a : S) → L) (a * y) : L) ∈
  (↑(Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) : Set L)
Tactic: rw [mk_yz_eq, IsFractionRing.mk'_eq_div, ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R K L, div_eq_mul_inv, ← mul_assoc, mul_comm, ← map_inv₀, ←
      Algebra.smul_def, ← map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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')
⊢ HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) a : L) (mk' L y' z') ∈
    (↑(Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) : Set L)
have suffices : Membership.mem.{u_5, u_5} (α := L) (γ := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b))
  ((algebraMap S L : (a : S) → L) (a * y) : L)
Tactic: suffices hy : algebraMap S L (a * y) ∈ Submodule.span K ((algebraMap S L) '' b) by
    rw [mk_yz_eq, IsFractionRing.mk'_eq_div, ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R K L, div_eq_mul_inv, ← mul_assoc, mul_comm, ← map_inv₀, ←
      Algebra.smul_def, ← map_mul]
    exact (Submodule.span K _).smul_mem _ hy
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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.{u_5, u_5} (α := L) (γ := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b))
    ((algebraMap S L : (a : S) → L) (a * y) : L)
have refine : 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: refine Submodule.span_subset_span R K _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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.span R ((⇑(algebraMap S L) : (a : S) → L) '' b)) : Set L)
    ((algebraMap S L : (a : S) → L) (a * y) : L)
have 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)
Tactic: rw [Submodule.span_algebraMap_image_of_tower]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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
⊢ Algebra.IsAlgebraic K L
have isAlgebraic : ∀ (x : L), IsAlgebraic K x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 K x
have isAlgebraic : ∀ (x : S) (s : ↥(S⁰ : Submonoid S)), IsAlgebraic K (mk' L x s)
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S⁰ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 K (mk' L x s)
have isAlgebraic : IsIntegral K (mk' L x s)
Tactic: apply IsIntegral.isAlgebraic
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 K (mk' L x s)
have isAlgebraic : IsIntegral K (HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) x : L) (mk' L 1 s))
Tactic: rw [IsLocalization.mk'_eq_mul_mk'_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 K (HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) x : L) (mk' L 1 s))
have isAlgebraic : RingHom.IsIntegralElem (algebraMap K L) ((algebraMap S L : (a : S) → L) x)
Tactic: apply RingHom.IsIntegralElem.mul
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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)
⊢ IsIntegral K (HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) x : L) (mk' L 1 s))
have isAlgebraic₁ : RingHom.IsIntegralElem (algebraMap K L) (mk' L 1 s)
Tactic: apply RingHom.IsIntegralElem.mul
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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)
⊢ RingHom.IsIntegralElem (algebraMap K L) ((algebraMap S L : (a : S) → L) x)
have isAlgebraic : IsIntegral.{u_5, u_8} R (A := L) ((algebraMap S L : (a : S) → L) x : L)
Tactic: apply IsIntegral.tower_top (R := R)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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.{u_5, u_8} R (A := L) ((algebraMap S L : (a : S) → L) x : L)
have isAlgebraic : IsIntegral R x
Tactic: apply IsIntegral.map (IsScalarTower.toAlgHom R S L)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 K (mk' L 1 s)
have isAlgebraic : IsIntegral K (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (mk' L 1 s) _)
Tactic: rw [← isAlgebraic_iff_isIntegral, ← IsAlgebraic.invOf_iff, isAlgebraic_iff_isIntegral]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 K (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (mk' L 1 s) _)
have isAlgebraic : IsIntegral R (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (mk' L 1 s) _)
Tactic: apply IsIntegral.tower_top (R := R)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
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 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (mk' L 1 s) _)
have isAlgebraic : IsIntegral R (↑s : S)
Tactic: apply IsIntegral.map (IsScalarTower.toAlgHom R S L)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
⊢ HSMul.hSMul (β := S) m
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S) =
    1
have h : Eq (α := S → S) (HSMul.hSMul m) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S))
Tactic: convert! mul_toInvSubmonoid M S m
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
⊢ Eq (α := S → S) (HSMul.hSMul m) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S))
have h : ∀ (x : S), m • x = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S) x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S) x
have h : m • x = (↑m : R) • x
Tactic: rw [← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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),
    z =
      HSMul.hSMul (β := S) r
        (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S)
have 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)
Tactic: rcases IsLocalization.surj M z with ⟨⟨r, m⟩, e : z * _ = algebraMap R S r⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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)
have 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)
Tactic: refine ⟨r, m, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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 =
    HSMul.hSMul (β := S) r
      (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S)
have 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)
Tactic: rw [Algebra.smul_def, ← e, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
x : ↥M
⊢ (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) x) : S) =
    mk' S 1 x
have rw : HMul.hMul (α := S) (β := S)
    ((↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) x) : S) :
      S)
    ((algebraMap R S : (a : R) → S) (↑x : R) : S) =
  HMul.hMul (β := S) (mk' S 1 x) ((algebraMap R S : (a : R) → S) (↑x : R) : S)
Tactic: rw [← (IsLocalization.map_units S x).mul_left_inj]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
x : S
⊢ Membership.mem (γ := Submonoid S) (invSubmonoid M S) x ↔ ∃ (m : ↥M), mk' S 1 m = x
have simp_rw : Membership.mem (γ := Submonoid S) (invSubmonoid M S) x ↔
  ∃ (m : ↥M),
    (↑(((toInvSubmonoid M S : MonoidHom.{u_1, u_2} ↥M ↥(invSubmonoid M S)) : (a : ↥M) → ↥(invSubmonoid M S)) m) : S) = x
Tactic: simp_rw [← toInvSubmonoid_eq_mk']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
⊢ Eq (α := Submodule R S) (Submodule.span R (↑(invSubmonoid M S) : Set S)) ⊤
have rw : LE.le (α := Submodule R S) ⊤ (Submodule.span R (↑(invSubmonoid M S) : Set S))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
x : S
⊢ Membership.mem (γ := Submodule R S) (Submodule.span R (↑(invSubmonoid M S) : Set S)) x
have rcases : ∀ (r : R) (m : ↥M),
  Membership.mem (γ := Submodule R S) (Submodule.span R (↑(invSubmonoid M S) : Set S))
    (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 x with ⟨r, m, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (hypothesis)
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
inst_4 : Monoid.FG.{u_1} ↥M
⊢ Algebra.FiniteType R S
have this : Monoid.FG.{u_2} ↥(invSubmonoid M S)
Tactic: have := Monoid.fg_of_surjective _ (toInvSubmonoid_surjective M S)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (hypothesis)
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
inst_4 : Monoid.FG.{u_1} ↥M
this : Monoid.FG.{u_2} ↥(invSubmonoid M S)
⊢ Algebra.FiniteType R S
have this₁ : Submonoid.FG (invSubmonoid M S)
Tactic: rw [Monoid.fg_iff_submonoid_fg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
inst_4 : Monoid.FG.{u_1} ↥M
this : Submonoid.FG (invSubmonoid M S)
⊢ Algebra.FiniteType R S
have rcases : ∀ (s : Finset S) (hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)),
  Algebra.FiniteType R S
Tactic: rcases this with ⟨s, hs⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
inst_4 : Monoid.FG.{u_1} ↥M
s : Finset S
hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)
⊢ Algebra.FiniteType R S
have refine : Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
Tactic: refine ⟨⟨s, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
inst_4 : Monoid.FG.{u_1} ↥M
s : Finset S
hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)
⊢ Eq (α := Subalgebra R S) (Algebra.adjoin R (↑s : Set S)) ⊤
have rw : LE.le (α := Subalgebra R S) ⊤ (Algebra.adjoin R (↑s : Set S))
Tactic: rw [eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.InvSubmonoid (goal)
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
inst_4 : Monoid.FG.{u_1} ↥M
s : Finset S
hs : Eq (α := Submonoid S) (Submonoid.closure (↑s : Set S)) (invSubmonoid M S)
x : S
⊢ x ∈
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) (Algebra.adjoin R (↑s : Set S)) :
          Submodule R S) :
      Set S)
have rw : x ∈ (↑⊤ : Set S)
Tactic: rw [Algebra.adjoin_eq_span, hs, span_invSubmonoid]