awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
A : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Ring A
inst_3 : Algebra K L
inst_4 : Algebra L A
inst_5 : Algebra K A
inst_6 : IsScalarTower K L A
inst_7 : Algebra.IsAlgebraic K A
⊢ Algebra.IsAlgebraic L A

Tactic:
Algebra.IsAlgebraic.extendScalars (algebraMap K L).injective

Premises used: Algebra.algebraMap, Algebra.IsAlgebraic.extendScalars, RingHom.injective
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_6
L : Type u_7
A : Type u_8
inst : CommRing K
inst_1 : Field L
inst_2 : Ring A
inst_3 : Algebra K L
inst_4 : Algebra L A
inst_5 : Algebra K A
inst_6 : IsScalarTower K L A
inst_7 : Nontrivial A
inst_8 : Algebra.IsAlgebraic K A
⊢ Algebra.IsAlgebraic K L

Tactic:
tower_bot_of_injective (algebraMap L A).injective

Premises used: Algebra.algebraMap, RingHom.injective, Algebra.IsAlgebraic.tower_bot_of_injective
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
⊢ Function.Bijective (α := L) (β := L) (⇑f : (a : L) → L)

Tactic:
⟨f.injective, fun b ↦ ?_⟩

Premises used: RingHom.injective, AlgHom.toRingHom, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
refine : ∀ (b : L), ∃ (a : L), (f : (a : L) → L) a = b
⊢ Function.Bijective (α := L) (β := L) (⇑f : (a : L) → L)

Tactic:
refine ⟨f.injective, fun b ↦ ?_⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
obtain :
  ∀ (p : K[X]) (hp : p ≠ 0) (he : Eq.{u_2 + 1} (α := L) ((aeval b : (a : K[X]) → L) p : L) (0 : L)),
    ∃ (a : L), (f : (a : L) → L) a = b
⊢ ∃ (a : L), (f : (a : L) → L) a = b

Tactic:
obtain ⟨p, hp, he⟩ := Algebra.IsAlgebraic.isAlgebraic (R := K) b

Premises used: Algebra.IsAlgebraic.isAlgebraic
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : Eq.{u_2 + 1} (α := L) ((aeval b : (a : K[X]) → L) p : L) (0 : L)
f' : (↑(p.rootSet L) : Type u_2) → (↑(p.rootSet L) : Type u_2) :=
  Set.MapsTo.restrict (⇑f : (a : L) → L) (p.rootSet L) (p.rootSet L) ⋯
⊢ Function.Surjective f'

Tactic:
have : f'.Surjective := Finite.injective_iff_surjective.1
    fun _ _ h ↦ Subtype.ext <| f.injective <| Subtype.ext_iff.1 h
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : Eq.{u_2 + 1} (α := L) ((aeval b : (a : K[X]) → L) p : L) (0 : L)
f' : (↑(p.rootSet L) : Type u_2) → (↑(p.rootSet L) : Type u_2) :=
  Set.MapsTo.restrict (⇑f : (a : L) → L) (p.rootSet L) (p.rootSet L) ⋯
