awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
⊢ Function.Injective.{u_5 + 1, u_7 + 1} (α := S) (β := U) (⇑(algebraMap S U) : (a : S) → U)
have refine_1 : Function.Injective.{u_5 + 1, u_7 + 1} (α := S) (β := U)
  (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap T U) (algebraMap S T)) : (a : S) → U)
Tactic: rw [IsScalarTower.algebraMap_eq S T U]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : U
⊢ IsIntegral R x ↔ ∃ (y : S), (algebraMap S U : (a : S) → U) y = x
have refine_2 : ∀ (h : IsIntegral R x), ∃ (y : S), (algebraMap S U : (a : S) → U) y = x
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : U
refine_2 : ∀ (h : IsIntegral R x), ∃ (y : S), (algebraMap S U : (a : S) → U) y = x
⊢ IsIntegral R x ↔ ∃ (y : S), (algebraMap S U : (a : S) → U) y = x
have refine_2₁ : (∃ (y : S), (algebraMap S U : (a : S) → U) y = x) → IsIntegral R x
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : U
h : IsIntegral R x
⊢ ∃ (y : S), (algebraMap S U : (a : S) → U) y = x
have refine_2 : ∀ (x : T) (h : IsIntegral.{u_4, u_7} R (A := U) ((algebraMap T U : (a : T) → U) x : U)),
  ∃ (y : S), Eq.{u_7 + 1} (α := U) ((algebraMap S U : (a : S) → U) y : U) ((algebraMap T U : (a : T) → U) x : U)
Tactic: obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := T) (A := T)).mp h.tower_top
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (hypothesis)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : T
h : IsIntegral.{u_4, u_7} R (A := U) ((algebraMap T U : (a : T) → U) x : U)
⊢ ∃ (y : S), Eq.{u_7 + 1} (α := U) ((algebraMap S U : (a : S) → U) y : U) ((algebraMap T U : (a : T) → U) x : U)
have h₁ : IsIntegral R x
Tactic: rw [isIntegral_algebraMap_iff (IsIntegralClosure.algebraMap_injective T T U)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : T
h : IsIntegral R x
⊢ ∃ (y : S), Eq.{u_7 + 1} (α := U) ((algebraMap S U : (a : S) → U) y : U) ((algebraMap T U : (a : T) → U) x : U)
have refine_2 : ∀ (x : S) (h : IsIntegral.{u_4, u_6} R (A := T) ((algebraMap S T : (a : S) → T) x : T)),
  ∃ (y : S),
    Eq.{u_7 + 1} (α := U) ((algebraMap S U : (a : S) → U) y : U)
      ((algebraMap T U : (a : T) → U) ((algebraMap S T : (a : S) → T) x : T) : U)
Tactic: obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := R) (A := S)).mp h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : CommRing U
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : Algebra R U
inst_7 : Algebra S U
inst_8 : Algebra T U
inst_9 : IsScalarTower S T U
inst_10 : IsScalarTower R T U
inst_11 : IsIntegralClosure S R T
inst_12 : IsIntegrallyClosedIn T U
x : S
⊢ IsIntegral.{u_4, u_7} R (A := U) ((algebraMap S U : (a : S) → U) x : U)
have refine_2 : IsIntegral.{u_4, u_7} R (A := U) ((algebraMap T U : (a : T) → U) ((algebraMap S T : (a : S) → T) x : T) : U)
Tactic: rw [IsScalarTower.algebraMap_apply S T U]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
⊢ a ^ n ∣ b ^ n ↔ a ∣ b
have refine : a ^ n ∣ b ^ n → ∀ (x : R) (hx : b ^ n = a ^ n * x), a ∣ b
Tactic: refine ⟨fun ⟨x, hx⟩ ↦ ?_, fun h ↦ pow_dvd_pow_of_dvd h n⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
⊢ a ∣ b
have pos : ∀ (ha : a = 0), a ∣ b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
pos : ∀ (ha : a = 0), a ∣ b
⊢ a ∣ b
have neg : ∀ (ha : ¬a = 0), a ∣ b
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
ha : ¬a = 0
K : Type u_1 := FractionRing R
⊢ a ∣ b
have ha₁ : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
Tactic: replace ha : algebraMap R K a ≠ 0 := fun h ↦
    ha <| (injective_iff_map_eq_zero _).1 (IsFractionRing.injective R K) _ h
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
⊢ IsIntegral R y
have refine : eval₂ (algebraMap R K) y (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])) = 0
Tactic: refine ⟨X ^ n - C x, monic_X_pow_sub_C _ hn, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
⊢ eval₂ (algebraMap R K) y (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) x : R[X])) = 0
have simp : HSub.hSub (β := K)
    (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) b : K) n /
      HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) a : K) n)
    (((algebraMap R K : R →+* K) : (a : R) → K) x : K) =
  0
