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
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
⊢ eval₂ (algebraMap R S) t q' = 0
have trans : eval₂ (algebraMap R S) t q' =
  t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)
Tactic: trans t ^ N * q.sum (t ^ · * φ.toRingHom ·)
-- 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
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
trans :
  eval₂ (algebraMap R S) t q' =
    t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)
⊢ eval₂ (algebraMap R S) t q' = 0
have trans₁ : (t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)) = 0
Tactic: trans t ^ N * q.sum (t ^ · * φ.toRingHom ·)
-- 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
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
⊢ (t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)) = 0
have simp_rw : (q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (α := S) ((φ.toRingHom : (a : R[X]) → S) x2 : S) (t ^ x1)) * t ^ N = 0
Tactic: simp_rw [mul_comm (t ^ _), ← eval₂_eq_sum, hqt, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
simp_rw :
  (q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (α := S) ((φ.toRingHom : (a : R[X]) → S) x2 : S) (t ^ x1)) * t ^ N = 0
⊢ (t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)) = 0
have simp_rw₁ : eval₂ φ.toRingHom t q * t ^ N = 0
Tactic: simp_rw [mul_comm (t ^ _), ← eval₂_eq_sum, hqt, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
t s : S
hst : s * t = 1
ht : IsIntegral (↥R[s]) t
h : Nontrivial S
φ : R[X] →ₐ[R] S := aeval s
q : R[X][X]
hqm : q.Monic
hqt : eval₂ φ.toRingHom t q = 0
N : ℕ := q.support.sup fun (x : ℕ) ↦ (q.coeff x).natDegree
hN : ∀ (i : ℕ), (q.coeff i).natDegree ≤ N
q' : R[X] := q.sum fun (i : ℕ) (r : R[X]) ↦ HPow.hPow (α := R[X]) X i * reflect N r
this :
  ∀ (i : ℕ),
    (aeval t : (a : R[X]) → S) (reflect N (q.coeff i)) =
      HMul.hMul (β := S) (t ^ N) ((aeval s : (a : R[X]) → S) (q.coeff i) : S)
simp_rw :
  (q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (α := S) ((φ.toRingHom : (a : R[X]) → S) x2 : S) (t ^ x1)) * t ^ N = 0
simp_rw₁ : eval₂ φ.toRingHom t q * t ^ N = 0
⊢ (t ^ N * q.sum fun (x1 : ℕ) (x2 : R[X]) ↦ HMul.hMul (β := S) (t ^ x1) ((φ.toRingHom : (a : R[X]) → S) x2 : S)) = 0
have simp_rw₂ : 0 * t ^ N = 0
Tactic: simp_rw [mul_comm (t ^ _), ← eval₂_eq_sum, hqt, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
x : S
inst_7 : Away x Sₘ
hx : IsIntegral.{u_5, u_7} R (A := Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x : Sₘ)
⊢ IsIntegral R x
have obtain : ∀ (p : R[X]) (hpm : p.Monic) (hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x) p = 0), IsIntegral R x
Tactic: obtain ⟨p, hpm, hp⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (hypothesis)
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
x : S
inst_7 : Away x Sₘ
p : R[X]
hpm : p.Monic
hp : eval₂ (algebraMap R Sₘ) ((algebraMap S Sₘ : (a : S) → Sₘ) x) p = 0
⊢ IsIntegral R x
have hp₁ : ∃ (a : ℕ), x ^ a * eval₂ (algebraMap R S) x p = 0
Tactic: simp only [IsScalarTower.algebraMap_eq R S Sₘ, IsLocalization.map_eq_zero_iff (.powers x),
    Subtype.exists, Submonoid.mem_powers_iff, ← hom_eval₂, exists_prop, exists_exists_eq_and] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
R : Type u_5
S : Type u_6
Sₘ : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing Sₘ
inst_3 : Algebra R S
inst_4 : Algebra S Sₘ
inst_5 : Algebra R Sₘ
inst_6 : IsScalarTower R S Sₘ
x : S
inst_7 : Away x Sₘ
p : R[X]
hpm : p.Monic
hp : ∃ (a : ℕ), x ^ a * eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R x
have obtain : ∀ (n : ℕ) (hn : x ^ n * eval₂ (algebraMap R S) x p = 0), IsIntegral R x
Tactic: obtain ⟨n, hn⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
h : Eq.{u_6 + 1} (α := C) ((algebraMap A C : (a : A) → C) x : C) (0 : C)
⊢ Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L)
have rw : Eq.{u_5 + 1} (α := L) ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) x : C) : L) (0 : L)
Tactic: rw [IsScalarTower.algebraMap_apply A C L, h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
h : Eq.{u_6 + 1} (α := C) ((algebraMap A C : (a : A) → C) x : C) (0 : C)
rw : Eq.{u_5 + 1} (α := L) ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) x : C) : L) (0 : L)
⊢ Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L)
have rw₁ : Eq.{u_5 + 1} (α := L) ((algebraMap C L : (a : C) → L) 0 : L) (0 : L)
Tactic: rw [IsScalarTower.algebraMap_apply A C L, h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
h : Eq.{u_6 + 1} (α := C) ((algebraMap A C : (a : A) → C) x : C) (0 : C)
rw : Eq.{u_5 + 1} (α := L) ((algebraMap C L : (a : C) → L) ((algebraMap A C : (a : A) → C) x : C) : L) (0 : L)
rw₁ : Eq.{u_5 + 1} (α := L) ((algebraMap C L : (a : C) → L) 0 : L) (0 : L)
⊢ Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L)
have rw₂ : Eq.{u_5 + 1} (α := L) 0 0
Tactic: rw [IsScalarTower.algebraMap_apply A C L, h, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(mk' C (x • z) int,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                      ((algebraMap A C : (a : A) → C) x) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((mk' C (x • z) int,
            Subtype.mk (p := fun (x : C) ↦ Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
              ((algebraMap A C : (a : A) → C) x) ⋯) :
          C × ↥(nonZeroDivisors C : Submonoid C)).1
have rw : HMul.hMul (β := L) z
    ((algebraMap C L : (a : C) → L)
        ((↑(mk' C (x • z) int,
                  Subtype.mk (p := fun (x : C) ↦ Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                    ((algebraMap A C : (a : A) → C) x) sorry).2 :
            C) :
          C) :
      L) =
  x • z
Tactic: rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, Algebra.smul_def, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
rw :
  HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(mk' C (x • z) int,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                      ((algebraMap A C : (a : A) → C) x) ⋯).2 :
              C) :
            C) :
        L) =
    x • z
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(mk' C (x • z) int,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                      ((algebraMap A C : (a : A) → C) x) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((mk' C (x • z) int,
            Subtype.mk (p := fun (x : C) ↦ Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
              ((algebraMap A C : (a : A) → C) x) ⋯) :
          C × ↥(nonZeroDivisors C : Submonoid C)).1
