awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
x : A
p : K[X]
hp : p ≠ 0
hpx : Eq.{v + 1} (α := A) ((aeval x : (a : K[X]) → A) p : A) (0 : A)
rw :
  Eq.{v + 1} (α := A)
    ((aeval x : (a : K[X]) → A) (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) : A) (0 : A)
rw₁ :
  HMul.hMul (α := A) (β := A) ((aeval x : (a : K[X]) → A) p : A)
      ((aeval x : (a : K[X]) → A) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X]) : A) =
    0
rw₂ :
  HMul.hMul (α := A) (β := A) (0 : A) ((aeval x : (a : K[X]) → A) ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X]) : A) =
    0
rw₃ rw₄ : Eq.{v + 1} (α := A) 0 0
⊢ eval₂ (algebraMap K A) x (HMul.hMul (β := K[X]) p ((C : (a : K) → K[X]) p.leadingCoeff⁻¹ : K[X])) = 0

Tactic:
rw [← aeval_def, map_mul, hpx, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.aeval_def, map_mul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
rw : (∀ (x : A), IsAlgebraic K x) ↔ Algebra.IsIntegral K A
rw₁ : (∀ (x : A), IsAlgebraic K x) ↔ ∀ (x : A), IsIntegral K x
rw₂ rw₃ : (∀ (a : A), IsIntegral K a) ↔ ∀ (x : A), IsIntegral K x
⊢ Algebra.IsAlgebraic K A ↔ Algebra.IsIntegral K A

Tactic:
rw [Algebra.isAlgebraic_def, Algebra.isIntegral_def,
      forall_congr' fun _ ↦ isAlgebraic_iff_isIntegral]

Premises used: Algebra.isIntegral_def, Algebra.isAlgebraic_def, forall_congr', isAlgebraic_iff_isIntegral
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u
A : Type v
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : Algebra.IsAlgebraic K A
⊢ Algebra.IsIntegral K A

Tactic:
Algebra.isAlgebraic_iff_isIntegral.mp ‹_›

Premises used: Algebra.isAlgebraic_iff_isIntegral, Iff.mp
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R B
inst_5 : Algebra R C
inst_6 : Algebra B C
inst_7 : IsScalarTower R B C
inst_8 : IsIntegralClosure B R C
⊢ Algebra.IsAlgebraic R B

Tactic:
have := IsIntegralClosure.isIntegral_algebra R (A := B) C
  inferInstance

Premises used: IsIntegralClosure.isIntegral_algebra, inferInstance
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : Ring A
inst_3 : Algebra R A
e : A
inst_4 : Module.Finite R A
⊢ IsAlgebraic R e

Tactic:
(IsIntegral.of_finite R e).isAlgebraic

Premises used: IsIntegral.isAlgebraic, IsIntegral.of_finite
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u_1
L : Type u_2
R : Type u_3
A : Type u_4
inst : CommRing R
inst_1 : Nontrivial R
inst_2 : Ring A
inst_3 : Algebra R A
inst_4 : Module.Finite R A
⊢ Algebra.IsAlgebraic R A

Tactic:
(IsIntegral.of_finite R A).isAlgebraic

Premises used: Algebra.IsIntegral.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
⊢ Transcendental.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A) ↔ Transcendental K r ∧ Transcendental K f

Tactic:
⟨fun h ↦ ⟨?_, h.of_aeval⟩, fun ⟨h1, h2⟩ ↦ h1.aeval_of_transcendental h2⟩

Premises used: Transcendental.of_aeval, _private.0.transcendental_aeval_iff.match_1, Transcendental, And.intro, Iff.intro, Polynomial.aeval, DFunLike.coe, Transcendental.aeval_of_transcendental
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
refine : ∀ (h : Transcendental.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)), Transcendental K r
⊢ Transcendental.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A) ↔ Transcendental K r ∧ Transcendental K f

Tactic:
refine ⟨fun h ↦ ⟨?_, h.of_aeval⟩, fun ⟨h1, h2⟩ ↦ h1.aeval_of_transcendental h2⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
h : Transcendental.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
⊢ ¬IsAlgebraic.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)

Tactic:
rw [Transcendental] at h ⊢

Premises used: Transcendental
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
h : ¬IsAlgebraic.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
contrapose : ∀ (h : IsAlgebraic K r), IsAlgebraic.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
⊢ ¬IsAlgebraic K r