Tactic: simp only [y, eval₂_sub, eval₂_X_pow, div_pow, eval₂_C]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
⊢ HSub.hSub (β := K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) b : K) n /
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) a : K) n)
      (((algebraMap R K : R →+* K) : (a : R) → K) x : K) =
    0
have hx₁ : Eq (α := K) ((algebraMap R K : (a : R) → K) (b ^ n) : K) ((algebraMap R K : (a : R) → K) (a ^ n * x) : K)
Tactic: replace hx := congr_arg (algebraMap R K) hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
hx : Eq (α := K) ((algebraMap R K : (a : R) → K) (b ^ n) : K) ((algebraMap R K : (a : R) → K) (a ^ n * x) : K)
⊢ HSub.hSub (β := K)
      (HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) b : K) n /
        HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) a : K) n)
      (((algebraMap R K : R →+* K) : (a : R) → K) x : K) =
    0
have hx₁ : HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) b : K) n = (algebraMap R K : (a : R) → K) (a ^ n * x)
Tactic: rw [map_pow] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
⊢ a ∣ b
have hy : IsIntegral R y
Tactic: have hy : IsIntegral R y := by
    refine ⟨X ^ n - C x, monic_X_pow_sub_C _ hn, ?_⟩
    simp only [y, eval₂_sub, eval₂_X_pow, div_pow, eval₂_C]
    replace hx := congr_arg (algebraMap R K) hx
    rw [map_pow] at hx
    simp [hx, ha]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
hy : IsIntegral R y
⊢ a ∣ b
have neg : ∀ (k : R) (hk : (algebraMap R K : (a : R) → K) k = y), a ∣ b
Tactic: obtain ⟨k, hk⟩ := algebraMap_eq_of_integral hy
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
hy : IsIntegral R y
k : R
hk : (algebraMap R K : (a : R) → K) k = y
⊢ a ∣ b
have neg : Eq (α := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) (a * k) : K)
Tactic: refine ⟨k, IsFractionRing.injective R K ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
hy : IsIntegral R y
k : R
hk : (algebraMap R K : (a : R) → K) k = y
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) (a * k) : K)
have neg : (algebraMap R K : (a : R) → K) b =
  HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) k : K)
Tactic: rw [map_mul, hk, mul_div_cancel₀ _ ha]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
hy : IsIntegral R y
k : R
hk : (algebraMap R K : (a : R) → K) k = y
neg :
  (algebraMap R K : (a : R) → K) b =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) k : K)
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) (a * k) : K)
have neg₁ : (algebraMap R K : (a : R) → K) b = HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) a : K) y
Tactic: rw [map_mul, hk, mul_div_cancel₀ _ ha]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
h : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : Ne (α := K) ((algebraMap R K : (a : R) → K) a : K) (0 : K)
y : K := HDiv.hDiv (α := K) (β := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) a : K)
hy : IsIntegral R y
k : R
hk : (algebraMap R K : (a : R) → K) k = y
neg :
  (algebraMap R K : (a : R) → K) b =
    HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) k : K)
