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
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
have injRS : Function.Injective (algebraMap R S) := by
    refine
      Function.Injective.of_comp (show Function.Injective (algebraMap S L ∘ algebraMap R S) from ?_)
    rwa [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq]
-- 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)
⊢ Membership.mem (α := S) (γ := Submonoid S) S⁰ ((algebraMap R S : (a : R) → S) z : S)

Tactic:
have hz0' : algebraMap R S z ∈ S⁰ :=
    map_mem_nonZeroDivisors (algebraMap R S) injRS (mem_nonZeroDivisors_of_ne_zero hz0)
-- 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)
⊢ HMul.hMul (β := S) y' ((algebraMap R S : (a : R) → S) z : S) = y * (↑z' : S)

Tactic:
rw [Algebra.smul_def, mul_comm _ y, mul_comm _ y'] at yz_eq

Premises used: mul_comm, Algebra.smul_def
-- 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)
yz_eq₁ : HMul.hMul (β := S) y' ((algebraMap R S : (a : R) → S) z : S) = y * (↑z' : S)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
rw [Algebra.smul_def, mul_comm _ y, mul_comm _ y'] at yz_eq

Premises used: mul_comm, Algebra.smul_def
-- 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)
yz_eq₁ : HMul.hMul (β := S) y' ((algebraMap R S : (a : R) → S) z : S) = y * (↑z' : S)
injRS₁ : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Membership.mem (α := S) (γ := Submonoid S) S⁰ ((algebraMap R S : (a : R) → S) z : S)

Tactic:
rw [Algebra.smul_def, mul_comm _ y, mul_comm _ y'] at yz_eq

Premises used: mul_comm, Algebra.smul_def
-- 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 : HMul.hMul (β := S) y' ((algebraMap R S : (a : R) → S) z : S) = y * (↑z' : S)
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)
rw :
  y * (↑z' : S) =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (S⁰ : Submonoid S) x)
              ((algebraMap R S : (a : R) → S) z) hz0') :
          S) :
        S)
      y'
rw₁ :
  y * (↑z' : S) =
    HMul.hMul (β := S) y'
      ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (S⁰ : Submonoid S) x)
              ((algebraMap R S : (a : R) → S) z) hz0') :
          S) :
        S)
rw₂ rw₃ : y * (↑z' : S) = y * (↑z' : S)
⊢ (↑z' : S) * y =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (S⁰ : Submonoid S) x)
              ((algebraMap R S : (a : R) → S) z) hz0') :
          S) :
        S)
      y'

Tactic:
rw [mul_comm _ y, mul_comm _ y', yz_eq]

Premises used: mul_comm
-- 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 : HMul.hMul (β := S) y' ((algebraMap R S : (a : R) → S) z : S) = y * (↑z' : S)
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' 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')

Tactic:
exact IsLocalization.mk'_eq_of_eq (by rw [mul_comm _ y, mul_comm _ y', yz_eq])

Premises used: IsLocalization.mk'_eq_of_eq
-- 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' 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')

Tactic:
have mk_yz_eq : IsLocalization.mk' L y' z' = IsLocalization.mk' L y ⟨_, hz0'⟩ := by
    rw [Algebra.smul_def, mul_comm _ y, mul_comm _ y'] at yz_eq
    exact IsLocalization.mk'_eq_of_eq (by rw [mul_comm _ y, mul_comm _ y', yz_eq])
-- 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')
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)
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)
⊢ 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)

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]

Premises used: IsFractionRing.mk'_eq_div, mul_assoc, map_inv₀, div_eq_mul_inv, map_mul, mul_comm, Algebra.smul_def, IsScalarTower.algebraMap_apply
-- 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')
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)
⊢ 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:
(Submodule.span K _).smul_mem _ hy

Premises used: Set.Mem, Submodule.span, Submodule.smul_mem
-- 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')
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)
⊢ 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:
exact (Submodule.span K _).smul_mem _ hy

Premises used: Submodule.span, Submodule.smul_mem
-- 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')
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)
⊢ 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)

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
-- 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.{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:
Submodule.span_subset_span R K _ ?_

Premises used: Submodule.span_subset_span
-- 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')
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)
⊢ 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:
refine Submodule.span_subset_span R K _ ?_

Premises used: Submodule.span_subset_span