Tactic:
contrapose h
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
h : IsAlgebraic K r
rw : ∀ (h : IsIntegral K r), IsIntegral.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)
⊢ IsAlgebraic.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)

Tactic:
rw [isAlgebraic_iff_isIntegral] at h ⊢

Premises used: isAlgebraic_iff_isIntegral
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
h : IsIntegral K r
⊢ IsIntegral.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)

Tactic:
.of_mem_of_fg _ h.fg_adjoin_singleton _ (aeval_mem_adjoin_singleton _ _)

Premises used: IsIntegral.of_mem_of_fg, IsIntegral.fg_adjoin_singleton, Polynomial.aeval_mem_adjoin_singleton
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u_1
A : Type u_4
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
r : A
f : K[X]
h : IsIntegral K r
⊢ IsIntegral.{u_1, u_4} K (A := A) ((aeval r : (a : K[X]) → A) f : A)

Tactic:
exact .of_mem_of_fg _ h.fg_adjoin_singleton _ (aeval_mem_adjoin_singleton _ _)
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
ϕ : L →ₐ[K] L
⊢ Function.Bijective (α := L) (β := L) (⇑ϕ : (a : L) → L)

Tactic:
(Algebra.IsAlgebraic.of_finite K L).algHom_bijective ϕ

Premises used: Algebra.IsAlgebraic.algHom_bijective
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
pos :
  ∀ (inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)),
    ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
neg :
  ∀ (inj : ¬Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)),
    ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
by_cases inj : Function.Injective (algebraMap R A)

Premises used: Algebra.algebraMap, Function.Injective, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
⊢ ¬∀ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) → a = 0

Tactic:
rw [injective_iff_map_eq_zero] at inj

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ¬∀ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) → a = 0
⊢ ∃ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) ∧ a ≠ 0

Tactic:
push Not at inj

Premises used: Not
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) ∧ a ≠ 0
neg :
  ∀ (r : R) (eq : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) (0 : A)) (ne : r ≠ 0),
    ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
have ⟨r, eq, ne⟩ := inj
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) ∧ a ≠ 0
r : R
eq : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) (0 : A)
ne : r ≠ 0
⊢ IsIntegral R (r • z)

Tactic:
simpa [← algebraMap_smul A, eq, zero_smul] using isIntegral_zero

Premises used: algebraMap_smul, zero_smul, isIntegral_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : ∃ (a : R), Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) a : A) (0 : A) ∧ a ≠ 0
r : R
eq : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) r : A) (0 : A)
ne : r ≠ 0
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
exact ⟨r, ne, by simpa [← algebraMap_smul A, eq, zero_smul] using isIntegral_zero⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
pos :
  ∀ (p : R[X]) (p_ne_zero : p ≠ 0) (px : Eq.{u_3 + 1} (α := A) ((aeval z : (a : R[X]) → A) p : A) (0 : A)),
    ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
have ⟨p, p_ne_zero, px⟩ := hz
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p : R[X]
p_ne_zero : p ≠ 0
px : Eq.{u_3 + 1} (α := A) ((aeval z : (a : R[X]) → A) p : A) (0 : A)
a : R := p.leadingCoeff
⊢ a ≠ 0

Tactic:
have a_ne_zero : a ≠ 0 := mt Polynomial.leadingCoeff_eq_zero.mp p_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p : R[X]
p_ne_zero : p ≠ 0
px : Eq.{u_3 + 1} (α := A) ((aeval z : (a : R[X]) → A) p : A) (0 : A)
a : R := p.leadingCoeff
a_ne_zero : a ≠ 0
⊢ IsIntegral R (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) a : A) z)

Tactic:
have x_integral : IsIntegral R (algebraMap R A a * z) :=
    ⟨p.integralNormalization, monic_integralNormalization p_ne_zero,
      integralNormalization_aeval_eq_zero px fun _ ↦ (map_eq_zero_iff _ inj).mp⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p : R[X]
p_ne_zero : p ≠ 0
px : Eq.{u_3 + 1} (α := A) ((aeval z : (a : R[X]) → A) p : A) (0 : A)
a : R := p.leadingCoeff
a_ne_zero : a ≠ 0
x_integral : IsIntegral R (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) a : A) z)
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
⟨_, a_ne_zero, Algebra.smul_def a z ▸ x_integral⟩