have rw₁ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) x : L) = x • z
Tactic: rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, Algebra.smul_def, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
rw :
  HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(mk' C (x • z) int,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                      ((algebraMap A C : (a : A) → C) x) ⋯).2 :
              C) :
            C) :
        L) =
    x • z
rw₁ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) x : L) = x • z
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(mk' C (x • z) int,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                      ((algebraMap A C : (a : A) → C) x) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((mk' C (x • z) int,
            Subtype.mk (p := fun (x : C) ↦ Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
              ((algebraMap A C : (a : A) → C) x) ⋯) :
          C × ↥(nonZeroDivisors C : Submonoid C)).1
have rw₂ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) x : L) =
  HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) x : L) z
Tactic: rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, Algebra.smul_def, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Integral (goal)
Goal:
A : Type u_3
inst : CommRing A
L : Type u_5
inst_1 : Field L
inst_2 : Algebra A L
C : Type u_6
inst_3 : CommRing C
inst_4 : IsDomain C
inst_5 : Algebra C L
inst_6 : IsIntegralClosure C A L
inst_7 : Algebra A C
inst_8 : IsScalarTower A C L
inst_9 : Algebra.IsAlgebraic A L
inj : ∀ (x : A), Eq.{u_5 + 1} (α := L) ((algebraMap A L : (a : A) → L) x : L) (0 : L) → x = 0
z : L
x : A
hx : x ≠ 0
int : IsIntegral A (x • z)
rw :
  HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(mk' C (x • z) int,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                      ((algebraMap A C : (a : A) → C) x) ⋯).2 :
              C) :
            C) :
        L) =
    x • z
rw₁ : HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) x : L) = x • z
rw₂ :
  HMul.hMul (β := L) z ((algebraMap A L : (a : A) → L) x : L) =
    HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) x : L) z
