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
Rf : Type u_5
Sf : Type u_6
inst_3 : CommRing Rf
inst_4 : CommRing Sf
inst_5 : Algebra R Rf
inst_6 : Algebra S Sf
inst_7 : Algebra Rf Sf
inst_8 : Algebra R Sf
inst_9 : IsScalarTower R S Sf
inst_10 : IsScalarTower R Rf Sf
f : R
inst_11 : Away f Rf
inst_12 : Away.{u_2, u_6} (R := S) ((algebraMap R S : (a : R) → S) f : S) Sf
inst_13 : Algebra.{u_2, u_6} ↥(integralClosure R S) ↥(integralClosure Rf Sf)
inst_14 : IsScalarTower.{u_2, u_6, u_6} (↥(integralClosure R S)) (↥(integralClosure Rf Sf)) Sf
inst_15 : IsScalarTower.{u_1, u_2, u_6} R ↥(integralClosure R S) ↥(integralClosure Rf Sf)
⊢ Eq.{u_2 + 1} (α := Submonoid ↥(integralClosure R S))
    (Submonoid.powers ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) f) :
      Submonoid ↥(integralClosure R S))
    (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) (Submonoid.powers f) : Submonoid ↥(integralClosure R S))

Tactic:
simp
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
simp : (∀ (x : S), IsAlgebraic R x) ↔ ∀ (x : K), IsAlgebraic R x
⊢ Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K

Tactic:
simp only [Algebra.isAlgebraic_def]

Premises used: Algebra.isAlgebraic_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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
mp : (∀ (x : S), IsAlgebraic R x) → ∀ (x : K), IsAlgebraic R x
mpr : (∀ (x : K), IsAlgebraic R x) → ∀ (x : S), IsAlgebraic R x
⊢ (∀ (x : S), IsAlgebraic R x) ↔ ∀ (x : K), IsAlgebraic R x

Tactic:
constructor
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
this_1 : Nontrivial S := ⋯
this : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
⊢ IsScalarTower R (FractionRing R) K

Tactic:
have := FractionRing.isScalarTower_liftAlgebra R K
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
mp : IsIntegral.{u_1, u_4} (FractionRing R) x
⊢ IsAlgebraic R x

Tactic:
rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]

Premises used: FractionRing, IsFractionRing.isAlgebraic_iff, isAlgebraic_iff_isIntegral
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
x : K
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
mp :
  ∀ (a b : S) (ha : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) b),
    IsIntegral.{u_1, u_4} (FractionRing R)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap S K : (a : S) → K) a : K) ((algebraMap S K : (a : S) → K) b : K))
⊢ IsIntegral.{u_1, u_4} (FractionRing R) x

Tactic:
obtain ⟨a : S, b, ha, rfl⟩ := div_surjective S x

Premises used: IsFractionRing.div_surjective, 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) b
mp :
  ∀ (f : R[X]) (hf₁ : f ≠ 0) (hf₂ : Eq.{u_2 + 1} (α := S) ((aeval b : (a : R[X]) → S) f : S) (0 : S)),
    IsIntegral.{u_1, u_4} (FractionRing R)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap S K : (a : S) → K) a : K) ((algebraMap S K : (a : S) → K) b : K))
⊢ IsIntegral.{u_1, u_4} (FractionRing R)
    (HDiv.hDiv (α := K) (β := K) ((algebraMap S K : (a : S) → K) a : K) ((algebraMap S K : (a : S) → K) b : K))

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := h b
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) b
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_2 + 1} (α := S) ((aeval b : (a : R[X]) → S) f : S) (0 : S)
mp :
  IsIntegral.{u_1, u_4} (FractionRing R)
    (HMul.hMul (α := K) (β := K) ((algebraMap S K : (a : S) → K) a : K) (((algebraMap S K : (a : S) → K) b)⁻¹ : K))
⊢ IsIntegral.{u_1, u_4} (FractionRing R)
    (HDiv.hDiv (α := K) (β := K) ((algebraMap S K : (a : S) → K) a : K) ((algebraMap S K : (a : S) → K) b : K))

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) b
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_2 + 1} (α := S) ((aeval b : (a : R[X]) → S) f : S) (0 : S)
⊢ IsIntegral.{u_1, u_4} (FractionRing R)
    (HMul.hMul (α := K) (β := K) ((algebraMap S K : (a : S) → K) a : K) (((algebraMap S K : (a : S) → K) b)⁻¹ : K))