Premises used: Eq.rec, And.intro, Exists.intro, Algebra.smul_def, Eq.symm
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
hz : IsAlgebraic R z
inj : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
p : R[X]
p_ne_zero : p ≠ 0
px : Eq.{u_3 + 1} (α := A) ((aeval z : (a : R[X]) → A) p : A) (0 : A)
a : R := p.leadingCoeff
a_ne_zero : a ≠ 0
x_integral : IsIntegral R (HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) a : A) z)
⊢ ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)

Tactic:
exact ⟨_, a_ne_zero, Algebra.smul_def a z ▸ x_integral⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
⊢ Nontrivial R

Tactic:
have := Algebra.IsAlgebraic.nontrivial R A
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
choose :
  ∀ (r : (x : A) → R) (hr : ∀ (x : A), r x ≠ 0) (int : ∀ (x : A), IsIntegral R (r x • x)),
    ∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)
⊢ ∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Tactic:
choose r hr int using fun x ↦ (alg.1 x).exists_integral_multiple

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.exists_integral_multiple
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : (x : A) → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
⊢ ∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Tactic:
⟨∏ x ∈ s, r x, Finset.prod_ne_zero_iff.mpr fun _ _ ↦ hr _, fun _ h ↦ ?_⟩

Premises used: Iff.mpr, Finset.prod_ne_zero_iff, Finset.prod, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : (x : A) → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
refine : ∀ (x : A) (h : x ∈ s), IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s, r x) x)
⊢ ∃ (y : R), y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)

Tactic:
refine ⟨∏ x ∈ s, r x, Finset.prod_ne_zero_iff.mpr fun _ _ ↦ hr _, fun _ h ↦ ?_⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : (x : A) → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x : A
h : x ∈ s
rw : IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s.erase x, r x) (r x • x))
⊢ IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s, r x) x)

Tactic:
rw [← Finset.prod_erase_mul _ _ h, mul_smul]

Premises used: Finset.prod_erase_mul, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : (x : A) → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x : A
h : x ∈ s
classical : IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s.erase x, r x) (r x • x))
⊢ IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s, r x) x)

Tactic:
classical rw [← Finset.prod_erase_mul _ _ h, mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : (x : A) → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x : A
h : x ∈ s
⊢ IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s.erase x, r x) (r x • x))

Tactic:
(int _).smul _

Premises used: IsIntegral.smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : NoZeroDivisors R
alg : Algebra.IsAlgebraic R A
s : Finset A
this : Nontrivial R
r : (x : A) → R
hr : ∀ (x : A), r x ≠ 0
int : ∀ (x : A), IsIntegral R (r x • x)
x : A
h : x ∈ s
⊢ IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) (∏ x ∈ s.erase x, r x) (r x • x))

Tactic:
exact (int _).smul _

Premises used: IsIntegral.smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h : IsIntegral R (y • z)
have : ∀ (p : R[X]) (monic : p.Monic) (eval0 : eval₂ (algebraMap R A) (y • z) p = 0), IsAlgebraic R z
⊢ IsAlgebraic R z

Tactic:
have ⟨p, monic, eval0⟩ := h
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
refine : ∀ (h : p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X) = 0), False
⊢ IsAlgebraic R z

