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
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
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) 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)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
⊢ ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1
have refine_2 : ∀ (x : S) (m₁ : R) (hm₁ : m₁ ∈ (↑M : Set R))
  (e :
    HMul.hMul (β := Sf) s
        ((algebraMap S Sf : (a : S) → Sf)
            ((↑(x,
                      Subtype.mk (p := fun (x : S) ↦
                        Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                        ((algebraMap R S : (a : R) → S) m₁) sorry).2 :
                S) :
              S) :
          Sf) =
      (algebraMap S Sf : (a : S) → Sf)
        ((x,
              Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                ((algebraMap R S : (a : R) → S) m₁) sorry) :
            S × ↥(Algebra.algebraMapSubmonoid S M)).1),
  ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1
Tactic: obtain ⟨⟨x, _, m₁, hm₁, rfl⟩, e⟩ := IsLocalization.surj (Algebra.algebraMapSubmonoid S M) s
-- 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
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
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) 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)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e :
  HMul.hMul (β := Sf) s
      ((algebraMap S Sf : (a : S) → Sf)
          ((↑(x,
                    Subtype.mk (p := fun (x : S) ↦
                      Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
                      ((algebraMap R S : (a : R) → S) m₁) ⋯).2 :
              S) :
            S) :
        Sf) =
    (algebraMap S Sf : (a : S) → Sf)
      ((x,
            Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Algebra.algebraMapSubmonoid S M) x)
              ((algebraMap R S : (a : R) → S) m₁) ⋯) :
          S × ↥(Algebra.algebraMapSubmonoid S M)).1
⊢ ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1
have e₁ : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
Tactic: simp only [← IsScalarTower.algebraMap_apply] at e
Cleared hypotheses: e
-- 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
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
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) 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)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
⊢ ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1
have refine_2 : ∀ (m₂ : R) (hm₂ : m₂ ∈ M) (hm₂s : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m₂ hm₂ • s)),
  ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1
Tactic: obtain ⟨⟨m₂, hm₂⟩, hm₂s⟩ := IsIntegral.exists_multiple_integral_of_isLocalization M _ hs
-- 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
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
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) 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)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) m₂ hm₂ • s)
⊢ ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1
have hm₂s₁ : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
Tactic: simp only [Submonoid.smul_def, Algebra.smul_def] at hm₂s
Cleared hypotheses: hm₂s
-- 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
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
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) 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)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
⊢ IsIntegral.{u_1, u_6} R (A := Sf) ((algebraMap S Sf : (a : S) → Sf) (m₂ • x) : Sf)
have simp : IsIntegral R
  (HMul.hMul (β := Sf) (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
    ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf))
Tactic: simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, ← e, ← mul_assoc]
-- 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
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
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) 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)
s : Sf
hs : Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) s
x : S
m₁ : R
hm₁ : m₁ ∈ (↑M : Set R)
e : HMul.hMul (β := Sf) s ((algebraMap R Sf : (a : R) → Sf) m₁ : Sf) = (algebraMap S Sf : (a : S) → Sf) x
m₂ : R
hm₂ : m₂ ∈ M
hm₂s : IsIntegral R (HMul.hMul (α := Sf) ((algebraMap R Sf : (a : R) → Sf) m₂ : Sf) s)
⊢ ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1
have refine_2 : ∀ (m₃ : R) (hm₃ : m₃ ∈ M) (hm₃s : IsIntegral R (m₃ • m₂ • x)),
  ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : Sf) ↦ Membership.mem (γ := Subalgebra Rf Sf) (integralClosure Rf Sf) x) s hs)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (↑x.2 : ↥(integralClosure R S)) :
          ↥(integralClosure Rf Sf)) =
      (algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        x.1
Tactic: obtain ⟨m₃, hm₃, hm₃s⟩ := IsLocalization.exists_isIntegral_smul_of_isIntegral_map (Sₘ := Sf)
      M (x := m₂ • x) <| by
        simp only [Algebra.smul_def, map_mul, ← IsScalarTower.algebraMap_apply, ← e, ← mul_assoc]
        exact hm₂s.mul (.algebraMap (Algebra.IsIntegral.isIntegral _))
-- 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
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
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) 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)
a : S
ha : Membership.mem (γ := Subalgebra R S) (integralClosure R S) a
b : S
hb : Membership.mem (γ := Subalgebra R S) (integralClosure R S) b
e :
  Eq.{u_6 + 1} (α := ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
      ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
      ↥(integralClosure Rf Sf))
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    (↑c : ↥(integralClosure R S)) *
        Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha =
      (↑c : ↥(integralClosure R S)) *
        Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb
have this : Eq (α := Sf)
  ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
      ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
            (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
        ↥(integralClosure Rf Sf)) :
    Sf)
  ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
      ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
            (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
        ↥(integralClosure Rf Sf)) :
    Sf)
Tactic: have := congr(algebraMap _ Sf $e)
-- 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
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
M : Submonoid R
inst_11 : IsLocalization M Rf
inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) 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)
a : S
ha : Membership.mem (γ := Subalgebra R S) (integralClosure R S) a
b : S
hb : Membership.mem (γ := Subalgebra R S) (integralClosure R S) b
e :
  Eq.{u_6 + 1} (α := ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
      ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
      ↥(integralClosure Rf Sf))
this :
  Eq (α := Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha) :
          ↥(integralClosure Rf Sf)) :
      Sf)
    ((algebraMap (↥(integralClosure Rf Sf)) Sf : (a : ↥(integralClosure Rf Sf)) → Sf)
        ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
              (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
            (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb) :
          ↥(integralClosure Rf Sf)) :
      Sf)
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    (↑c : ↥(integralClosure R S)) *
        Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) a ha =
      (↑c : ↥(integralClosure R S)) *
        Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) (integralClosure R S) x) b hb
have this₁ : Eq.{u_6 + 1} (α := Sf) ((algebraMap S Sf : (a : S) → Sf) a : Sf) ((algebraMap S Sf : (a : S) → Sf) b : Sf)
Tactic: have : algebraMap S Sf a = algebraMap S Sf b := by
      simpa only [← IsScalarTower.algebraMap_apply] using this
-- 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
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)
⊢ Away.{u_2, u_6} (R := ↥(integralClosure R S))
    ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) f : ↥(integralClosure R S))
    ↥(integralClosure Rf Sf)
have h : 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: convert! IsLocalization.integralClosure (S := S) (Rf := Rf) (Sf := Sf) (.powers f)
-- 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
⊢ Algebra.IsAlgebraic R S ↔ Algebra.IsAlgebraic R K
have simp : (∀ (x : S), IsAlgebraic R x) ↔ ∀ (x : K), IsAlgebraic R x
Tactic: simp only [Algebra.isAlgebraic_def]
-- 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
⊢ (∀ (x : S), IsAlgebraic R x) ↔ ∀ (x : K), IsAlgebraic R x
have mp : (∀ (x : S), IsAlgebraic R x) → ∀ (x : K), IsAlgebraic R x
Tactic: constructor
-- 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
mp : (∀ (x : S), IsAlgebraic R x) → ∀ (x : K), IsAlgebraic R x
⊢ (∀ (x : S), IsAlgebraic R x) ↔ ∀ (x : K), IsAlgebraic R x
have mpr : (∀ (x : K), IsAlgebraic R x) → ∀ (x : S), IsAlgebraic R x
Tactic: constructor
-- 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 : S), IsAlgebraic R x
x : K
this_1 : Nontrivial S := ⋯
this : Algebra.{u_1, u_4} (FractionRing R) K := FractionRing.liftAlgebra R K
⊢ IsAlgebraic R x
have this₁ : IsScalarTower R (FractionRing R) K
Tactic: have := FractionRing.isScalarTower_liftAlgebra 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
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
⊢ IsAlgebraic R x
have mp : IsIntegral.{u_1, u_4} (FractionRing R) x
Tactic: rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]
-- 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
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
⊢ IsIntegral.{u_1, u_4} (FractionRing R) x
have 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))
Tactic: obtain ⟨a : S, b, ha, rfl⟩ := div_surjective S x
Cleared hypotheses: x