Tactic:
.mul ?_ (.inv ?_)

Premises used: IsIntegral.mul, IsIntegral.inv
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) b
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_2 + 1} (α := S) ((aeval b : (a : R[X]) → S) f : S) (0 : S)
mp : IsIntegral.{u_1, u_4} (FractionRing R) (A := K) ((algebraMap S K : (a : S) → K) a : K)
mp₁ : IsIntegral.{u_1, u_4} (FractionRing R) (A := K) ((algebraMap S K : (a : S) → K) b : K)
⊢ IsIntegral.{u_1, u_4} (FractionRing R)
    (HMul.hMul (α := K) (β := K) ((algebraMap S K : (a : S) → K) a : K) (((algebraMap S K : (a : S) → K) b)⁻¹ : K))

Tactic:
refine .mul ?_ (.inv ?_)
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) b
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_2 + 1} (α := S) ((aeval b : (a : R[X]) → S) f : S) (0 : S)
⊢ IsIntegral.{u_1, u_4} (FractionRing R) (A := K) ((algebraMap S K : (a : S) → K) a : K)

Tactic:
isAlgebraic_iff_isIntegral.mp <|
      (h _).algebraMap.extendScalars (FaithfulSMul.algebraMap_injective R _)

Premises used: IsAlgebraic.extendScalars, FaithfulSMul.algebraMap_injective, Iff.mp, IsAlgebraic.algebraMap, isAlgebraic_iff_isIntegral
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) b
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_2 + 1} (α := S) ((aeval b : (a : R[X]) → S) f : S) (0 : S)
⊢ IsIntegral.{u_1, u_4} (FractionRing R) (A := K) ((algebraMap S K : (a : S) → K) a : K)

Tactic:
exact isAlgebraic_iff_isIntegral.mp <|
      (h _).algebraMap.extendScalars (FaithfulSMul.algebraMap_injective R _)

Premises used: IsAlgebraic.extendScalars, FaithfulSMul.algebraMap_injective, Iff.mp, IsAlgebraic.algebraMap, isAlgebraic_iff_isIntegral
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) b
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_2 + 1} (α := S) ((aeval b : (a : R[X]) → S) f : S) (0 : S)
⊢ IsIntegral.{u_1, u_4} (FractionRing R) (A := K) ((algebraMap S K : (a : S) → K) b : K)

Tactic:
isAlgebraic_iff_isIntegral.mp <|
      (h _).algebraMap.extendScalars (FaithfulSMul.algebraMap_injective R _)

Premises used: IsAlgebraic.extendScalars, FaithfulSMul.algebraMap_injective, Iff.mp, IsAlgebraic.algebraMap, isAlgebraic_iff_isIntegral
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : S), IsAlgebraic R x
this_1 : Nontrivial S := ⋯
this_2 : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
this : IsScalarTower R (FractionRing R) K
a b : S
ha : Membership.mem (γ := Submonoid S) (nonZeroDivisors S) b
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_2 + 1} (α := S) ((aeval b : (a : R[X]) → S) f : S) (0 : S)
⊢ IsIntegral.{u_1, u_4} (FractionRing R) (A := K) ((algebraMap S K : (a : S) → K) b : K)

Tactic:
exact isAlgebraic_iff_isIntegral.mp <|
      (h _).algebraMap.extendScalars (FaithfulSMul.algebraMap_injective R _)

Premises used: IsAlgebraic.extendScalars, FaithfulSMul.algebraMap_injective, Iff.mp, IsAlgebraic.algebraMap, isAlgebraic_iff_isIntegral
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
mpr :
  ∀ (f : R[X]) (hf₁ : f ≠ 0)
    (hf₂ :
      Eq.{u_4 + 1} (α := K) (((aeval ((algebraMap S K : (a : S) → K) x) : R[X] →ₐ[R] K) : (a : R[X]) → K) f : K)
        (0 : K)),
    IsAlgebraic R x
⊢ IsAlgebraic R x

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := h (algebraMap S K x)

Premises used: Algebra.algebraMap, DFunLike.coe
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_4 + 1} (α := K) (((aeval ((algebraMap S K : (a : S) → K) x) : R[X] →ₐ[R] K) : (a : R[X]) → K) f : K) (0 : K)
right : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
⊢ IsAlgebraic R x

