awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨r, s, hr, hs.symm⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
obtain :
  ∀ (a : ℤ) (s : S) (ha : a ≠ 0) (h : a • x = (algebraMap S K : (a : S) → K) s),
    ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
⊢ ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s

Tactic:
obtain ⟨a, s, ha, h⟩ := hx.exists_smul_eq S

Premises used: IsAlgebraic.exists_smul_eq
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
a : ℤ
s : S
ha : a ≠ 0
h : a • x = (algebraMap S K : (a : S) → K) s
inl :
  ∀ (n : ℕ) (ha : Ne (α := ℤ) (↑n : ℤ) 0) (h : HSMul.hSMul (α := ℤ) (↑n : ℤ) x = (algebraMap S K : (a : S) → K) s),
    ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
inr :
  ∀ (n : ℕ) (ha : Ne (α := ℤ) (-(↑n : ℤ)) 0)
    (h : HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x = (algebraMap S K : (a : S) → K) s),
    ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s
⊢ ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s

Tactic:
obtain ⟨n, rfl | rfl⟩ := a.eq_nat_or_neg

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : Ne (α := ℤ) (↑n : ℤ) 0
h : HSMul.hSMul (α := ℤ) (↑n : ℤ) x = (algebraMap S K : (a : S) → K) s
⊢ ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s

Tactic:
⟨n, s, mod_cast ha, mod_cast h⟩

Premises used: Algebra.algebraMap, congrArg, cast, Ne, Int, Nat.cast, And.intro, Exists.intro, Nat.cast_smul_eq_nsmul, Nat.cast_inj._simp_1, congrFun', Nat.cast_zero, Eq.symm, Eq, DFunLike.coe, Not, Eq.trans
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : Ne (α := ℤ) (↑n : ℤ) 0
h : HSMul.hSMul (α := ℤ) (↑n : ℤ) x = (algebraMap S K : (a : S) → K) s
⊢ ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s

Tactic:
exact ⟨n, s, mod_cast ha, mod_cast h⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : Ne (α := ℤ) (-(↑n : ℤ)) 0
h : HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x = (algebraMap S K : (a : S) → K) s
⊢ n ≠ 0

Tactic:
simpa using ha
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : Ne (α := ℤ) (-(↑n : ℤ)) 0
h : HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x = (algebraMap S K : (a : S) → K) s
⊢ n • x = (algebraMap S K : (a : S) → K) (-s)

Tactic:
simp [← h]
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : CommRing K
inst_2 : Algebra S K
inst_3 : IsIntegralClosure S ℤ K
x : K
hx : IsAlgebraic ℤ x
s : S
n : ℕ
ha : Ne (α := ℤ) (-(↑n : ℤ)) 0
h : HSMul.hSMul (α := ℤ) (-(↑n : ℤ)) x = (algebraMap S K : (a : S) → K) s
⊢ ∃ (m : ℕ) (s : S), m ≠ 0 ∧ m • x = (algebraMap S K : (a : S) → K) s

