awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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
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.{u_7 + 1} (α := S') ((pb.equivOfRoot pb' h₁ h₂ : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) f : S) : S')
    ((aeval pb'.gen : (a : A[X]) → S') f : S')

Tactic:
pb.lift_aeval _ h₂ _

Premises used: Multiset.sum, Multiset.foldr, PowerBasis.lift_aeval, Finsupp.sum, 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
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')
⊢ (pb.equivOfRoot pb' h₁ h₂ : (a : S) → S') pb.gen = pb'.gen

Tactic:
pb.lift_gen _ h₂

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, PowerBasis.lift_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
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')
⊢ (pb.equivOfRoot pb' h₁ h₂).symm = pb'.equivOfRoot pb h₂ h₁

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.ofAlgHom, PowerBasis.equivOfRoot, Equiv.symm, 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
pb' : PowerBasis A S'
h : Eq (α := A[X]) (minpoly A pb.gen) (minpoly A pb'.gen)
f : A[X]
⊢ Eq.{u_7 + 1} (α := S') ((pb.equivOfMinpoly pb' h : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) f : S) : S')
    ((aeval pb'.gen : (a : A[X]) → S') f : S')

Tactic:
pb.equivOfRoot_aeval pb' _ _ _

Premises used: PowerBasis.equivOfRoot_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
pb' : PowerBasis A S'
h : Eq (α := A[X]) (minpoly A pb.gen) (minpoly A pb'.gen)
⊢ (pb.equivOfMinpoly pb' h : (a : S) → S') pb.gen = pb'.gen

Tactic:
pb.equivOfRoot_gen pb' _ _

Premises used: PowerBasis.equivOfRoot_gen
-- 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
pb' : PowerBasis A S'
h : Eq (α := A[X]) (minpoly A pb.gen) (minpoly A pb'.gen)
⊢ (pb.equivOfMinpoly pb' h).symm = pb'.equivOfMinpoly pb ⋯

Tactic:
rfl

Premises used: AlgEquiv.symm, AlgEquiv.ofAlgHom, PowerBasis.equivOfRoot, Equiv.symm, PowerBasis.equivOfMinpoly, rfl
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
pos :
  ∀ (h : IsIntegral K x),
    LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)
neg :
  ∀ (h : ¬IsIntegral K x),
    LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)

Tactic:
by_cases h : IsIntegral K x

Premises used: IsIntegral
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : ¬IsIntegral K x
neg : LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin 0) ↦ x ^ (↑i : ℕ)
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)

Tactic:
rw [minpoly.eq_zero h, natDegree_zero]

Premises used: Polynomial.natDegree_zero, minpoly.eq_zero
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin 0) ↦ x ^ (↑i : ℕ)

Tactic:
linearIndependent_empty_type

Premises used: linearIndependent_empty_type
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : ¬IsIntegral K x
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin 0) ↦ x ^ (↑i : ℕ)

Tactic:
exact linearIndependent_empty_type

Premises used: linearIndependent_empty_type
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)

Tactic:
Fintype.linearIndependent_iff.2 fun g hg i => ?_

Premises used: Iff.mpr, Fintype.linearIndependent_iff
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
pos :
  ∀ (g : Fin (natDegree (minpoly K x)) → K)
    (hg : Eq.{u_2 + 1} (α := S) (∑ i : Fin (minpoly K x).natDegree, g i • x ^ (↑i : ℕ)) 0)
    (i : Fin (natDegree (minpoly K x))), g i = 0
⊢ LinearIndependent.{0, u_6, u_2} K (M := S) fun (i : Fin (natDegree (minpoly K x))) ↦ x ^ (↑i : ℕ)

Tactic:
refine Fintype.linearIndependent_iff.2 fun g hg i => ?_

Premises used: Iff.mpr, Fintype.linearIndependent_iff
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
hg : Eq.{u_2 + 1} (α := S) (∑ i : Fin (minpoly K x).natDegree, g i • x ^ (↑i : ℕ)) 0
i : Fin (natDegree (minpoly K x))
⊢ Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)

Tactic:
simp_rw [Algebra.smul_def, ← aeval_monomial, ← map_sum] at hg