Tactic:
use f, hf₁
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_4 + 1} (α := K) (((aeval ((algebraMap S K : (a : S) → K) x) : R[X] →ₐ[R] K) : (a : R[X]) → K) f : K) (0 : K)
⊢ Eq.{u_4 + 1} (α := K) ((algebraMap S K : (a : S) → K) ((aeval x : (a : R[X]) → S) f : S) : K) (0 : K)

Tactic:
rw [Polynomial.aeval_algebraMap_apply] at hf₂

Premises used: Polynomial.aeval_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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_4 + 1} (α := K) ((algebraMap S K : (a : S) → K) ((aeval x : (a : R[X]) → S) f : S) : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)

Tactic:
(injective_iff_map_eq_zero (algebraMap S K)).1 (FaithfulSMul.algebraMap_injective _ _) _
        hf₂

Premises used: Algebra.algebraMap, injective_iff_map_eq_zero, FaithfulSMul.algebraMap_injective, Iff.mp
-- 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
inst_3 : Field K
inst_4 : IsDomain R
inst_5 : Algebra R K
inst_6 : Algebra S K
inst_7 : Module.IsTorsionFree R K
inst_8 : IsFractionRing S K
inst_9 : IsScalarTower R S K
h : ∀ (x : K), IsAlgebraic R x
x : S
f : R[X]
hf₁ : f ≠ 0
hf₂ : Eq.{u_4 + 1} (α := K) ((algebraMap S K : (a : S) → K) ((aeval x : (a : R[X]) → S) f : S) : K) (0 : K)
⊢ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)

Tactic:
exact
      (injective_iff_map_eq_zero (algebraMap S K)).1 (FaithfulSMul.algebraMap_injective _ _) _
        hf₂

Premises used: Algebra.algebraMap, injective_iff_map_eq_zero, FaithfulSMul.algebraMap_injective, Iff.mp
-- 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)
x : L
hx : x ∈ (↑(Ideal.span (singleton (α := L) ((algebraMap S L : (a : S) → L) a : L))) : Set L)
obtain :
  ∀ (x' : L)
    (hx :
      HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) a : L) x' ∈
        (↑(Ideal.span (singleton (α := L) ((algebraMap S L : (a : S) → L) a : L))) : Set L)),
    HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) a : L) x' ∈
      (↑(Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) : Set L)
⊢ x ∈ (↑(Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) : Set L)

Tactic:
obtain ⟨x', rfl⟩ := Ideal.mem_span_singleton.mp hx

Premises used: Iff.mp, 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)
x' : L
hx :
  HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) a : L) x' ∈
    (↑(Ideal.span (singleton (α := L) ((algebraMap S L : (a : S) → L) a : L))) : Set L)
obtain :
  ∀ (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)),
    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)
⊢ HMul.hMul (α := L) ((algebraMap S L : (a : S) → L) a : L) x' ∈
    (↑(Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) : Set L)

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

Premises used: nonZeroDivisors, rfl, IsLocalization.exists_mk'_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)
obtain :
  ∀ (y : S) (z : R) (hz0 : z ≠ 0) (yz_eq : z • y' = (↑z' : S) * y),
    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)
⊢ 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:
obtain ⟨y, z, hz0, yz_eq⟩ :=
    Algebra.IsAlgebraic.exists_smul_eq_mul R y' (nonZeroDivisors.coe_ne_zero z')

Premises used: Algebra.IsAlgebraic.exists_smul_eq_mul, nonZeroDivisors.coe_ne_zero
-- 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:
Function.Injective.of_comp (show Function.Injective (algebraMap S L ∘ algebraMap R S) from ?_)

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

Tactic:
refine
      Function.Injective.of_comp (show Function.Injective (algebraMap S L ∘ algebraMap R S) from ?_)

Premises used: Function.Injective.of_comp
-- 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
rwa :
  Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S)) : (a : R) → L)
rwa₁ rwa₂ rwa₃ rwa₄ : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
⊢ Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := L)
    (Function.comp.{u_1 + 1, u_2 + 1, u_5 + 1} (β := S) (⇑(algebraMap S L) : (a : S) → L)
      (⇑(algebraMap R S) : (a : R) → S))

Tactic:
rwa [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq]

Premises used: IsScalarTower.algebraMap_eq, RingHom.coe_comp