awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
h : Nontrivial A
hf : ¬f %ₘ minpoly A pb.gen = 0
this : (f %ₘ minpoly A pb.gen).natDegree < pb.dim
i : ℕ
hi : i < pb.dim
neg :
  ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (pb.gen ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ)) =
    y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ)
neg₁ :
  ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      ((pb.basis : (a : Fin pb.dim) → S) (⟨i, hi⟩ : Fin pb.dim) : S) =
    y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ)
neg₂ neg₃ : y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ) = y ^ (↑(⟨i, hi⟩ : Fin pb.dim) : ℕ)
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (pb.gen ^ i) =
    y ^ i

Tactic:
rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]

Premises used: Fin.val_mk, Fin.mk, PowerBasis.basis_eq_pow, Module.Basis.constr_basis
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) X : S) :
      S')
    ((aeval y : (a : A[X]) → S') X : S')

Tactic:
pb.constr_pow_aeval hy X

Premises used: Polynomial.X, PowerBasis.constr_pow_aeval
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h : pb.gen = (aeval pb.gen : (a : A[X]) → S) X
h₁ : y = (aeval y : (a : A[X]) → S') X
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S') pb.gen =
    y

Tactic:
convert! pb.constr_pow_aeval hy X

Premises used: Polynomial.X, PowerBasis.constr_pow_aeval
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h h₁ : pb.gen = pb.gen
⊢ pb.gen = (aeval pb.gen : (a : A[X]) → S) X

Tactic:
rw [aeval_X]

Premises used: Polynomial.aeval_X
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h h₁ : y = y
⊢ y = (aeval y : (a : A[X]) → S') X

Tactic:
rw [aeval_X]

Premises used: Polynomial.aeval_X
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x : A
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((aeval pb.gen : (a : A[X]) → S) ((C : (a : A) → A[X]) x : A[X]) : S) :
      S')
    ((aeval y : (a : A[X]) → S') ((C : (a : A) → A[X]) x : A[X]) : S')

Tactic:
pb.constr_pow_aeval hy (C x)

Premises used: Polynomial.C, DFunLike.coe, PowerBasis.constr_pow_aeval
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x : A
h :
  Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S)
    ((aeval pb.gen : (a : A[X]) → S) ((C : (a : A) → A[X]) x : A[X]) : S)
h₁ :
  Eq.{u_7 + 1} (α := S') ((algebraMap A S' : (a : A) → S') x : S')
    ((aeval y : (a : A[X]) → S') ((C : (a : A) → A[X]) x : A[X]) : S')
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((algebraMap A S : (a : A) → S) x : S) :
      S')
    ((algebraMap A S' : (a : A) → S') x : S')

Tactic:
convert! pb.constr_pow_aeval hy (C x)

Premises used: Polynomial.C, DFunLike.coe, PowerBasis.constr_pow_aeval
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x : A
h h₁ : Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S) ((algebraMap A S : (a : A) → S) x : S)
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap A S : (a : A) → S) x : S)
    ((aeval pb.gen : (a : A[X]) → S) ((C : (a : A) → A[X]) x : A[X]) : S)

Tactic:
rw [aeval_C]

Premises used: Polynomial.aeval_C
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x : A
h h₁ : Eq.{u_7 + 1} (α := S') ((algebraMap A S' : (a : A) → S') x : S') ((algebraMap A S' : (a : A) → S') x : S')
⊢ Eq.{u_7 + 1} (α := S') ((algebraMap A S' : (a : A) → S') x : S')
    ((aeval y : (a : A[X]) → S') ((C : (a : A) → A[X]) x : A[X]) : S')

Tactic:
rw [aeval_C]

Premises used: Polynomial.aeval_C
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x x' : S
obtain :
  ∀ (f : A[X]),
    ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        (HMul.hMul (α := S) ((aeval pb.gen : (a : A[X]) → S) f : S) x') =
      HMul.hMul (α := S') (β := S')
        (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
            ((aeval pb.gen : (a : A[X]) → S) f : S) :
          S')
        (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
            x' :
          S')
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (x * x') =
    HMul.hMul (α := S') (β := S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S') x :
        S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          x' :
        S')

Tactic:
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x

Premises used: PowerBasis.exists_eq_aeval', rfl
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x' : S
f : A[X]
obtain :
  ∀ (g : A[X]),
    ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        (HMul.hMul (α := S) (β := S) ((aeval pb.gen : (a : A[X]) → S) f : S) ((aeval pb.gen : (a : A[X]) → S) g : S)) =
      HMul.hMul (α := S') (β := S')
        (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
            ((aeval pb.gen : (a : A[X]) → S) f : S) :
          S')
        (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
            ((aeval pb.gen : (a : A[X]) → S) g : S) :
          S')
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (HMul.hMul (α := S) ((aeval pb.gen : (a : A[X]) → S) f : S) x') =
    HMul.hMul (α := S') (β := S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          ((aeval pb.gen : (a : A[X]) → S) f : S) :
        S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          x' :
        S')

Tactic:
obtain ⟨g, rfl⟩ := pb.exists_eq_aeval' x'

Premises used: PowerBasis.exists_eq_aeval', rfl
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f g : A[X]
⊢ ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
      (HMul.hMul (α := S) (β := S) ((aeval pb.gen : (a : A[X]) → S) f : S) ((aeval pb.gen : (a : A[X]) → S) g : S)) =
    HMul.hMul (α := S') (β := S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          ((aeval pb.gen : (a : A[X]) → S) f : S) :
        S')
      (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
          ((aeval pb.gen : (a : A[X]) → S) g : S) :
        S')

Tactic:
simp only [← aeval_mul, pb.constr_pow_aeval hy]

Premises used: Polynomial.aeval_mul, PowerBasis.constr_pow_aeval
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((algebraMap A S : (a : A) → S) 1 : S) :
      S')
    ((algebraMap A S' : (a : A) → S') 1 : S')

Tactic:
pb.constr_pow_algebraMap hy 1

Premises used: PowerBasis.constr_pow_algebraMap, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h : Eq.{u_2 + 1} (α := S) (1 : S) ((algebraMap A S : (a : A) → S) 1 : S)
h₁ : Eq.{u_7 + 1} (α := S') (1 : S') ((algebraMap A S' : (a : A) → S') 1 : S')
⊢ Eq.{u_7 + 1} (α := S')
    (AddHom.toFun.{u_2, u_7} (M := S)
      (LinearMap.toAddHom.{u_4, u_4, u_2, u_7} (R := A) (S := A) (σ := RingHom.id A)
        ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ)))
      1)
    1

Tactic:
convert! pb.constr_pow_algebraMap hy 1 using 2

Premises used: PowerBasis.constr_pow_algebraMap, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h h₁ : Eq.{u_2 + 1} (α := S) 1 1
⊢ Eq.{u_2 + 1} (α := S) (1 : S) ((algebraMap A S : (a : A) → S) 1 : S)

Tactic:
rw [map_one]

Premises used: map_one
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h h₁ : Eq.{u_7 + 1} (α := S') 1 1
⊢ Eq.{u_7 + 1} (α := S') (1 : S') ((algebraMap A S' : (a : A) → S') 1 : S')

Tactic:
rw [map_one]

Premises used: map_one
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
⊢ Eq.{u_7 + 1} (α := S')
    (((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ) : (a : S) → S')
        ((algebraMap A S : (a : A) → S) 0 : S) :
      S')
    ((algebraMap A S' : (a : A) → S') 0 : S')

Tactic:
pb.constr_pow_algebraMap hy 0

Premises used: PowerBasis.constr_pow_algebraMap, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h : Eq.{u_2 + 1} (α := S) (0 : S) ((algebraMap A S : (a : A) → S) 0 : S)
h₁ : Eq.{u_7 + 1} (α := S') (0 : S') ((algebraMap A S' : (a : A) → S') 0 : S')
⊢ Eq.{u_7 + 1} (α := S')
    (AddHom.toFun.{u_2, u_7} (M := S)
      (LinearMap.toAddHom.{u_4, u_4, u_2, u_7} (R := A) (S := A) (σ := RingHom.id A)
        ((pb.basis.constr A : (a : Fin pb.dim → S') → S →ₗ[A] S') fun (i : Fin pb.dim) ↦ y ^ (↑i : ℕ)))
      0)
    0

Tactic:
convert! pb.constr_pow_algebraMap hy 0 using 2

Premises used: PowerBasis.constr_pow_algebraMap, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h h₁ : Eq.{u_2 + 1} (α := S) 0 0
⊢ Eq.{u_2 + 1} (α := S) (0 : S) ((algebraMap A S : (a : A) → S) 0 : S)

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h h₁ : Eq.{u_7 + 1} (α := S') 0 0
⊢ Eq.{u_7 + 1} (α := S') (0 : S') ((algebraMap A S' : (a : A) → S') 0 : S')

Tactic:
rw [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
⊢ (pb.lift y hy : (a : S) → S') pb.gen = y

Tactic:
pb.constr_pow_gen hy

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, PowerBasis.constr_pow_gen, Finset.sum
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
inst_2 : Algebra A S
S' : Type u_7
inst_3 : Ring S'
inst_4 : Algebra A S'
pb : PowerBasis A S
y : S'
hy : Eq.{u_7 + 1} (α := S') ((aeval y : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
⊢ Eq.{u_7 + 1} (α := S') ((pb.lift y hy : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) f : S) : S')
    ((aeval y : (a : A[X]) → S') f : S')

Tactic:
pb.constr_pow_aeval hy f

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, PowerBasis.constr_pow_aeval, Finset.sum
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
f : S →ₐ[A] S'
rw : Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb.gen) : S) : S') (0 : S')
rw₁ : Eq.{u_7 + 1} (α := S') ((f : (a : S) → S') 0 : S') (0 : S')
rw₂ rw₃ : Eq.{u_7 + 1} (α := S') 0 0
⊢ Eq.{u_7 + 1} (α := S')
    (((aeval ((f : (a : S) → S') pb.gen) : A[X] →ₐ[A] S') : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')

Tactic:
rw [aeval_algHom_apply, minpoly.aeval, map_zero]

Premises used: map_zero, minpoly.aeval, Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
inst_10 : IsDomain B
pb : PowerBasis A S
x : B
rw :
  Eq.{u_5 + 1} (α := B) ((aeval x : (a : A[X]) → B) (minpoly A pb.gen) : B) (0 : B) ↔
    Eq (α := B) ((aeval x : (a : B[X]) → B) (map (algebraMap A B) (minpoly A pb.gen)) : B) (0 : B)
rw₁ : Ne (α := B[X]) (map (algebraMap A B) (minpoly A pb.gen)) 0
⊢ Eq.{u_5 + 1} (α := B) ((aeval x : (a : A[X]) → B) (minpoly A pb.gen) : B) (0 : B) ↔
    Membership.mem (α := B) (aroots (minpoly A pb.gen) B) ((Equiv.refl B : (a : B) → B) x : B)

Tactic:
rw [Equiv.refl_apply, mem_roots_iff_aeval_eq_zero]

Premises used: Equiv.refl_apply, Polynomial.mem_roots_iff_aeval_eq_zero
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
inst_10 : IsDomain B
pb : PowerBasis A S
x : B
⊢ Eq.{u_5 + 1} (α := B) ((aeval x : (a : A[X]) → B) (minpoly A pb.gen) : B) (0 : B) ↔
    Eq (α := B) ((aeval x : (a : B[X]) → B) (map (algebraMap A B) (minpoly A pb.gen)) : B) (0 : B)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
inst_10 : IsDomain B
pb : PowerBasis A S
x : B
⊢ Ne (α := B[X]) (map (algebraMap A B) (minpoly A pb.gen)) 0

Tactic:
map_monic_ne_zero (minpoly.monic pb.isIntegral_gen)

Premises used: minpoly.monic, PowerBasis.isIntegral_gen, Polynomial.map_monic_ne_zero
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
inst_10 : IsDomain B
pb : PowerBasis A S
x : B
⊢ Ne (α := B[X]) (map (algebraMap A B) (minpoly A pb.gen)) 0

Tactic:
exact map_monic_ne_zero (minpoly.monic pb.isIntegral_gen)

Premises used: minpoly.monic, PowerBasis.isIntegral_gen, Polynomial.map_monic_ne_zero
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb'.gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval pb'.gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
H :
  ∀ (x : S'),
    Eq (α := S') (((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) : (a : S') → S') x : S')
      ((AlgHom.id A S' : (a : S') → S') x : S')
⊢ (pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) = AlgHom.id A S'

Tactic:
ext x
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb'.gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval pb'.gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x : S'
H :
  ∀ (f : A[X]),
    Eq (α := S')
      (((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) : (a : S') → S') ((aeval pb'.gen : (a : A[X]) → S') f : S') : S')
      ((AlgHom.id A S' : (a : S') → S') ((aeval pb'.gen : (a : A[X]) → S') f : S') : S')
⊢ Eq (α := S') (((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) : (a : S') → S') x : S')
    ((AlgHom.id A S' : (a : S') → S') x : S')

Tactic:
obtain ⟨f, hf, rfl⟩ := pb'.exists_eq_aeval' x

Premises used: PowerBasis.exists_eq_aeval', rfl
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb'.gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval pb'.gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
⊢ Eq (α := S')
    (((pb.lift pb'.gen h₂).comp (pb'.lift pb.gen h₁) : (a : S') → S') ((aeval pb'.gen : (a : A[X]) → S') f : S') : S')
    ((AlgHom.id A S' : (a : S') → S') ((aeval pb'.gen : (a : A[X]) → S') f : S') : S')

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
A : Type u_4
B : Type u_5
inst_3 : CommRing A
inst_4 : CommRing B
inst_5 : Algebra A B
K : Type u_6
inst_6 : Field K
inst_7 : Algebra A S
S' : Type u_7
inst_8 : Ring S'
inst_9 : Algebra A S'
pb : PowerBasis A S
pb' : PowerBasis A S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A pb'.gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval pb'.gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
H :
  ∀ (x : S),
    Eq (α := S) (((pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂) : (a : S) → S) x : S)
      ((AlgHom.id A S : (a : S) → S) x : S)
⊢ (pb'.lift pb.gen h₁).comp (pb.lift pb'.gen h₂) = AlgHom.id A S

Tactic:
ext x