awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
coeff_zero_ne : p.coeff 0 ≠ 0
h : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
convert_2 : Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L) (0 : L)
⊢ Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 0 : L)

Tactic:
rw [RingHom.map_zero]

Premises used: RingHom.map_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
coeff_zero_ne : p.coeff 0 ≠ 0
h : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
⊢ Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)

Tactic:
aeval_eq
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
coeff_zero_ne : p.coeff 0 ≠ 0
h : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
h₁ :
  Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L) ((aeval x : (a : K[X]) → L) p : L)
⊢ Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L) (0 : L)

Tactic:
convert! aeval_eq
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
coeff_zero_ne : p.coeff 0 ≠ 0
h : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
rw : ((aeval x : (a : K[X]) → L) (HAdd.hAdd (β := K[X]) (p.divX * X) ((C : (a : K) → K[X]) (p.coeff 0) : K[X])) : L)
| ((aeval x : (a : K[X]) → L) p : L)

Tactic:
rw [← divX_mul_X_add p]

Premises used: Polynomial.divX_mul_X_add
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
coeff_zero_ne : p.coeff 0 ≠ 0
h : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
h₁ :
  Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L)
    ((aeval x : (a : K[X]) → L) (HAdd.hAdd (β := K[X]) (p.divX * X) ((C : (a : K) → K[X]) (p.coeff 0) : K[X])) : L)
⊢ Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L) ((aeval x : (a : K[X]) → L) p : L)

Tactic:
conv_rhs => rw [← divX_mul_X_add p]

Premises used: Polynomial.divX_mul_X_add
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p : L) (0 : L)
coeff_zero_ne : p.coeff 0 ≠ 0
h : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
h₁ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) =
    HAdd.hAdd (α := L) (β := L) ((aeval x : (a : K[X]) → L) (p.divX * X) : L)
      ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L)
h₂ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) =
    HAdd.hAdd (β := L)
      (HMul.hMul (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L) ((aeval x : (a : K[X]) → L) X : L))
      ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L)
h₃ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) (β := L) (0 : L) ((aeval x : (a : K[X]) → L) X : L))
      ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L)
h₄ :
  ((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) =
    HAdd.hAdd (α := L) (β := L) (0 : L) ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L)
h₅ :
  Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L)
    ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L)
h₆ h₇ :
  Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L)
    ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
⊢ Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L)
    ((aeval x : (a : K[X]) → L) (HAdd.hAdd (β := K[X]) (p.divX * X) ((C : (a : K) → K[X]) (p.coeff 0) : K[X])) : L)

Tactic:
rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]

Premises used: MulZeroClass.zero_mul, map_add, zero_add, map_mul, Polynomial.aeval_C
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
coeff_zero_ne : p.coeff 0 ≠ 0
this : (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
rw : HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) ∈ A
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
coeff_zero_ne : p.coeff 0 ≠ 0
this : (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
⊢ HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) ∈ A

Tactic:
A.smul_mem (aeval x _).2 _

Premises used: Subalgebra.smul_mem, Polynomial.aeval, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
coeff_zero_ne : p.coeff 0 ≠ 0
this : (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
⊢ HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) ∈ A

Tactic:
exact A.smul_mem (aeval x _).2 _

Premises used: Subalgebra.smul_mem, Polynomial.aeval, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
coeff_zero_ne : p.coeff 0 ≠ 0
suffices : (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
suffices (x⁻¹ : L) = (-p.coeff 0)⁻¹ • aeval x (divX p) by
    rw [this]
    exact A.smul_mem (aeval x _).2 _
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
coeff_zero_ne : p.coeff 0 ≠ 0
rw : Eq.{u_2 + 1} (α := L) (↑((aeval x : (a : K[X]) → ↥A) p) : L) 0
rw₁ : Eq.{u_2 + 1} (α := L) (↑0 : L) 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := L) 0 0
⊢ Eq.{u_2 + 1} (α := L) ((aeval (↑x : L) : (a : K[X]) → L) p : L) (0 : L)

Tactic:
rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]

Premises used: Subalgebra.aeval_coe, Subalgebra.coe_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ Eq.{u_2 + 1} (α := L) ((aeval (↑x : L) : (a : K[X]) → L) p : L) (0 : L)

Tactic:
have : aeval (x : L) p = 0 := by rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
coeff_zero_ne : p.coeff 0 ≠ 0
this : Eq.{u_2 + 1} (α := L) ((aeval (↑x : L) : (a : K[X]) → L) p : L) (0 : L)
rw :
  -HDiv.hDiv (α := L) (β := L) ((aeval (↑x : L) : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
rw₁ :
  -HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
        ((aeval (↑x : L) : (a : K[X]) → L) p.divX : L) =
    HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
rw₂ :
  -HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
        ((aeval (↑x : L) : (a : K[X]) → L) p.divX : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) (-p.coeff 0)⁻¹ : L)
      ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L)
