awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
S' : Type u_7
inst_3 : Semiring S'
inst_4 : Algebra R S'
pb : PowerBasis R S
f_1 g : S →ₐ[R] S'
h : Eq.{u_7 + 1} (α := S') ((f_1 : (a : S) → S') pb.gen : S') ((g : (a : S) → S') pb.gen : S')
f : R[X]
H :
  Eq.{u_7 + 1} (α := S') (((aeval ((f_1 : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
    ((g : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
H₁ :
  Eq.{u_7 + 1} (α := S') (((aeval ((f_1 : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
    (((aeval ((g : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
H₂ H₃ :
  Eq.{u_7 + 1} (α := S') (((aeval ((g : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
    (((aeval ((g : (a : S) → S') pb.gen) : R[X] →ₐ[R] S') : (a : R[X]) → S') f : S')
⊢ Eq.{u_7 + 1} (α := S') ((f_1 : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')
    ((g : (a : S) → S') ((aeval pb.gen : (a : R[X]) → S) f : S) : S')

Tactic:
rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]

Premises used: Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
inl : Subsingleton B → ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)
inr : Nontrivial B → ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)
⊢ ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)

Tactic:
rcases subsingleton_or_nontrivial B

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Subsingleton B
rw :
  Eq (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (Submodule.Quotient.mk b)
    (Submodule.Quotient.mk ((algebraMap A B : (a : A) → B) 0))
rw₁ :
  Eq.{u_5 + 1} (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk ((algebraMap A B : (a : A) → B) 0) :
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
rw₂ rw₃ :
  Eq.{u_5 + 1} (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (Submodule.Quotient.mk 0)
    (Submodule.Quotient.mk 0)
⊢ SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) 0)

Tactic:
rw [SModEq, Subsingleton.eq_zero b, map_zero]

Premises used: map_zero, Subsingleton.eq_zero, SModEq
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Subsingleton B
⊢ ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)

Tactic:
exact ⟨0, by rw [SModEq, Subsingleton.eq_zero b, map_zero]⟩
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
⊢ ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)

Tactic:
⟨pb.basis.repr b ⟨0, pb.dim_pos⟩, ?_⟩

Premises used: Fin.mk, PowerBasis.basis, Module.Basis.repr, PowerBasis.dim_pos, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
inr :
  SModEq (R := B) (Ideal.span {pb.gen}) b
    ((algebraMap A B : (a : A) → B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
          (⟨0, ⋯⟩ : Fin pb.dim) :
        A))
⊢ ∃ (a : A), SModEq (R := B) (Ideal.span {pb.gen}) b ((algebraMap A B : (a : A) → B) a)

Tactic:
refine ⟨pb.basis.repr b ⟨0, pb.dim_pos⟩, ?_⟩
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
⊢ ∑ i : Fin pb.dim,
      HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A)
        ((pb.basis : (a : Fin pb.dim) → B) i : B) =
    b

Tactic:
have H := pb.basis.sum_repr b
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  ∑ i : Fin pb.dim,
      HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A)
        ((pb.basis : (a : Fin pb.dim) → B) i : B) =
    b
⊢ HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b

Tactic:
rw [← insert_erase (mem_univ ⟨0, pb.dim_pos⟩), sum_insert (notMem_erase _ _)] at H

Premises used: Finset.mem_univ, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
inr :
  Submodule.Quotient.mk b =
    HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
          ((algebraMap A B : (a : A) → B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
                (⟨0, ⋯⟩ : Fin pb.dim) :
              A)) :
        HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
⊢ SModEq (R := B) (Ideal.span {pb.gen}) b
    ((algebraMap A B : (a : A) → B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
          (⟨0, ⋯⟩ : Fin pb.dim) :
        A))

Tactic:
rw [SModEq, ← add_zero (algebraMap _ _ _), Quotient.mk_add]

Premises used: Submodule.Quotient.mk_add, Algebra.algebraMap, add_zero, DFunLike.coe, SModEq
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
inr :
  Submodule.Quotient.mk
      (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              (⟨0, ⋯⟩ : Fin pb.dim) :
            A)
          ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
        ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
          HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
            ((pb.basis : (a : Fin pb.dim) → B) x : B)) =
    HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
          ((algebraMap A B : (a : A) → B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
                (⟨0, ⋯⟩ : Fin pb.dim) :
              A)) :
        HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
⊢ Submodule.Quotient.mk b =
    HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
          ((algebraMap A B : (a : A) → B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
                (⟨0, ⋯⟩ : Fin pb.dim) :
              A)) :
        HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))

Tactic:
nth_rewrite 1 [← H]
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
inr :
  Eq (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
      (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B)))
    (Submodule.Quotient.mk
      ((algebraMap A B : (a : A) → B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)))
inr₁ :
  Eq.{u_5 + 1} (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
      (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B)))
    (Submodule.Quotient.mk 0)
⊢ HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
        (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              (⟨0, ⋯⟩ : Fin pb.dim) :
            A)
          ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B)))
      (Submodule.Quotient.mk
        (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
          HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
            ((pb.basis : (a : Fin pb.dim) → B) x : B))) =
    HAdd.hAdd (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen})) (β :=
      HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk
          ((algebraMap A B : (a : A) → B)
            ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
                (⟨0, ⋯⟩ : Fin pb.dim) :
              A)) :
        HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
      (Submodule.Quotient.mk 0 : HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
⊢ Eq (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
      (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B)))
    (Submodule.Quotient.mk
      ((algebraMap A B : (a : A) → B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)))

Tactic:
simp [Algebra.algebraMap_eq_smul_one ((pb.basis.repr b) _)]