this : Function.Surjective f'
obtain :
  ∀ (a : (↑(p.rootSet L) : Type u_2)) (ha : f' a = Subtype.mk (p := fun (x : L) ↦ x ∈ p.rootSet L) b ⋯),
    ∃ (a : L), (f : (a : L) → L) a = b
⊢ ∃ (a : L), (f : (a : L) → L) a = b

Tactic:
obtain ⟨a, ha⟩ := this ⟨b, mem_rootSet.2 ⟨hp, he⟩⟩

Premises used: Iff.mpr, Subtype.mk, And.intro, Polynomial.mem_rootSet
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : Eq.{u_2 + 1} (α := L) ((aeval b : (a : K[X]) → L) p : L) (0 : L)
f' : (↑(p.rootSet L) : Type u_2) → (↑(p.rootSet L) : Type u_2) :=
  Set.MapsTo.restrict (⇑f : (a : L) → L) (p.rootSet L) (p.rootSet L) ⋯
this : Function.Surjective f'
a : (↑(p.rootSet L) : Type u_2)
ha : f' a = Subtype.mk (p := fun (x : L) ↦ x ∈ p.rootSet L) b ⋯
⊢ ∃ (a : L), (f : (a : L) → L) a = b

Tactic:
⟨a, Subtype.ext_iff.1 ha⟩

Premises used: Subtype.ext_iff, Exists.intro, Iff.mp, Subtype.val
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
f : L →ₐ[K] L
b : L
p : K[X]
hp : p ≠ 0
he : Eq.{u_2 + 1} (α := L) ((aeval b : (a : K[X]) → L) p : L) (0 : L)
f' : (↑(p.rootSet L) : Type u_2) → (↑(p.rootSet L) : Type u_2) :=
  Set.MapsTo.restrict (⇑f : (a : L) → L) (p.rootSet L) (p.rootSet L) ⋯
this : Function.Surjective f'
a : (↑(p.rootSet L) : Type u_2)
ha : f' a = Subtype.mk (p := fun (x : L) ↦ x ∈ p.rootSet L) b ⋯
⊢ ∃ (a : L), (f : (a : L) → L) a = b

Tactic:
exact ⟨a, Subtype.ext_iff.1 ha⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
R : Type u_3
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : DivisionRing R
inst_6 : Algebra K R
inst_7 : Algebra.IsAlgebraic K L
f : L →ₐ[K] R
g : R →ₐ[K] L
⊢ Function.Bijective.{u_2 + 1, u_3 + 1} (α := L) (β := R) (⇑f : (a : L) → R) ∧
    Function.Bijective.{u_3 + 1, u_2 + 1} (α := R) (β := L) (⇑g : (a : R) → L)

Tactic:
(g.injective.bijective₂_of_surjective f.injective (algHom_bijective <| g.comp f).2).symm

Premises used: Algebra.IsAlgebraic.algHom_bijective, RingHom.injective, And.right, AlgHom.toRingHom, AlgHom.comp, And.symm, Function.Injective.bijective₂_of_surjective
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
R : Type u_3
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsTorsionFree K L
inst_5 : Algebra.IsAlgebraic K L
inst_6 : DivisionRing R
inst_7 : Algebra K R
inst_8 : Algebra L R
inst_9 : IsScalarTower K L R
f : R →ₐ[K] L
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := R) (β := L) (⇑f : (a : R) → L)

Tactic:
(algHom_bijective₂ (IsScalarTower.toAlgHom K L R) f).2

Premises used: IsScalarTower.toAlgHom, Algebra.IsAlgebraic.algHom_bijective₂, And.right
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
R : Type u_3
inst : CommRing K
inst_1 : IsDomain K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field R
inst_5 : Algebra K R
inst_6 : IsTorsionFree K R
inst_7 : Algebra.IsAlgebraic K R
inst_8 : Algebra L R
inst_9 : IsScalarTower K L R
f : R →ₐ[K] L
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := R) (β := L) (⇑f : (a : R) → L)

Tactic:
(algHom_bijective₂ f (IsScalarTower.toAlgHom K L R)).1

Premises used: IsScalarTower.toAlgHom, Algebra.IsAlgebraic.algHom_bijective₂, And.left
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
obtain :
  ∀ (p : R[X]) (hp0 : p ≠ 0) (hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)),
    ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
⊢ ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)

Tactic:
obtain ⟨p, hp0, hp⟩ := hRs
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
obtain :
  ∀ (q : R[X]) (hpq : p = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ^ rootMultiplicity 0 p * q)
    (hq : ¬HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ∣ q),
    ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
⊢ ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)

Tactic:
obtain ⟨q, hpq, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp0 0

Premises used: Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
q : R[X]
hpq : p = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ^ rootMultiplicity 0 p * q
hq : ¬HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ∣ q
⊢ p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)

Tactic:
simp only [C_0, sub_zero, X_pow_mul, X_dvd_iff] at hpq hq

Premises used: sub_zero, Polynomial.C_0, Polynomial.X_dvd_iff, Polynomial.X_pow_mul
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
q : R[X]
hpq : p = HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ^ rootMultiplicity 0 p * q
hq : ¬HSub.hSub (α := R[X]) X ((C : (a : R) → R[X]) 0) ∣ q
hpq₁ : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
⊢ ¬q.coeff 0 = 0

Tactic:
simp only [C_0, sub_zero, X_pow_mul, X_dvd_iff] at hpq hq

Premises used: sub_zero, Polynomial.C_0, Polynomial.X_dvd_iff, Polynomial.X_pow_mul
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
q : R[X]
hpq : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
hq : ¬q.coeff 0 = 0
⊢ HMul.hMul (α := S) ((aeval s : (a : R[X]) → S) q : S) (s ^ rootMultiplicity 0 p) = 0

