awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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)
⊢ 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
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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)
⊢ 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

Premises used: map_pow
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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 : HPow.hPow (α := K) ((algebraMap R K : (a : R) → K) b : K) n = (algebraMap R K : (a : R) → K) (a ^ n * x)
⊢ 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 [hx, ha]
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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

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]
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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
neg : ∀ (k : R) (hk : (algebraMap R K : (a : R) → K) k = y), a ∣ b
⊢ a ∣ b

Tactic:
obtain ⟨k, hk⟩ := algebraMap_eq_of_integral hy

Premises used: IsIntegrallyClosed.algebraMap_eq_of_integral
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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

Tactic:
⟨k, IsFractionRing.injective R K ?_⟩

Premises used: IsFractionRing.injective, Exists.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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 : Eq (α := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) (a * k) : K)
⊢ a ∣ b

Tactic:
refine ⟨k, IsFractionRing.injective R K ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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
neg₂ neg₃ : Eq (α := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) b : K)
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) b : K) ((algebraMap R K : (a : R) → K) (a * k) : K)

Tactic:
rw [map_mul, hk, mul_div_cancel₀ _ ha]

Premises used: mul_div_cancel₀, map_mul
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
simp_rw : a ^ n ∣ b ^ n ∧ b ^ n ∣ a ^ n ↔ a ∣ b ∧ b ∣ a
⊢ Associated (a ^ n) (b ^ n) ↔ Associated a b

Tactic:
simp_rw [← dvd_dvd_iff_associated, pow_dvd_pow_iff hn]

Premises used: dvd_dvd_iff_associated, IsIntegrallyClosed.pow_dvd_pow_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
K : Type u_3
inst_1 : CommRing K
inst_2 : Algebra R K
ifr : IsFractionRing R K
inst_3 : IsIntegrallyClosed R
⊢ Eq (α := Subalgebra R K) (integralClosure R K) ⊥

Tactic:
(integralClosure_eq_bot_iff K).mpr ‹_›

Premises used: Iff.mpr, IsIntegrallyClosed.integralClosure_eq_bot_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
L : Type u_3
inst_4 : Field L
inst_5 : Algebra K L
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : IsDomain R
inst_9 : FiniteDimensional K L
⊢ IsIntegrallyClosed.{u_3} ↥(integralClosure R L)

Tactic:
letI : IsFractionRing (integralClosure R L) L := isFractionRing_of_finite_extension K L
  (integralClosure_eq_bot_iff L).mp integralClosure_idem

Premises used: integralClosure_idem, IsIntegrallyClosed.integralClosure_eq_bot_iff, Iff.mp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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))
rw₂ rw₃ : Eq (α := R →+* K) (algebraMap R K) (algebraMap R K)
⊢ Eq (α := R →+* K) (algebraMap R K)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S K) (algebraMap R S))

Tactic:
rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]

Premises used: RingHomCompTriple.comp_eq, IsLocalization.map_comp, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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
⊢ 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])
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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
⊢ IsFractionRing S K

Tactic:
have := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M S K
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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

Tactic:
(isIntegrallyClosed_iff_isIntegralClosure (K := K)).mpr
    ⟨IsFractionRing.injective _ _, fun {x} ↦ ⟨?_, fun e ↦ e.choose_spec ▸ isIntegral_algebraMap⟩⟩

Premises used: Iff.mpr, Exists.choose_spec, IsFractionRing.injective, IsIntegralClosure.mk, Eq.rec, isIntegral_algebraMap, Iff.intro, isIntegrallyClosed_iff_isIntegralClosure
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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
refine : ∀ {x : K}, IsIntegral S x → ∃ (y : S), ((algebraMap S K : S →+* K) : (a : S) → K) y = x
⊢ IsIntegrallyClosed S

Tactic:
refine (isIntegrallyClosed_iff_isIntegralClosure (K := K)).mpr
    ⟨IsFractionRing.injective _ _, fun {x} ↦ ⟨?_, fun e ↦ e.choose_spec ▸ isIntegral_algebraMap⟩⟩

Premises used: Iff.mpr, IsFractionRing.injective, IsIntegralClosure.mk, Iff.intro, isIntegrallyClosed_iff_isIntegralClosure
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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
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
⊢ ∃ (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 _

Premises used: IsIntegral.exists_multiple_integral_of_isLocalization
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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)
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
⊢ ∃ (y : S), ((algebraMap S K : S →+* K) : (a : S) → K) y = x