Premises used: PowerBasis.basis, Module.Basis.repr, Algebra.algebraMap_eq_smul_one, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
inr :
  Membership.mem (γ := Submodule B B) (Ideal.span {pb.gen})
    (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
      HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
        ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) x))
⊢ Eq.{u_5 + 1} (α := HasQuotient.Quotient B (B := Submodule B B) (Ideal.span {pb.gen}))
    (Submodule.Quotient.mk
      (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B)))
    (Submodule.Quotient.mk 0)

Tactic:
rw [Quotient.mk_zero, Quotient.mk_eq_zero, coe_basis]

Premises used: PowerBasis.coe_basis, Submodule.Quotient.mk_eq_zero, Submodule.Quotient.mk_zero
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
⊢ Membership.mem (γ := Submodule B B) (Ideal.span {pb.gen})
    (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
      HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
        ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) x))

Tactic:
sum_mem _ (fun i hi ↦ ?_)

Premises used: Set.Mem, Ideal.sum_mem
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
inr :
  ∀ (i : Fin pb.dim) (hi : i ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim)),
    Membership.mem (γ := Ideal B) (Ideal.span {pb.gen})
      (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A)
        ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) i))
⊢ Membership.mem (γ := Submodule B B) (Ideal.span {pb.gen})
    (∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
      HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
        ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) x))

Tactic:
refine sum_mem _ (fun i hi ↦ ?_)

Premises used: Ideal.sum_mem
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
i : Fin pb.dim
hi : i ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim)
inr :
  Membership.mem (γ := Ideal B) (Ideal.span {pb.gen})
    (HMul.hMul (α := B) (β := B)
      ((algebraMap A B : (a : A) → B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A) :
        B)
      ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) i : B))
⊢ Membership.mem (γ := Ideal B) (Ideal.span {pb.gen})
    (HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
      ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A)
      ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) i))

Tactic:
rw [Algebra.smul_def']

Premises used: Algebra.smul_def'
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
i : Fin pb.dim
hi : i ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim)
⊢ Membership.mem (γ := Set B) {pb.gen} pb.gen

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
h : Nontrivial B
H :
  HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
        ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
            (⟨0, ⋯⟩ : Fin pb.dim) :
          A)
        ((pb.basis : (a : Fin pb.dim) → B) (⟨0, ⋯⟩ : Fin pb.dim) : B) +
      ∑ x ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim),
        HSMul.hSMul.{u_4, u_5, u_5} (α := A) (β := B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) x : A)
          ((pb.basis : (a : Fin pb.dim) → B) x : B) =
    b
i : Fin pb.dim
hi : i ∈ Finset.erase univ (⟨0, ⋯⟩ : Fin pb.dim)
⊢ Membership.mem (γ := Ideal B) (Ideal.span {pb.gen})
    (HMul.hMul (α := B) (β := B)
      ((algebraMap A B : (a : A) → B)
          ((((pb.basis.repr : (a : B) → Fin pb.dim →₀ A) b : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A) i : A) :
        B)
      ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) i : B))

Tactic:
refine Ideal.mul_mem_left _ _ <| Ideal.pow_mem_of_mem _ (Ideal.subset_span (by simp)) _ <|
      Nat.pos_of_ne_zero <| fun h ↦ notMem_erase i univ <| Fin.eq_mk_iff_val_eq.2 h ▸ hi

Premises used: Ideal.subset_span, Finset.univ, Ideal.pow_mem_of_mem, Nat.pos_of_ne_zero, Finset.notMem_erase, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.PowerBasis
Goal:
A : Type u_4
B : Type u_5
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
pb : PowerBasis A B
b : B
⊢ ∃ (a : A), pb.gen ∣ HSub.hSub (β := B) b ((algebraMap A B : (a : A) → B) a : B)

Tactic:
simpa [← Ideal.mem_span_singleton, ← mk_eq_zero, mk_sub, sub_eq_zero] using pb.exists_smodEq b

Premises used: sub_eq_zero, Submodule.Quotient.mk_sub, PowerBasis.exists_smodEq, Ideal.mem_span_singleton, Submodule.Quotient.mk_eq_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
pb : PowerBasis A S
simp_rw :
  pb.gen ^ pb.dim -
      ∑ x : Fin pb.dim,
        HSMul.hSMul.{u_4, u_2, u_2} (α := A)
          ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              x :
            A)
          (pb.gen ^ (↑x : ℕ)) =
    0
⊢ Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : A[X]) → S) pb.minpolyGen : S) (0 : S)

Tactic:
simp_rw [minpolyGen, map_sub, map_sum, map_mul, map_pow, aeval_C, ← Algebra.smul_def, aeval_X]

Premises used: map_sub, PowerBasis.minpolyGen, map_pow, map_sum, map_mul, Polynomial.aeval_C, Algebra.smul_def, 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
pb : PowerBasis A S
⊢ pb.gen ^ pb.dim -
      ∑ x : Fin pb.dim,
        HSMul.hSMul.{u_4, u_2, u_2} (α := A)
          ((((pb.basis.repr : (a : S) → Fin pb.dim →₀ A) (pb.gen ^ pb.dim) : Fin pb.dim →₀ A) : (a : Fin pb.dim) → A)
              x :
            A)
          (pb.gen ^ (↑x : ℕ)) =
    0

Tactic:
sub_eq_zero.mpr ((pb.basis.linearCombination_repr (pb.gen ^ pb.dim)).symm.trans ?_)

Premises used: Iff.mpr, PowerBasis.dim, sub_eq_zero, PowerBasis.gen, PowerBasis.basis, HPow.hPow, Module.Basis.linearCombination_repr, Eq.symm, Eq.trans