Tactic:
rw [hpq, map_mul, aeval_X_pow] at hp

Premises used: Polynomial.aeval_X_pow, map_mul
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
q : R[X]
hpq : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
hq : ¬q.coeff 0 = 0
hp₁ : HMul.hMul (α := S) ((aeval s : (a : R[X]) → S) q : S) (s ^ rootMultiplicity 0 p) = 0
⊢ p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)

Tactic:
rw [hpq, map_mul, aeval_X_pow] at hp

Premises used: Polynomial.aeval_X_pow, map_mul
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
hp : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) p : S) (0 : S)
q : R[X]
hpq : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
hq : ¬q.coeff 0 = 0
hp₁ : HMul.hMul (α := S) ((aeval s : (a : R[X]) → S) q : S) (s ^ rootMultiplicity 0 p) = 0
hpq₁ : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
⊢ ¬q.coeff 0 = 0

Tactic:
rw [hpq, map_mul, aeval_X_pow] at hp

Premises used: Polynomial.aeval_X_pow, map_mul
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
q : R[X]
hp : HMul.hMul (α := S) ((aeval s : (a : R[X]) → S) q : S) (s ^ rootMultiplicity 0 p) = 0
hpq : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
hq : ¬q.coeff 0 = 0
⊢ ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)

Tactic:
⟨q, hq, (S⁰.pow_mem hs (rootMultiplicity 0 p)).2 (aeval s q) hp⟩

Premises used: Submonoid.pow_mem, nonZeroDivisors, And.right, And.intro, Exists.intro, Polynomial.rootMultiplicity, Polynomial.aeval, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hs : Membership.mem (γ := Submonoid S) S⁰ s
p : R[X]
hp0 : p ≠ 0
q : R[X]
hp : HMul.hMul (α := S) ((aeval s : (a : R[X]) → S) q : S) (s ^ rootMultiplicity 0 p) = 0
hpq : p = q * HPow.hPow (α := R[X]) X (rootMultiplicity 0 p)
hq : ¬q.coeff 0 = 0
⊢ ∃ (q : R[X]), q.coeff 0 ≠ 0 ∧ Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)

Tactic:
exact ⟨q, hq, (S⁰.pow_mem hs (rootMultiplicity 0 p)).2 (aeval s q) hp⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
have :
  ∀ (q : R[X]) (hq0 : q.coeff 0 ≠ 0) (hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)),
    ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r
⊢ ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r

Tactic:
have ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
have :
  ∀ (p : R[X]) (hp : HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) = X * p),
    ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r
⊢ ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r

Tactic:
have ⟨p, hp⟩ := X_dvd_sub_C (p := q)
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
p : R[X]
hp : HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) = X * p
⊢ ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r

Tactic:
⟨aeval s p, aeval_mem_adjoin_singleton _ _, _, neg_ne_zero.mpr hq0, ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, neg_ne_zero, Polynomial.aeval, Polynomial.aeval_mem_adjoin_singleton, DFunLike.coe
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
p : R[X]
hp : HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) = X * p
refine : HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
⊢ ∃ (t : S), Membership.mem (γ := Subalgebra R S) R[s] t ∧ ∃ (r : R), r ≠ 0 ∧ s * t = (algebraMap R S : (a : R) → S) r

Tactic:
refine ⟨aeval s p, aeval_mem_adjoin_singleton _ _, _, neg_ne_zero.mpr hq0, ?_⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
p : R[X]
hp : HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) = X * p
⊢ Eq.{u_2 + 1} (α := S)
    ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)
    ((aeval s : (a : R[X]) → S) (X * p) : S)

Tactic:
apply_fun aeval s at hp

Premises used: Polynomial.aeval
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
p : R[X]
hp :
  Eq.{u_2 + 1} (α := S)
    ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)
    ((aeval s : (a : R[X]) → S) (X * p) : S)