neg₁ : (algebraMap R K : (a : R) → K) b = HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) a : K) y
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) (a * k) : K)
have neg₂ : Eq (α := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) b : K)
Tactic: rw [map_mul, hk, mul_div_cancel₀ _ ha]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
⊢ Associated (a ^ n) (b ^ n) ↔ Associated a b
have simp_rw : a ^ n ∣ b ^ n ∧ b ^ n ∣ a ^ n ↔ a ∣ b ∧ b ∣ a
Tactic: simp_rw [← dvd_dvd_iff_associated, pow_dvd_pow_iff hn]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ Eq (α := R →+* K) (algebraMap R K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S K) (algebraMap R S))
have rw : Eq (α := R →+* K) (algebraMap R K) (g.comp (algebraMap R S))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
rw : Eq (α := R →+* K) (algebraMap R K) (g.comp (algebraMap R S))
⊢ Eq (α := R →+* K) (algebraMap R K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S K) (algebraMap R S))
have rw₁ : Eq (α := R →+* K) (algebraMap R K) (RingHom.comp (algebraMap R K) (RingHom.id R))
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
rw : Eq (α := R →+* K) (algebraMap R K) (g.comp (algebraMap R S))
rw₁ : Eq (α := R →+* K) (algebraMap R K) (RingHom.comp (algebraMap R K) (RingHom.id R))
⊢ Eq (α := R →+* K) (algebraMap R K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S K) (algebraMap R S))
have rw₂ : Eq (α := R →+* K) (algebraMap R K) (algebraMap R K)
Tactic: rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ IsIntegrallyClosed S
have this₁ : IsScalarTower R S K
Tactic: have : IsScalarTower R S K := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this_1 : Algebra S K := g.toAlgebra
this : IsScalarTower R S K
⊢ IsIntegrallyClosed S
have this₁ : IsFractionRing S K
Tactic: have := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M S K
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this_1 : Algebra S K := g.toAlgebra
this_2 : IsScalarTower R S K
this : IsFractionRing S K
⊢ IsIntegrallyClosed S
have refine : ∀ {x : K}, IsIntegral S x → ∃ (y : S), ((algebraMap S K : S →+* K) : (a : S) → K) y = x
Tactic: refine (isIntegrallyClosed_iff_isIntegralClosure (K := K)).mpr
    ⟨IsFractionRing.injective _ _, fun {x} ↦ ⟨?_, fun e ↦ e.choose_spec ▸ isIntegral_algebraMap⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this_1 : Algebra S K := g.toAlgebra
this_2 : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
⊢ ∃ (y : S), ((algebraMap S K : S →+* K) : (a : S) → K) y = x
have obtain : ∀ (y : R) (y_mem : y ∈ M) (hy : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x)),
  ∃ (y : S), ((algebraMap S K : S →+* K) : (a : S) → K) y = x
Tactic: obtain ⟨⟨y, y_mem⟩, hy⟩ := hx.exists_multiple_integral_of_isLocalization M _
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this_1 : Algebra S K := g.toAlgebra
this_2 : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x)
⊢ ∃ (y : S), ((algebraMap S K : S →+* K) : (a : S) → K) y = x
have obtain : ∀ (z : R) (hz : (algebraMap R K : (a : R) → K) z = Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x),
  ∃ (y : S), ((algebraMap S K : S →+* K) : (a : S) → K) y = x
Tactic: obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp ‹_› hy
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this_1 : Algebra S K := g.toAlgebra
this_2 : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x)
z : R
hz : (algebraMap R K : (a : R) → K) z = Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x
⊢ ∃ (y : S), ((algebraMap S K : S →+* K) : (a : S) → K) y = x
have refine : (RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K) z =
  HMul.hMul (α := K)
    ((RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K)
        (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) :
      K)
    x
Tactic: refine ⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegrallyClosed (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsIntegrallyClosed R
inst_4 : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst_5 : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map (M := M) (T := R⁰) K (RingHom.id R) hM
this_1 : Algebra S K := g.toAlgebra
this_2 : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x)
z : R
hz : (algebraMap R K : (a : R) → K) z = Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x
⊢ (RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K) z =
    HMul.hMul (α := K)
      ((RingHom.comp (algebraMap R K) (RingHom.id R) : (a : R) → K)
          (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) :
        K)
      x
have rw : (algebraMap R K : (a : R) → K) z =
  HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) : K) x
Tactic: rw [RingHom.comp_id, hz, ← Algebra.smul_def, Submonoid.mk_smul]