Tactic:
obtain ⟨z, hz⟩ := (isIntegrallyClosed_iff _).mp ‹_› hy

Premises used: Iff.mp, isIntegrallyClosed_iff
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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

Tactic:
⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩

Premises used: Iff.mpr, IsLocalization.lift_mk'_spec, Subtype.mk, IsLocalization.mk', Exists.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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
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
⊢ ∃ (y : S), ((algebraMap S K : S →+* K) : (a : S) → K) y = x

Tactic:
refine ⟨IsLocalization.mk' S z ⟨y, y_mem⟩, (IsLocalization.lift_mk'_spec _ _ _ _).mpr ?_⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
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
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
rw₁ :
  Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x =
    HMul.hMul (α := K) ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) : K) x
rw₂ : Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem • x = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) • x
rw₃ rw₄ : y • x = (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y y_mem) : R) • 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

Tactic:
rw [RingHom.comp_id, hz, ← Algebra.smul_def, Submonoid.mk_smul]

Premises used: Submonoid.mk_smul, RingHom.comp_id, Algebra.smul_def
-- Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
Goal:
K : Type u_1
inst : Field K
⊢ IsIntegrallyClosed K

Tactic:
(isIntegrallyClosed_iff K).mpr fun {x} _ ↦ ⟨x, rfl⟩

Premises used: Iff.mpr, Exists.intro, isIntegrallyClosed_iff, rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
f : R →+* S
x : R
⊢ eval₂ f ((f : (a : R) → S) x) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
x : R
⊢ IsIntegral.{u_1, u_3} R (A := A) ((algebraMap R A : (a : R) → A) x : A)

Tactic:
(algebraMap R A).isIntegralElem_map

Premises used: Algebra.algebraMap, RingHom.isIntegralElem_map, IsIntegral
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
x : S
hx : f.IsIntegralElem x
g : S →+* T
obtain : ∀ (p : R[X]) (hp : p.Monic) (hx : eval₂ f x p = 0), (g.comp f).IsIntegralElem ((g : (a : S) → T) x)
⊢ (g.comp f).IsIntegralElem ((g : (a : S) → T) x)

Tactic:
obtain ⟨p, hp, hx⟩ := hx
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
x : S
g : S →+* T
p : R[X]
hp : p.Monic
hx : eval₂ f x p = 0
simp_rw :
  ∀ (hx : eval x (Polynomial.map f p) = 0),
    Eq.{u_4 + 1} (α := T) ((g : (a : S) → T) (eval x (Polynomial.map f p)) : T) (0 : T)
⊢ eval₂ (g.comp f) ((g : (a : S) → T) x) p = 0

Tactic:
simp_rw [← hom_eval₂, eval₂_eq_eval_map] at hx ⊢

Premises used: Polynomial.hom_eval₂, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
x : S
g : S →+* T
p : R[X]
hp : p.Monic
hx : eval x (Polynomial.map f p) = 0
⊢ Eq.{u_4 + 1} (α := T) ((g : (a : S) → T) (eval x (Polynomial.map f p)) : T) (0 : T)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
x : S
g : S →+* T
p : R[X]
hp : p.Monic
hx : eval₂ f x p = 0
⊢ (g.comp f).IsIntegralElem ((g : (a : S) → T) x)

Tactic:
exact ⟨p, hp, by simp_rw [← hom_eval₂, eval₂_eq_eval_map] at hx ⊢; simp [hx]⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
g : S →+* T
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
x : S
hx : (g.comp f).IsIntegralElem ((g : (a : S) → T) x)
obtain : ∀ (p : R[X]) (hp : p.Monic) (hx : eval₂ (g.comp f) ((g : (a : S) → T) x) p = 0), f.IsIntegralElem x
⊢ f.IsIntegralElem x

Tactic:
obtain ⟨p, hp, hx⟩ := hx
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
g : S →+* T
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
x : S
p : R[X]
hp : p.Monic
hx : eval₂ (g.comp f) ((g : (a : S) → T) x) p = 0
⊢ Eq.{u_4 + 1} (α := T) ((g : (a : S) → T) (eval₂ f x p) : T) ((g : (a : S) → T) 0 : T)

