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
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
⊢ 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))
have 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))
Tactic: obtain ⟨f, hf₁, hf₂⟩ := h b
-- 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
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)
    (HDiv.hDiv (α := K) (β := K) ((algebraMap S K : (a : S) → K) a : K) ((algebraMap S K : (a : S) → K) b : K))
have 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))
Tactic: rw [div_eq_mul_inv]
-- 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
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))
have mp : IsIntegral.{u_1, u_4} (FractionRing R) (A := K) ((algebraMap S K : (a : S) → K) a : K)
Tactic: refine .mul ?_ (.inv ?_)
-- 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
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)
⊢ 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))
have mp₁ : IsIntegral.{u_1, u_4} (FractionRing R) (A := K) ((algebraMap S K : (a : S) → K) b : K)
Tactic: refine .mul ?_ (.inv ?_)
-- 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
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
⊢ IsAlgebraic R x
have 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
Tactic: obtain ⟨f, hf₁, hf₂⟩ := h (algebraMap S K x)
-- 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
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)
⊢ IsAlgebraic R x
have right : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
Tactic: use f, hf₁
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) (0 : S)
have hf₃ : 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₂
Cleared hypotheses: hf₂
-- 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)
x : L
hx : x ∈ (↑(Ideal.span (singleton (α := L) ((algebraMap S L : (a : S) → L) a : L))) : Set L)
⊢ x ∈ (↑(Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) : Set L)
have 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)
Tactic: obtain ⟨x', rfl⟩ := Ideal.mem_span_singleton.mp hx
Cleared hypotheses: x, hx
-- 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)
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)
have 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)
Tactic: obtain ⟨y', z', rfl⟩ := IsLocalization.exists_mk'_eq S⁰ x'
Cleared hypotheses: x', hx
-- 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)
⊢ 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 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)
Tactic: obtain ⟨y, z, hz0, yz_eq⟩ :=
    Algebra.IsAlgebraic.exists_smul_eq_mul R y' (nonZeroDivisors.coe_ne_zero z')
-- 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
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
have 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))
Tactic: refine
      Function.Injective.of_comp (show Function.Injective (algebraMap S L ∘ algebraMap R S) from ?_)
-- 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
⊢ 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))
have rwa : Function.Injective.{u_1 + 1, u_5 + 1} (α := R) (β := L)
  (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S L) (algebraMap R S)) : (a : R) → L)
Tactic: rwa [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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
⊢ 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 injRS : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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)
⊢ 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 hz0' : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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')
have yz_eq₁ : 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
Cleared hypotheses: yz_eq, injRS, hz0'
-- 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 : 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)
⊢ (↑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'
have 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'
Tactic: rw [mul_comm _ y, mul_comm _ y', yz_eq]
-- 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 : 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'
⊢ (↑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'
have 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)
Tactic: rw [mul_comm _ y, mul_comm _ y', yz_eq]
-- 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 : 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)
⊢ (↑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'
have rw₂ : y * (↑z' : S) = y * (↑z' : S)
Tactic: rw [mul_comm _ y, mul_comm _ y', yz_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
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 (α := 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 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')
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])