Premises used: map_sum, Polynomial.aeval_monomial, Algebra.smul_def
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
pos :
  degree.{u_6} (R := K) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) <
    degree (minpoly K x)
apply :
  ∀ (hn0 : ¬g i = 0)
    (h0 :
      Eq.{u_6 + 1} (α := K[X]) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) 0),
    g i = 0
⊢ g i = 0

Tactic:
apply (fun hn0 => (minpoly.degree_le_of_ne_zero K x (mt (fun h0 => ?_) hn0) hg).not_gt).mtr

Premises used: mt, minpoly.degree_le_of_ne_zero, LE.le.not_gt, Function.mtr
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
pos :
  degree.{u_6} (R := K)
      (∑ x_1 : Fin (minpoly K x).natDegree,
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g x_1) : K[X]) (HPow.hPow (α := K[X]) X (↑x_1 : ℕ))) <
    degree (minpoly K x)
⊢ degree.{u_6} (R := K) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) <
    degree (minpoly K x)

Tactic:
simp_rw [← C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
⊢ degree.{u_6} (R := K)
      (∑ x_1 : Fin (minpoly K x).natDegree,
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g x_1) : K[X]) (HPow.hPow (α := K[X]) X (↑x_1 : ℕ))) <
    degree (minpoly K x)

Tactic:
(degree_eq_natDegree <| minpoly.ne_zero h).symm ▸ degree_sum_fin_lt _

Premises used: Polynomial.degree_eq_natDegree, Eq.rec, Eq.symm, Polynomial.degree_sum_fin_lt, minpoly.ne_zero
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
⊢ degree.{u_6} (R := K)
      (∑ x_1 : Fin (minpoly K x).natDegree,
        HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) (g x_1) : K[X]) (HPow.hPow (α := K[X]) X (↑x_1 : ℕ))) <
    degree (minpoly K x)

Tactic:
exact (degree_eq_natDegree <| minpoly.ne_zero h).symm ▸ degree_sum_fin_lt _
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
hn0 : ¬g i = 0
h0 : Eq.{u_6 + 1} (α := K[X]) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) 0
⊢ Eq (α := K)
    ((lcoeff K (↑i : ℕ) : (a : K[X]) → K)
        (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      K)
    ((lcoeff K (↑i : ℕ) : (a : K[X]) → K) 0 : K)

Tactic:
apply_fun lcoeff K i at h0

Premises used: Fin.val, Polynomial.lcoeff
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
hn0 : ¬g i = 0
h0 :
  Eq (α := K)
    ((lcoeff K (↑i : ℕ) : (a : K[X]) → K)
        (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      K)
    ((lcoeff K (↑i : ℕ) : (a : K[X]) → K) 0 : K)
⊢ (if Membership.mem (γ := Finset (Fin (natDegree (minpoly K x)))) Finset.univ i then g i else 0) = coeff 0 (↑i : ℕ)

Tactic:
simp_rw [map_sum, lcoeff_apply, coeff_monomial, Fin.val_eq_val, Finset.sum_ite_eq'] at h0

Premises used: Finset.sum_ite_eq', Polynomial.coeff_monomial, Polynomial.lcoeff_apply, map_sum, Fin.val_eq_val
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
hn0 : ¬g i = 0
h0 : (if Membership.mem (γ := Finset (Fin (natDegree (minpoly K x)))) Finset.univ i then g i else 0) = coeff 0 (↑i : ℕ)
⊢ g i = 0

Tactic:
(if_pos <| Finset.mem_univ _).symm.trans h0

Premises used: Finset.mem_univ, if_pos, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
K : Type u_6
inst_1 : Field K
inst_2 : Algebra K S
x : S
h : IsIntegral K x
g : Fin (natDegree (minpoly K x)) → K
i : Fin (natDegree (minpoly K x))
hg :
  Eq.{u_2 + 1} (α := S)
    ((aeval x : (a : K[X]) → S) (∑ x_1 : Fin (minpoly K x).natDegree, (monomial (↑x_1 : ℕ) : (a : K) → K[X]) (g x_1)) :
      S)
    (0 : S)
hn0 : ¬g i = 0
h0 : (if Membership.mem (γ := Finset (Fin (natDegree (minpoly K x)))) Finset.univ i then g i else 0) = coeff 0 (↑i : ℕ)
⊢ g i = 0

Tactic:
exact (if_pos <| Finset.mem_univ _).symm.trans h0

Premises used: Finset.mem_univ, if_pos, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x y : S
hx : IsIntegral R x
hy : ∃ (f : R[X]), y = (aeval x : (a : R[X]) → S) f
obtain :
  ∀ (f : R[X]),
    Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S)
      (Submodule.span R (Set.range fun (i : Fin (natDegree (minpoly R x))) ↦ x ^ (↑i : ℕ)))
      ((aeval x : (a : R[X]) → S) f : S)
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R (Set.range fun (i : Fin (natDegree (minpoly R x))) ↦ x ^ (↑i : ℕ))) y

Tactic:
obtain ⟨f, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
apply :
  ∃ (f_1 : R[X]),
    f_1.degree < (↑(natDegree (minpoly R x)) : WithBot ℕ) ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) f_1 : S)
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Submodule R S)
    (Submodule.span R (Set.range fun (i : Fin (natDegree (minpoly R x))) ↦ x ^ (↑i : ℕ)))
    ((aeval x : (a : R[X]) → S) f : S)