rwa :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) ((aeval s : (a : R[X]) → S) q : S)
          ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₁ :
  ∀
    (hp :
      HSub.hSub (α := S) (β := S) (0 : S) ((aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S) =
        (aeval s : (a : R[X]) → S) (X * p)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₂ :
  ∀
    (hp :
      Eq.{u_2 + 1} (α := S) (-(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) : S)
        ((aeval s : (a : R[X]) → S) (X * p) : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₃ :
  ∀
    (hp :
      -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
        HMul.hMul (α := S) (β := S) ((aeval s : (a : R[X]) → S) X : S) ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₄ :
  ∀
    (hp :
      -(aeval s : (a : R[X]) → S) ((C : (a : R) → R[X]) (q.coeff 0) : R[X]) =
        HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₅ :
  ∀ (hp : -(algebraMap R S : (a : R) → S) (q.coeff 0) = HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₆ :
  ∀ (hp : (algebraMap R S : (a : R) → S) (-q.coeff 0) = HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
rwa₇ rwa₈ rwa₉ rwa₁₀ :
  ∀ (hp : HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)),
    HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)
⊢ HMul.hMul (β := S) s ((aeval s : (a : R[X]) → S) p : S) = (algebraMap R S : (a : R) → S) (-q.coeff 0)

Tactic:
rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp

Premises used: map_sub, map_neg, eq_comm, map_mul, Polynomial.aeval_C, Polynomial.aeval_X, zero_sub
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
obtain :
  ∀ (q : R[X]) (hq0 : q.coeff 0 ≠ 0) (hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)),
    ∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S : (a : R) → S) r
⊢ ∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S : (a : R) → S) r

Tactic:
obtain ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs

Premises used: IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
⊢ Dvd.dvd.{u_2} (α := S) ((aeval s : (a : R[X]) → S) X : S)
    ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)

Tactic:
have key := map_dvd (aeval s) (X_dvd_sub_C (p := q))
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
key :
  Dvd.dvd.{u_2} (α := S) ((aeval s : (a : R[X]) → S) X : S)
    ((aeval s : (a : R[X]) → S) (HSub.hSub (β := R[X]) q ((C : (a : R) → R[X]) (q.coeff 0) : R[X])) : S)
⊢ s ∣ (algebraMap R S : (a : R) → S) (q.coeff 0)

Tactic:
rw [map_sub, hq, zero_sub, dvd_neg, aeval_X, aeval_C] at key

Premises used: map_sub, dvd_neg, Polynomial.aeval_C, Polynomial.aeval_X, zero_sub
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
key : s ∣ (algebraMap R S : (a : R) → S) (q.coeff 0)
⊢ ∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S : (a : R) → S) r

Tactic:
⟨q.coeff 0, hq0, key⟩

Premises used: Polynomial.coeff, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : Membership.mem (γ := Submonoid S) S⁰ s
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : Eq.{u_2 + 1} (α := S) ((aeval s : (a : R[X]) → S) q : S) (0 : S)
key : s ∣ (algebraMap R S : (a : R) → S) (q.coeff 0)
⊢ ∃ (r : R), r ≠ 0 ∧ s ∣ (algebraMap R S : (a : R) → S) r

Tactic:
exact ⟨q.coeff 0, hq0, key⟩
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
a b : S
hRb : IsAlgebraic R b
hb : Membership.mem (γ := Submonoid S) S⁰ b
r : R
hr : r ≠ 0
s : S
h : (algebraMap R S : (a : R) → S) r = b * s
rw : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a = b * (s * a)
rw₁ : b * s * a = b * (s * a)
rw₂ rw₃ : b * (s * a) = b * (s * a)
⊢ r • a = b * (s * a)

Tactic:
rw [smul_def, h, mul_assoc]

Premises used: mul_assoc, Algebra.smul_def
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : NoZeroDivisors S
inst_4 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
⊢ ∃ (c : S) (d : R), d ≠ 0 ∧ d • a = b * c

Tactic:
(isAlgebraic b).exists_smul_eq_mul a (mem_nonZeroDivisors_of_ne_zero hb)

Premises used: Algebra.IsAlgebraic.isAlgebraic, IsAlgebraic.exists_smul_eq_mul, mem_nonZeroDivisors_of_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := ↥R[s])
    (⇑(aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) : (a : R[X]) → ↥R[s])

Tactic:
⟨transcendental_iff_injective.mp ?_, ?_⟩

Premises used: transcendental_iff_injective, And.intro, Iff.mp, Function.Bijective
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : S
h : Transcendental R s
refine_1 :
  Transcendental R (A := ↥R[s]) (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)
refine_2 :
  Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := ↥R[s])
    (⇑(aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) : (a : R[X]) → ↥R[s])
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := ↥R[s])
    (⇑(aeval (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[s] x) s ⋯)) : (a : R[X]) → ↥R[s])

Tactic:
refine ⟨transcendental_iff_injective.mp ?_, ?_⟩