rw₃ :
  -HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
        ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L) =
    HMul.hMul (α := L) (β := L) ((algebraMap K L : (a : K) → L) (-p.coeff 0)⁻¹ : L)
      ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L)
rw₄ :
  -HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
        ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L) =
    HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) (-p.coeff 0))⁻¹ : L)
      ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L)
rw₅ :
  -HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
        ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L) =
    HMul.hMul (α := L) (β := L) ((-(algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
      ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L)
rw₆ :
  -HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
        ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L) =
    HMul.hMul (α := L) (β := L) (-((algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
      ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L)
rw₇ rw₈ :
  -HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
        ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L) =
    -HMul.hMul (α := L) (β := L) (((algebraMap K L : (a : K) → L) (p.coeff 0))⁻¹ : L)
        ((↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) : L)
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)

Tactic:
rw [inv_eq_of_root_of_coeff_zero_ne_zero this coeff_zero_ne, div_eq_inv_mul, Algebra.smul_def,
    aeval_coe, map_inv₀, map_neg, inv_neg, neg_mul]

Premises used: Subalgebra.aeval_coe, inv_neg, map_inv₀, map_neg, Algebra.smul_def, neg_mul, div_eq_inv_mul, inv_eq_of_root_of_coeff_zero_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
hx : IsAlgebraic K (↑x : L)
obtain :
  ∀ (p : K[X]) (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval (↑x : L) : (a : K[X]) → L) p : L) (0 : L)),
    (↑x : L)⁻¹ ∈ A
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
obtain ⟨p, ne_zero, aeval_eq⟩ := hx

Premises used: nonZeroDivisors.ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
ne_zero : p ≠ 0
aeval_eq : Eq.{u_2 + 1} (α := L) ((aeval (↑x : L) : (a : K[X]) → L) p : L) (0 : L)
⊢ Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)

Tactic:
rw [Subalgebra.aeval_coe, Subalgebra.coe_eq_zero] at aeval_eq

Premises used: Subalgebra.aeval_coe, Subalgebra.coe_eq_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
ne_zero : p ≠ 0
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
revert :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
revert ne_zero aeval_eq
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
⊢ ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A

Tactic:
p.recOnHorner ?_ ?_ ?_

Premises used: Polynomial.recOnHorner
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
refine_1 :
  ∀ (ne_zero : Ne.{u_1 + 1} (α := K[X]) 0 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) 0) 0),
    (↑x : L)⁻¹ ∈ A
refine_2 :
  ∀ (p : K[X]) (a : K),
    p.coeff 0 = 0 →
      a ≠ 0 →
        (∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)),
            (↑x : L)⁻¹ ∈ A) →
          ∀ (ne_zero : HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X]) ≠ 0)
            (aeval_eq :
              Eq.{u_2 + 1} (α := ↥A)
                ((aeval x : (a : K[X]) → ↥A) (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])) : ↥A) (0 : ↥A)),
            (↑x : L)⁻¹ ∈ A
refine_3 :
  ∀ (p : K[X]),
    p ≠ 0 →
      (∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)),
          (↑x : L)⁻¹ ∈ A) →
        ∀ (ne_zero : p * X ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) (p * X) : ↥A) (0 : ↥A)),
          (↑x : L)⁻¹ ∈ A
⊢ ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A

Tactic:
refine p.recOnHorner ?_ ?_ ?_
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p : K[X]
h : Ne.{u_1 + 1} (α := K[X]) 0 0
⊢ ∀ (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) 0) 0), (↑x : L)⁻¹ ∈ A

Tactic:
contradiction
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
a : K
hp : p.coeff 0 = 0
ha : a ≠ 0
_ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X]) ≠ 0
aeval_eq :
  Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])) : ↥A)
    (0 : ↥A)
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq ?_

Premises used: Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
a : K
hp : p.coeff 0 = 0
ha : a ≠ 0
_ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X]) ≠ 0
aeval_eq :
  Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])) : ↥A)
    (0 : ↥A)
refine_2 : (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])).coeff 0 ≠ 0
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
refine A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq ?_

Premises used: Subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
a : K
hp : p.coeff 0 = 0
ha : a ≠ 0
_ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X]) ≠ 0
aeval_eq :
  Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])) : ↥A)
    (0 : ↥A)