Tactic:
apply mem_span_pow'.mpr _

Premises used: Iff.mpr, PowerBasis.mem_span_pow'
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
⊢ Monic (minpoly R x)

Tactic:
have := minpoly.monic hx
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ ∃ (f_1 : R[X]),
    f_1.degree < (↑(natDegree (minpoly R x)) : WithBot ℕ) ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) f_1 : S)

Tactic:
⟨f %ₘ minpoly R x, (degree_modByMonic_lt _ this).trans_le degree_le_natDegree, ?_⟩

Premises used: Polynomial.degree_le_natDegree, minpoly, LT.lt.trans_le, Polynomial.modByMonic, And.intro, Polynomial.degree_modByMonic_lt, Exists.intro
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
refine : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x) : S)
⊢ ∃ (f_1 : R[X]),
    f_1.degree < (↑(natDegree (minpoly R x)) : WithBot ℕ) ∧
      Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) f_1 : S)

Tactic:
refine ⟨f %ₘ minpoly R x, (degree_modByMonic_lt _ this).trans_le degree_le_natDegree, ?_⟩
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
rw : ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) : S)
| ((aeval x : (a : R[X]) → S) f : S)

Tactic:
rw [← modByMonic_add_div f (minpoly R x)]

Premises used: minpoly, Polynomial.modByMonic_add_div
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
conv_lhs :
  Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) : S)
    ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x) : S)
⊢ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) f : S) ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x) : S)

Tactic:
conv_lhs => rw [← modByMonic_add_div f (minpoly R x)]

Premises used: minpoly, Polynomial.modByMonic_add_div
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial R
x : S
hx : IsIntegral R x
f : R[X]
this : Monic (minpoly R x)
⊢ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x + minpoly R x * (f /ₘ minpoly R x)) : S)
    ((aeval x : (a : R[X]) → S) (f %ₘ minpoly R x) : S)

Tactic:
simp only [add_zero, zero_mul, minpoly.aeval, aeval_add, map_mul]

