awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ ∈ A
have rw : HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L) ∈ A
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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
⊢ (↑x : L)⁻¹ ∈ A
have suffices : (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
Tactic: suffices (x⁻¹ : L) = (-p.coeff 0)⁻¹ • aeval x (divX p) by
    rw [this]
    exact A.smul_mem (aeval x _).2 _
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
have rw : Eq.{u_2 + 1} (α := L) (↑((aeval x : (a : K[X]) → ↥A) p) : L) 0
Tactic: rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := L) ((aeval (↑x : L) : (a : K[X]) → L) p : L) (0 : L)
have rw₁ : Eq.{u_2 + 1} (α := L) (↑0 : L) 0
Tactic: rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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
⊢ Eq.{u_2 + 1} (α := L) ((aeval (↑x : L) : (a : K[X]) → L) p : L) (0 : L)
have rw₂ : Eq.{u_2 + 1} (α := L) 0 0
Tactic: rw [Subalgebra.aeval_coe, aeval_eq, Subalgebra.coe_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
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
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ = HSMul.hSMul (β := L) (-p.coeff 0)⁻¹ (↑((aeval x : (a : K[X]) → ↥A) p.divX) : L)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (↑x : L)⁻¹ ∈ A
have 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
Tactic: obtain ⟨p, ne_zero, aeval_eq⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (hypothesis)
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)
⊢ (↑x : L)⁻¹ ∈ A
have aeval_eq₁ : 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
Cleared hypotheses: aeval_eq
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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
have 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
Tactic: revert ne_zero aeval_eq
Cleared hypotheses: ne_zero, aeval_eq
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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
have 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
Tactic: refine p.recOnHorner ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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
⊢ ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
have 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
Tactic: refine p.recOnHorner ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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
⊢ ∀ (ne_zero : p ≠ 0) (aeval_eq : Eq.{u_2 + 1} (α := ↥A) ((aeval x : (a : K[X]) → ↥A) p : ↥A) (0 : ↥A)), (↑x : L)⁻¹ ∈ A
have 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
Tactic: refine p.recOnHorner ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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
have refine_2 : (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])).coeff 0 ≠ 0
Tactic: refine A.inv_mem_of_root_of_coeff_zero_ne_zero aeval_eq ?_
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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)
⊢ (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])).coeff 0 ≠ 0
have refine_2 : p.coeff 0 + coeff ((C : (a : K) → K[X]) a) 0 ≠ 0
Tactic: rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
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
⊢ (HAdd.hAdd (β := K[X]) p ((C : (a : K) → K[X]) a : K[X])).coeff 0 ≠ 0
have refine_2₁ : HAdd.hAdd (α := K) 0 (coeff ((C : (a : K) → K[X]) a) 0) ≠ 0
Tactic: rwa [coeff_add, hp, zero_add, coeff_C, if_pos rfl]