refine_2 : p.coeff 0 + coeff ((C : (a : K) → K[X]) a) 0 ≠ 0
refine_2₁ : HAdd.hAdd (α := K) 0 (coeff ((C : (a : K) → K[X]) a) 0) ≠ 0
refine_2₂ : Ne.{u_1 + 1} (α := K) (coeff ((C : (a : K) → K[X]) a) 0) 0
refine_2₃ : (if Eq (α := ℕ) 0 0 then a else 0) ≠ 0
refine_2₄ refine_2₅ refine_2₆ refine_2₇ : a ≠ 0
⊢ (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])).coeff 0 ≠ 0

Tactic:
rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]

Premises used: Polynomial.coeff_add, if_pos, Polynomial.coeff_C, zero_add, rfl
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) (p * X) : ↥A) (0 : ↥A)
⊢ Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A) ∨ x = 0

Tactic:
rw [map_mul, aeval_X, mul_eq_zero] at aeval_eq

Premises used: mul_eq_zero, map_mul, Polynomial.aeval_X
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A) ∨ x = 0
refine_3 : ∀ (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
refine_3₁ : ∀ (x_eq : x = 0), (↑x : L)⁻¹ ∈ A
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
rcases aeval_eq with aeval_eq | x_eq
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
ih hp aeval_eq
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
exact ih hp aeval_eq
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
refine_3 : 0 ∈ A
⊢ (↑x : L)⁻¹ ∈ A

Tactic:
rw [x_eq, Subalgebra.coe_zero, inv_zero]

Premises used: inv_zero, Subalgebra.coe_zero
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ 0 ∈ A

Tactic:
A.zero_mem

Premises used: Set.Mem, Subalgebra.zero_mem
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
x : ↥A
p_1 p : K[X]
hp : p ≠ 0
ih :
  ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
x_eq : x = 0
⊢ 0 ∈ A

Tactic:
exact A.zero_mem

Premises used: Subalgebra.zero_mem
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
A : Subalgebra K L
inst_3 : Algebra.IsAlgebraic K L
⊢ Nontrivial.{u_2} ↥A

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
x : A
hx : Transcendental R x
⊢ Infinite A

Tactic:
.of_injective _ (transcendental_iff_injective.mp hx)

Premises used: Infinite.of_injective, transcendental_iff_injective, Iff.mp
-- Module: Mathlib.RingTheory.Algebraic.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : Nontrivial R
inst_4 : Algebra.Transcendental R A
⊢ Infinite A

Tactic:
have ⟨x, hx⟩ := ‹Algebra.Transcendental R A›
  hx.infinite

Premises used: _private.0.Algebra.Transcendental.infinite.match_1, Transcendental.infinite, Infinite
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
x : L
p : { x_1 : R[X] // x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L) } :=
  Classical.indefiniteDescription
    (fun (x_1 : R[X]) ↦ x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L)) ⋯
⊢ Ne (α := L[X]) (Polynomial.map (algebraMap R L) (↑p : R[X])) 0

Tactic:
have := (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective R L)).2 p.2.1
-- Module: Mathlib.RingTheory.Algebraic.Cardinality
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
L : Type v
inst_2 : CommRing L
inst_3 : IsDomain L
inst_4 : Algebra R L
inst_5 : IsTorsionFree R L
inst_6 : Algebra.IsAlgebraic R L
x : L
p : { x_1 : R[X] // x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L) } :=
  Classical.indefiniteDescription
    (fun (x_1 : R[X]) ↦ x_1 ≠ 0 ∧ Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) x_1 : L) (0 : L)) ⋯
this : Ne (α := L[X]) (Polynomial.map (algebraMap R L) (↑p : R[X])) 0
rw : Polynomial.IsRoot (Polynomial.map (algebraMap R L) (↑p : R[X])) x
rw₁ : Polynomial.eval x (Polynomial.map (algebraMap R L) (↑p : R[X])) = 0
rw₂ : Polynomial.eval₂ (algebraMap R L) x (↑p : R[X]) = 0
rw₃ : Eq.{v + 1} (α := L) ((Polynomial.aeval x : (a : R[X]) → L) (↑p : R[X]) : L) (0 : L)
rw₄ rw₅ : Eq.{v + 1} (α := L) 0 0
⊢ x ∈ (↑p : R[X]).aroots L

Tactic:
rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
          ← Polynomial.aeval_def, p.2.2]

Premises used: Polynomial.eval_map, Polynomial.IsRoot, Polynomial.aeval_def, And.right, Polynomial.mem_roots, Subtype.property