⊢ HMul.hMul (β := L) z
      ((algebraMap C L : (a : C) → L)
          ((↑(mk' C (x • z) int,
                    Subtype.mk (p := fun (x : C) ↦
                      Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
                      ((algebraMap A C : (a : A) → C) x) ⋯).2 :
              C) :
            C) :
        L) =
    (algebraMap C L : (a : C) → L)
      ((mk' C (x • z) int,
            Subtype.mk (p := fun (x : C) ↦ Membership.mem (γ := Submonoid C) (nonZeroDivisors C : Submonoid C) x)
              ((algebraMap A C : (a : A) → C) x) ⋯) :
          C × ↥(nonZeroDivisors C : Submonoid C)).1
have rw₃ : HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) x : L) z =
  HMul.hMul (α := L) ((algebraMap A L : (a : A) → L) x : L) z
Tactic: rw [algebraMap_mk', ← IsScalarTower.algebraMap_apply A C L, Algebra.smul_def, mul_comm]
-- 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)
⊢ IsLocalization.{u_2, u_6} (R := ↥(integralClosure R S)) (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)
    ↥(integralClosure Rf Sf)
have refine_1 : ∀ (y : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
  IsUnit.{u_6} (M := ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (↑y : ↥(integralClosure R S)) :
      ↥(integralClosure Rf Sf))
Tactic: refine ⟨⟨?_, ?_, ?_⟩⟩
-- 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)
refine_1 :
  ∀ (y : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    IsUnit.{u_6} (M := ↥(integralClosure Rf Sf))
      ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
            (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
          (↑y : ↥(integralClosure R S)) :
        ↥(integralClosure Rf Sf))
⊢ IsLocalization.{u_2, u_6} (R := ↥(integralClosure R S)) (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)
    ↥(integralClosure Rf Sf)
have refine_2 : ∀ (z : ↥(integralClosure Rf Sf)),
  ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    HMul.hMul (β := ↥(integralClosure Rf Sf)) z
        ((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: refine ⟨⟨?_, ?_, ?_⟩⟩
-- 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)
refine_1 :
  ∀ (y : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
    IsUnit.{u_6} (M := ↥(integralClosure Rf Sf))
      ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
            (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
          (↑y : ↥(integralClosure R S)) :
        ↥(integralClosure Rf Sf))
refine_2 :
  ∀ (z : ↥(integralClosure Rf Sf)),
    ∃ (x : ↥(integralClosure R S) × ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
      HMul.hMul (β := ↥(integralClosure Rf Sf)) z
          ((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
⊢ IsLocalization.{u_2, u_6} (R := ↥(integralClosure R S)) (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)
    ↥(integralClosure Rf Sf)
have refine_3 : ∀ {x y : ↥(integralClosure R S)},
  Eq.{u_6 + 1} (α := ↥(integralClosure Rf Sf))
      ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
            (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
          x :
        ↥(integralClosure Rf Sf))
      ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
            (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
          y :
        ↥(integralClosure Rf Sf)) →
    ∃ (c : ↥(Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M)),
      (↑c : ↥(integralClosure R S)) * x = (↑c : ↥(integralClosure R S)) * y
Tactic: refine ⟨⟨?_, ?_, ?_⟩⟩
-- 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)
f : R
hf : f ∈ (↑M : Set R)
⊢ IsUnit.{u_6} (M := ↥(integralClosure Rf Sf))
    ((algebraMap ↥(integralClosure R S) ↥(integralClosure Rf Sf) :
          (a : ↥(integralClosure R S)) → ↥(integralClosure Rf Sf))
        (↑(Subtype.mk (p := fun (x : ↥(integralClosure R S)) ↦
              Membership.mem (γ := Submonoid ↥(integralClosure R S))
                (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) x)
              ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) f) ⋯) :
          ↥(integralClosure R S)) :
      ↥(integralClosure Rf Sf))
have h : 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 : ↥(integralClosure R S)) ↦
            Membership.mem (γ := Submonoid ↥(integralClosure R S))
              (Algebra.algebraMapSubmonoid (↥(integralClosure R S)) M) x)
            ((algebraMap R ↥(integralClosure R S) : (a : R) → ↥(integralClosure R S)) f) sorry) :
        ↥(integralClosure R S)) :
    ↥(integralClosure Rf Sf))
  ((algebraMap Rf ↥(integralClosure Rf Sf) : (a : Rf) → ↥(integralClosure Rf Sf))
      ((algebraMap R Rf : (a : R) → Rf) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) f hf) : R)) :
    ↥(integralClosure Rf Sf))
Tactic: convert!
      (IsLocalization.map_units (S := Rf) ⟨f, hf⟩).map (algebraMap Rf (integralClosure Rf Sf))