Tactic:
refine ⟨p.comp (C y * X), fun h ↦ ?_, by simpa [aeval_comp, Algebra.smul_def] using eval0⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X) = 0
⊢ (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff p.natDegree = coeff 0 p.natDegree

Tactic:
apply_fun (coeff · p.natDegree) at h

Premises used: Polynomial.coeff, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
p : R[X]
monic : p.Monic
hy : ¬IsNilpotent.{u_1} (R := R) 0
h_1 : IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 z)
eval0 : eval₂ (algebraMap R A) (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 z) p = 0
h : (p.comp (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False

Tactic:
hy .zero

Premises used: IsNilpotent.zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
p : R[X]
monic : p.Monic
hy : ¬IsNilpotent.{u_1} (R := R) 0
h_1 : IsIntegral R (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 z)
eval0 : eval₂ (algebraMap R A) (HSMul.hSMul.{u_1, u_3, u_3} (α := R) 0 z) p = 0
h : (p.comp (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 0) X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ False

Tactic:
exact hy .zero

Premises used: IsNilpotent.zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h :
  (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff p.natDegree = coeff 0 p.natDegree
⊢ y ≠ 0

Tactic:
have hy0 : y ≠ 0 := by rintro rfl; exact hy .zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h :
  (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff p.natDegree = coeff 0 p.natDegree
hy0 : y ≠ 0
rw : ∀ (h : y ^ p.natDegree = 0) (hy0 : y ≠ 0), False
rw₁ :
  ∀
    (h :
      (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff
          (p.natDegree * (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X).natDegree) =
        0)
    (hy0 : y ≠ 0), (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X).natDegree ≠ 0
⊢ False

Tactic:
rw [coeff_zero, ← mul_one p.natDegree, ← natDegree_C_mul_X y hy0,
    coeff_comp_degree_mul_degree, monic, one_mul, leadingCoeff_C_mul_X] at h

Premises used: Polynomial.natDegree_C_mul_X, Polynomial.leadingCoeff_C_mul_X, Polynomial.coeff_zero, mul_one, Polynomial.natDegree, Polynomial.coeff_comp_degree_mul_degree, one_mul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : y ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

Tactic:
hy ⟨_, h⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h : y ^ p.natDegree = 0
hy0 : y ≠ 0
⊢ False

Tactic:
exact hy ⟨_, h⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
y : R
hy : ¬IsNilpotent y
h_1 : IsIntegral R (y • z)
p : R[X]
monic : p.Monic
eval0 : eval₂ (algebraMap R A) (y • z) p = 0
h :
  (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)).coeff
      (p.natDegree * (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X).natDegree) =
    0
hy0 : y ≠ 0
rw : Ne (α := ℕ) 1 0
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X).natDegree ≠ 0

Tactic:
rw [natDegree_C_mul_X _ hy0]

Premises used: Polynomial.natDegree_C_mul_X
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
y : R
hy : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) y
h : IsAlgebraic R (y • z)
p : R[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval (y • z) : (a : R[X]) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((aeval z : (a : R[X]) → A) (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) X)) : A)
    (0 : A)

Tactic:
simpa [aeval_comp, Algebra.smul_def] using eval0

Premises used: Polynomial.aeval_comp, Algebra.smul_def
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
A : Type u_3
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
z : A
inst_3 : IsReduced R
h : ∃ (y : R), y ≠ 0 ∧ IsIntegral R (y • z)
w : R
hy : w ≠ 0
int : IsIntegral R (w • z)
rwa rwa₁ rwa₂ rwa₃ : ¬w = 0
⊢ ¬IsNilpotent w

Tactic:
rwa [isNilpotent_iff_eq_zero]

Premises used: isNilpotent_iff_eq_zero
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_4
inst_2 : CommRing K
inst_3 : Algebra S K
inst_4 : Algebra R K
inst_5 : IsIntegralClosure S R K
x : K
hx : IsAlgebraic R x
obtain :
  ∀ (r : R) (hr : r ≠ 0) (h : IsIntegral R (r • x)), ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = (algebraMap S K : (a : S) → K) s
⊢ ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = (algebraMap S K : (a : S) → K) s

Tactic:
obtain ⟨r, hr, h⟩ := hx.exists_integral_multiple

Premises used: IsAlgebraic.exists_integral_multiple
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_4
inst_2 : CommRing K
inst_3 : Algebra S K
inst_4 : Algebra R K
inst_5 : IsIntegralClosure S R K
x : K
hx : IsAlgebraic R x
r : R
hr : r ≠ 0
h : IsIntegral R (r • x)
obtain :
  ∀ (s : S) (hs : (algebraMap S K : (a : S) → K) s = r • x),
    ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = (algebraMap S K : (a : S) → K) s
⊢ ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = (algebraMap S K : (a : S) → K) s

Tactic:
obtain ⟨s, hs⟩ := IsIntegralClosure.isIntegral_iff (A := S) |>.mp h

Premises used: IsIntegralClosure.isIntegral_iff, Iff.mp
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_4
inst_2 : CommRing K
inst_3 : Algebra S K
inst_4 : Algebra R K
inst_5 : IsIntegralClosure S R K
x : K
hx : IsAlgebraic R x
r : R
hr : r ≠ 0
h : IsIntegral R (r • x)
s : S
hs : (algebraMap S K : (a : S) → K) s = r • x
⊢ ∃ (r : R) (s : S), r ≠ 0 ∧ r • x = (algebraMap S K : (a : S) → K) s

Tactic:
⟨r, s, hr, hs.symm⟩

Premises used: And.intro, Exists.intro, Eq.symm