awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Algebraic.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
A : Type u_3
inst_1 : CommRing S
inst_2 : NoZeroDivisors S
inst_3 : Algebra R S
alg : Algebra.IsAlgebraic R S
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : FaithfulSMul R A
⊢ FaithfulSMul S A
have rw : Function.Injective.{u_1 + 1, u_3 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A) →
  Function.Injective.{u_2 + 1, u_3 + 1} (α := S) (β := A) (⇑(algebraMap S A) : (a : S) → A)
Tactic: rw [faithfulSMul_iff_algebraMap_injective] at *
Cleared hypotheses: inst_8
-- 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
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
⊢ x⁻¹ =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
have rw : (aeval x : (a : K[X]) → L) p =
  HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
    ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
Tactic: rw [inv_eq_iff_eq_inv, inv_div, eq_comm, div_eq_iff, sub_eq_iff_eq_add, mul_comm]
-- 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
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
| ((aeval x : (a : K[X]) → L) p : L)
have 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)
Tactic: rw [← divX_mul_X_add p]
-- 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
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
⊢ (aeval x : (a : K[X]) → L) p =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
have conv_lhs : (aeval x : (a : K[X]) → L) (HAdd.hAdd (β := K[X]) (p.divX * X) ((C : (a : K) → K[X]) (p.coeff 0) : K[X])) =
  HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
    ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
Tactic: conv_lhs => rw [← divX_mul_X_add p]
-- 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
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (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])) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
have rw : 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) =
  HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
    ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
Tactic: rw [map_add, map_mul, aeval_X, aeval_C]
-- 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
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
rw :
  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) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap 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])) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
have rw₁ : 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) =
  HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
    ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
Tactic: rw [map_add, map_mul, aeval_X, aeval_C]
-- 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
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
rw :
  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) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
rw₁ :
  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) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap 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])) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
have rw₂ : HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
    ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L) =
  HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
    ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
Tactic: rw [map_add, map_mul, aeval_X, aeval_C]
-- 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
x : L
p : K[X]
aeval_ne : Ne.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) (0 : L)
rw :
  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) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
rw₁ :
  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) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
rw₂ :
  HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((aeval x : (a : K[X]) → L) ((C : (a : K) → K[X]) (p.coeff 0) : K[X]) : L) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap 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])) =
    HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
      ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
have rw₃ : HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
    ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
  HAdd.hAdd (β := L) (HMul.hMul (α := L) ((aeval x : (a : K[X]) → L) p.divX : L) x)
    ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
Tactic: rw [map_add, map_mul, aeval_X, aeval_C]
-- 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
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
⊢ x⁻¹ =
    -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
have h : -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
  HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
    (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
Tactic: convert!
    inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
      (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1
-- 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
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 :
  -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
⊢ x⁻¹ =
    -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
have convert_2 : ∀ (h : Eq.{u_2 + 1} (α := L) ((aeval x : (a : K[X]) → L) p.divX : 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: convert!
    inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
      (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1
-- 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
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
⊢ -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
have h : -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
  HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
    (HSub.hSub (α := L) (β := L) (0 : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
Tactic: rw [aeval_eq, zero_sub, div_neg]
-- 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
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 :
  -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) (0 : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
⊢ -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
have h₁ : -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
  HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L) (-(algebraMap K L : (a : K) → L) (p.coeff 0) : L)
Tactic: rw [aeval_eq, zero_sub, div_neg]
-- 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
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 :
  -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) (0 : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
h₁ :
  -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (-(algebraMap K L : (a : K) → L) (p.coeff 0) : L)
⊢ -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L)
        ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
    HDiv.hDiv (α := L) ((aeval x : (a : K[X]) → L) p.divX : L)
      (HSub.hSub (α := L) (β := L) ((aeval x : (a : K[X]) → L) p : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L))
have h₂ : -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L) =
  -HDiv.hDiv (α := L) (β := L) ((aeval x : (a : K[X]) → L) p.divX : L) ((algebraMap K L : (a : K) → L) (p.coeff 0) : L)
Tactic: rw [aeval_eq, zero_sub, div_neg]
-- 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
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) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L)
    (((algebraMap K L : K →+* L) : (a : K) → L) 0 : L)
have convert_2 : Eq.{u_2 + 1} (α := L) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L) (0 : L)
Tactic: rw [RingHom.map_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
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) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L) (0 : L)
have 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)
Tactic: convert! 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
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)
| ((aeval x : (a : K[X]) → L) p : L)
have 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)
Tactic: rw [← divX_mul_X_add p]
-- 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
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) (((algebraMap K L : K →+* L) : (a : K) → L) (p.coeff 0) : L) ((aeval x : (a : K[X]) → L) p : L)
have 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)
Tactic: conv_rhs => rw [← divX_mul_X_add p]
-- 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
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) (((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)
have 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)
Tactic: rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]
-- 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
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)
⊢ 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)
have 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)
Tactic: rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]