Tactic:
exact ⟨n, -s, by simpa using ha, by simp [← h]⟩
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
pos :
  ∀ (hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
neg :
  ∀ (hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
⊢ IsAlgebraic R a

Tactic:
by_cases hRS : Function.Injective (algebraMap R S)

Premises used: Algebra.algebraMap, Function.Injective, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsAlgebraic R a

Tactic:
(Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _

Premises used: Algebra.IsAlgebraic.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsAlgebraic R a

Tactic:
exact (Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _

Premises used: Algebra.IsAlgebraic.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsAlgebraic R a

Tactic:
on_goal 2 => exact (Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _

Premises used: Algebra.IsAlgebraic.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ NoZeroDivisors R

Tactic:
have := hRS.noZeroDivisors _ (map_zero _) (map_mul _)
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
pos : ∀ (s : S) (hs : s ≠ 0) (int_s : IsIntegral S (s • a)), IsAlgebraic R a
⊢ IsAlgebraic R a

Tactic:
have ⟨s, hs, int_s⟩ := h.exists_integral_multiple
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
pos : Subsingleton R → IsAlgebraic R a
pos₁ : Nontrivial R → IsAlgebraic R a
⊢ IsAlgebraic R a

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Subsingleton R
⊢ Subsingleton S

Tactic:
have := Module.subsingleton R S
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this_1 : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Subsingleton R
this : Subsingleton S
⊢ IsAlgebraic R a

Tactic:
(is_transcendental_of_subsingleton _ _ h).elim

Premises used: False.elim, is_transcendental_of_subsingleton
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this_1 : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Subsingleton R
this : Subsingleton S
⊢ IsAlgebraic R a

Tactic:
exact (is_transcendental_of_subsingleton _ _ h).elim

Premises used: False.elim, is_transcendental_of_subsingleton
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
pos : ∀ (r : R) (hr : r ≠ 0) (w : S) (e : (algebraMap R S : (a : R) → S) r = s * w), IsAlgebraic R a
⊢ IsAlgebraic R a

Tactic:
have ⟨r, hr, _, e⟩ := (int.1 s).isAlgebraic.exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero hs)
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
r : R
hr : r ≠ 0
w : S
e : (algebraMap R S : (a : R) → S) r = s * w
rwa rwa₁ rwa₂ rwa₃ : ¬r = 0
⊢ ¬IsNilpotent r

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
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
r : R
hr : r ≠ 0
w : S
e : (algebraMap R S : (a : R) → S) r = s * w
pos : IsIntegral R (r • a)
⊢ IsAlgebraic R a

Tactic:
refine .of_smul_isIntegral (y := r) (by rwa [isNilpotent_iff_eq_zero]) ?_
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
r : R
hr : r ≠ 0
w : S
e : (algebraMap R S : (a : R) → S) r = s * w
pos : IsIntegral R (w • s • a)
⊢ IsIntegral R (r • a)

Tactic:
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R S,
    e, ← Algebra.smul_def, mul_comm, mul_smul]

Premises used: mul_comm, Algebra.smul_def, IsScalarTower.algebraMap_apply, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
r : R
hr : r ≠ 0
w : S
e : (algebraMap R S : (a : R) → S) r = s * w
⊢ IsIntegral R (w • s • a)

Tactic:
isIntegral_trans _ (int_s.smul _)

Premises used: isIntegral_trans, IsIntegral.smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
int : Algebra.IsIntegral R S
a : A
h : IsAlgebraic S a
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
this : NoZeroDivisors R
s : S
hs : s ≠ 0
int_s : IsIntegral S (s • a)
h_1 : Nontrivial R
r : R
hr : r ≠ 0
w : S
e : (algebraMap R S : (a : R) → S) r = s * w
⊢ IsIntegral R (w • s • a)

Tactic:
exact isIntegral_trans _ (int_s.smul _)

Premises used: isIntegral_trans, IsIntegral.smul
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
have :
  ∀ (p : S[X]) (hp : p ≠ 0) (eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)), IsAlgebraic R a
⊢ IsAlgebraic R a

Tactic:
have ⟨p, hp, eval0⟩ := h
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
pos :
  ∀ (hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
neg :
  ∀ (hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)), IsAlgebraic R a
⊢ IsAlgebraic R a

Tactic:
by_cases hRS : Function.Injective (algebraMap R S)

Premises used: Algebra.algebraMap, Function.Injective, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsAlgebraic R a

Tactic:
(Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _

Premises used: Algebra.IsAlgebraic.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsAlgebraic R a

Tactic:
exact (Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _

Premises used: Algebra.IsAlgebraic.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : ¬Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsAlgebraic R a

Tactic:
on_goal 2 => exact (Algebra.isAlgebraic_of_not_injective
    fun h ↦ hRS <| .of_comp (IsScalarTower.algebraMap_eq R S A ▸ h)).1 _

Premises used: Algebra.IsAlgebraic.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ FaithfulSMul R S

Tactic:
rw [← faithfulSMul_iff_algebraMap_injective] at hRS

Premises used: faithfulSMul_iff_algebraMap_injective
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
⊢ NoZeroDivisors R

Tactic:
have := NoZeroDivisors.of_faithfulSMul R S
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this : NoZeroDivisors R
⊢ Nontrivial R

Tactic:
have := Algebra.nontrivial_of_isAlgebraic R S
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this : Nontrivial R
⊢ IsDomain R

Tactic:
have : IsDomain R := NoZeroDivisors.to_isDomain _
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
pos : ∀ (r : R) (hr : r ≠ 0) (int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)), IsAlgebraic R a
⊢ IsAlgebraic R a

Tactic:
have ⟨r, hr, int⟩ := Algebra.IsAlgebraic.exists_integral_multiples R (p.support.image (coeff p))
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)
s : S
hs : s ∈ (↑(r • p).coeffs : Set S)
obtain :
  ∀ (n : ℕ) (hn : n ∈ (r • p).support) (hs : (r • p).coeff n ∈ (↑(r • p).coeffs : Set S)),
    (r • p).coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R S)) : Set S)
⊢ s ∈ (↑(Subalgebra.toSubring (integralClosure R S)) : Set S)

Tactic:
obtain ⟨n, hn, rfl⟩ := mem_coeffs_iff.mp hs

Premises used: Iff.mp, Polynomial.mem_coeffs_iff, rfl
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)
n : ℕ
hn : n ∈ (r • p).support
hs : (r • p).coeff n ∈ (↑(r • p).coeffs : Set S)
⊢ (r • p).coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R S)) : Set S)

Tactic:
int _ (Finset.mem_image_of_mem _ <| support_smul _ _ hn)

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, Polynomial.coeff, Polynomial.support_smul, IsIntegral, Finset.mem_image_of_mem
-- Module: Mathlib.RingTheory.Algebraic.Integral
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Ring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : NoZeroDivisors S
inst_8 : Algebra.IsAlgebraic R S
a : A
h : IsAlgebraic S a
p : S[X]
hp : p ≠ 0
eval0 : Eq.{u_3 + 1} (α := A) ((aeval a : (a : S[X]) → A) p : A) (0 : A)
hRS : FaithfulSMul R S
this_1 : NoZeroDivisors R
this_2 : Nontrivial R
this : IsDomain R
r : R
hr : r ≠ 0
int : ∀ z ∈ Finset.image p.coeff p.support, IsIntegral R (r • z)
n : ℕ
hn : n ∈ (r • p).support
hs : (r • p).coeff n ∈ (↑(r • p).coeffs : Set S)
⊢ (r • p).coeff n ∈ (↑(Subalgebra.toSubring (integralClosure R S)) : Set S)

Tactic:
exact int _ (Finset.mem_image_of_mem _ <| support_smul _ _ hn)

Premises used: Polynomial.support_smul, Finset.mem_image_of_mem