Tactic:
simp [Polynomial.hom_eval₂, hx]

Premises used: Polynomial.hom_eval₂
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
g : S →+* T
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
x : S
p : R[X]
hp : p.Monic
hx : eval₂ (g.comp f) ((g : (a : S) → T) x) p = 0
⊢ f.IsIntegralElem x

Tactic:
exact ⟨p, hp, hg <| by simp [Polynomial.hom_eval₂, hx]⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_4
inst : CommRing R
inst_1 : Ring S
inst_2 : Ring T
f : R →+* S
g : S →+* T
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := S) (β := T) (⇑g : (a : S) → T)
x : S
⊢ (g.comp f).IsIntegralElem ((g : (a : S) → T) x) ↔ f.IsIntegralElem x

Tactic:
⟨of_map hg, (map · g)⟩

Premises used: RingHom.IsIntegralElem.map, RingHom.IsIntegralElem.of_map, Iff.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring T
f : R →+* S
g : S →+* T
x : T
hx : (g.comp f).IsIntegralElem x
obtain : ∀ (p : R[X]) (hp : p.Monic) (hx : eval₂ (g.comp f) x p = 0), g.IsIntegralElem x
⊢ g.IsIntegralElem x

Tactic:
obtain ⟨p, hp, hx⟩ := hx
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring T
f : R →+* S
g : S →+* T
x : T
p : R[X]
hp : p.Monic
hx : eval₂ (g.comp f) x p = 0
⊢ eval₂ g x (Polynomial.map f p) = 0

Tactic:
simpa only [eval₂_eq_eval_map, map_map] using hx

Premises used: Polynomial.map_map, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring T
f : R →+* S
g : S →+* T
x : T
p : R[X]
hp : p.Monic
hx : eval₂ (g.comp f) x p = 0
⊢ g.IsIntegralElem x

Tactic:
exact ⟨p.map f, hp.map _, by simpa only [eval₂_eq_eval_map, map_map] using hx⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
C : Type u_7
F : Type u_8
inst_3 : Ring B
inst_4 : Ring C
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : Algebra R C
inst_8 : IsScalarTower R A B
inst_9 : Algebra A C
inst_10 : IsScalarTower R A C
b : B
inst_11 : FunLike F B C
inst_12 : AlgHomClass F A B C
f : F
hb : IsIntegral R b
rw :
  RingHom.IsIntegralElem
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R (↑f : B →ₐ[A] C)) : B →+* C)
      (algebraMap R B))
    ((f : (a : B) → C) b)
⊢ IsIntegral.{u_1, u_7} R (A := C) ((f : (a : B) → C) b : C)

Tactic:
rw [IsIntegral, ← ((AlgHomClass.toAlgHom f).restrictScalars R).comp_algebraMap]

Premises used: AlgHom.comp_algebraMap, AlgHom.restrictScalars, IsIntegral, AlgHomClass.toAlgHom
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
C : Type u_7
F : Type u_8
inst_3 : Ring B
inst_4 : Ring C
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : Algebra R C
inst_8 : IsScalarTower R A B
inst_9 : Algebra A C
inst_10 : IsScalarTower R A C
b : B
inst_11 : FunLike F B C
inst_12 : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ RingHom.IsIntegralElem
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R (↑f : B →ₐ[A] C)) : B →+* C)
      (algebraMap R B))
    ((f : (a : B) → C) b)

Tactic:
.map hb (RingHomClass.toRingHom f)

Premises used: RingHom.IsIntegralElem.map, MonoidHomClass.toMonoidHom, AlgHom.restrictScalars, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
C : Type u_7
F : Type u_8
inst_3 : Ring B
inst_4 : Ring C
inst_5 : Algebra R B
inst_6 : Algebra A B
inst_7 : Algebra R C
inst_8 : IsScalarTower R A B
inst_9 : Algebra A C
inst_10 : IsScalarTower R A C
b : B
inst_11 : FunLike F B C
inst_12 : AlgHomClass F A B C
f : F
hb : IsIntegral R b
⊢ RingHom.IsIntegralElem
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(AlgHom.restrictScalars R (↑f : B →ₐ[A] C)) : B →+* C)
      (algebraMap R B))
    ((f : (a : B) → C) b)

Tactic:
exact .map hb (RingHomClass.toRingHom f)