Premises used: MulZeroClass.zero_mul, minpoly.aeval, map_mul, add_zero, Polynomial.aeval_add
-- 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
S' : Type u_7
inst_7 : CommRing S'
inst_8 : Algebra R S'
pb : PowerBasis R S
e : S ≃ₐ[R] S'
i : Fin pb.dim
rw :
  ((↑e : S ≃ₗ[R] S') : (a : S) → S') ((pb.basis : (a : Fin pb.dim) → S) i : S) =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
rw₁ :
  ((↑e : S ≃ₗ[R] S') : (a : S) → S') (pb.gen ^ (↑i : ℕ)) = HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
rw₂ : (e : (a : S) → S') (pb.gen ^ (↑i : ℕ)) = HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
rw₃ rw₄ :
  HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ) =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)
⊢ (pb.basis.map (↑e : S ≃ₗ[R] S') : (a : Fin pb.dim) → S') i =
    HPow.hPow (α := S') ((e : (a : S) → S') pb.gen : S') (↑i : ℕ)

Tactic:
rw [Basis.map_apply, pb.basis_eq_pow, e.toLinearEquiv_apply, map_pow]

Premises used: map_pow, PowerBasis.basis_eq_pow, Module.Basis.map_apply, AlgEquiv.toLinearEquiv_apply
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
S' : Type u_7
inst_2 : CommRing S'
inst_3 : Algebra A S
inst_4 : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
⊢ (pb.map e).minpolyGen = pb.minpolyGen

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
S' : Type u_7
inst_2 : CommRing S'
inst_3 : Algebra A S
inst_4 : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A (pb.map e).gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval (pb.map e).gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
h :
  ∀ (x : S),
    Eq.{u_7 + 1} (α := S') ((pb.equivOfRoot (pb.map e) h₁ h₂ : (a : S) → S') x : S') ((e : (a : S) → S') x : S')
⊢ pb.equivOfRoot (pb.map e) h₁ h₂ = e

Tactic:
ext x
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
S' : Type u_7
inst_2 : CommRing S'
inst_3 : Algebra A S
inst_4 : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A (pb.map e).gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval (pb.map e).gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
x : S
h :
  ∀ (f : A[X]),
    Eq.{u_7 + 1} (α := S')
      ((pb.equivOfRoot (pb.map e) h₁ h₂ : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) f : S) : S')
      ((e : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) f : S) : S')
⊢ Eq.{u_7 + 1} (α := S') ((pb.equivOfRoot (pb.map e) h₁ h₂ : (a : S) → S') x : S') ((e : (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
S' : Type u_7
inst_2 : CommRing S'
inst_3 : Algebra A S
inst_4 : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h₁ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) (minpoly A (pb.map e).gen) : S) (0 : S)
h₂ : Eq.{u_7 + 1} (α := S') ((aeval (pb.map e).gen : (a : A[X]) → S') (minpoly A pb.gen) : S') (0 : S')
f : A[X]
⊢ Eq.{u_7 + 1} (α := S') ((pb.equivOfRoot (pb.map e) h₁ h₂ : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) f : S) : S')
    ((e : (a : S) → S') ((aeval pb.gen : (a : A[X]) → S) f : S) : S')

Tactic:
simp [aeval_algEquiv]

Premises used: Polynomial.aeval_algEquiv
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
S : Type u_2
inst : Ring S
A : Type u_4
inst_1 : CommRing A
S' : Type u_7
inst_2 : CommRing S'
inst_3 : Algebra A S
inst_4 : Algebra A S'
pb : PowerBasis A S
e : S ≃ₐ[A] S'
h : Eq (α := A[X]) (minpoly A pb.gen) (minpoly A (pb.map e).gen)
⊢ pb.equivOfMinpoly (pb.map e) h = e

Tactic:
pb.equivOfRoot_map _ _ _

Premises used: PowerBasis.equivOfRoot_map, PowerBasis.equivOfMinpoly
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
B : PowerBasis R S
rw :
  Set.range (ι := Fin B.dim) (⇑B.basis : (a : Fin B.dim) → S) ⊆
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[B.gen] : Submodule R S) : Set S)
⊢ Eq (α := Subalgebra R S) R[B.gen] ⊤

Tactic:
rw [← toSubmodule_eq_top, _root_.eq_top_iff, ← B.basis.span_eq, Submodule.span_le]

Premises used: eq_top_iff, PowerBasis.basis, Algebra.toSubmodule_eq_top, Module.Basis.span_eq, Submodule.span_le
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
B : PowerBasis R S
i : Fin B.dim
rw :
  B.gen ^ (↑i : ℕ) ∈
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[B.gen] : Submodule R S) : Set S)
⊢ Membership.mem (α := S)
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) R[B.gen] : Submodule R S) : Set S)
    ((B.basis : (a : Fin B.dim) → S) i : S)

Tactic:
rw [B.basis_eq_pow i]

Premises used: PowerBasis.basis_eq_pow