awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
y : S
hy : Membership.mem (γ := Subalgebra K S) K[x] y
h :
  Membership.mem (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
this :
  ∀
    (hy_1 :
      ∃ (f : K[X]),
        Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy =
          (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f),
    Membership.mem (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
hy₁ : Membership.mem (γ := Subalgebra K S) (AlgHom.range (aeval x)) y
⊢ Membership.mem (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)

Tactic:
rw [adjoin_singleton_eq_range_aeval] at hy

Premises used: Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
y : S
hy : Membership.mem (γ := Subalgebra K S) K[x] y
h :
  Membership.mem (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
this :
  ∀
    (hy_1 :
      ∃ (f : K[X]),
        Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy =
          (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f),
    Membership.mem (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
hy₁ : Membership.mem (γ := Subalgebra K S) (AlgHom.range (aeval x)) y
a :
  Membership.mem (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)
⊢ ∀
    (hy_1 :
      ∃ (f : K[X]),
        Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy =
          (aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f),
    Membership.mem (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) y hy)

Tactic:
rw [adjoin_singleton_eq_range_aeval] at hy

Premises used: Algebra.adjoin_singleton_eq_range_aeval
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
f : K[X]
hy_1 : Membership.mem (α := S) (γ := Subalgebra K S) K[x] ((aeval x : (a : K[X]) → S) f : S)
hy : Membership.mem (α := S) (γ := Subalgebra K S) (AlgHom.range (aeval x)) ((aeval x : (a : K[X]) → S) f : S)
h_1 :
  Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
        hy_1 :
      ↥K[x])
this :
  ∀
    (hy :
      ∃ (f_1 : K[X]),
        Eq.{u_2 + 1} (α := ↥K[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1)
              ((aeval x : (a : K[X]) → S) f) hy_1 :
            ↥K[x])
          ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                (a : K[X]) → ↥K[x])
              f_1 :
            ↥K[x])),
    Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
          hy_1 :
        ↥K[x])
h :
  Eq.{u_2 + 1} (α := ↥K[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
        hy_1 :
      ↥K[x])
    ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) : (a : K[X]) → ↥K[x])
        f :
      ↥K[x])
⊢ ∃ (f_1 : K[X]),
    Eq.{u_2 + 1} (α := ↥K[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
          hy_1 :
        ↥K[x])
      ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
            (a : K[X]) → ↥K[x])
          f_1 :
        ↥K[x])

Tactic:
use f
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
f : K[X]
hy_1 : Membership.mem (α := S) (γ := Subalgebra K S) K[x] ((aeval x : (a : K[X]) → S) f : S)
hy : Membership.mem (α := S) (γ := Subalgebra K S) (AlgHom.range (aeval x)) ((aeval x : (a : K[X]) → S) f : S)
h_1 :
  Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
        hy_1 :
      ↥K[x])
this :
  ∀
    (hy :
      ∃ (f_1 : K[X]),
        Eq.{u_2 + 1} (α := ↥K[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1)
              ((aeval x : (a : K[X]) → S) f) hy_1 :
            ↥K[x])
          ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                (a : K[X]) → ↥K[x])
              f_1 :
            ↥K[x])),
    Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
          hy_1 :
        ↥K[x])
h :
  Eq.{u_2 + 1} (α := S)
    ((↑(Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
            hy_1) :
        S) :
      S)
    ((↑((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f) :
        S) :
      S)
⊢ Eq.{u_2 + 1} (α := ↥K[x])
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
        hy_1 :
      ↥K[x])
    ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) : (a : K[X]) → ↥K[x])
        f :
      ↥K[x])

Tactic:
ext
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
f : K[X]
hy_1 : Membership.mem (α := S) (γ := Subalgebra K S) K[x] ((aeval x : (a : K[X]) → S) f : S)
hy : Membership.mem (α := S) (γ := Subalgebra K S) (AlgHom.range (aeval x)) ((aeval x : (a : K[X]) → S) f : S)
h :
  Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
        hy_1 :
      ↥K[x])
this :
  ∀
    (hy :
      ∃ (f_1 : K[X]),
        Eq.{u_2 + 1} (α := ↥K[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1)
              ((aeval x : (a : K[X]) → S) f) hy_1 :
            ↥K[x])
          ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                (a : K[X]) → ↥K[x])
              f_1 :
            ↥K[x])),
    Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
          hy_1 :
        ↥K[x])
⊢ Eq.{u_2 + 1} (α := S)
    ((↑(Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
            hy_1) :
        S) :
      S)
    ((↑((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f) :
        S) :
      S)

Tactic:
aeval_algebraMap_apply S (⟨x, _⟩ : K[x]) _

Premises used: Subsemiring.mk', Subsemiring.closure, Set.Mem, Subtype.mk, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hST : Function.Injective (α := ↥K[x]) (β := S) (⇑(algebraMap (↥K[x]) S) : (a : ↥K[x]) → S)
hx' : IsIntegral K (A := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
f : K[X]
hy_1 : Membership.mem (α := S) (γ := Subalgebra K S) K[x] ((aeval x : (a : K[X]) → S) f : S)
hy : Membership.mem (α := S) (γ := Subalgebra K S) (AlgHom.range (aeval x)) ((aeval x : (a : K[X]) → S) f : S)
h :
  Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x]) ⊤
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
        hy_1 :
      ↥K[x])
this :
  ∀
    (hy :
      ∃ (f_1 : K[X]),
        Eq.{u_2 + 1} (α := ↥K[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1)
              ((aeval x : (a : K[X]) → S) f) hy_1 :
            ↥K[x])
          ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                (a : K[X]) → ↥K[x])
              f_1 :
            ↥K[x])),
    Membership.mem.{u_2, u_2} (α := ↥K[x]) (γ := Submodule K ↥K[x])
      (Submodule.span K
        (Set.range
          fun
            (i :
              Fin
                (natDegree
                  (minpoly K (B := S)
                    ((algebraMap (↥K[x]) S : (a : ↥K[x]) → S)
                        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
                      S)))) ↦
          HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
            (↑i : ℕ)))
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
          hy_1 :
        ↥K[x])
⊢ Eq.{u_2 + 1} (α := S)
    ((↑(Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) ((aeval x : (a : K[X]) → S) f)
            hy_1) :
        S) :
      S)
    ((↑((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯) :
              (a : K[X]) → ↥K[x])
            f) :
        S) :
      S)

Tactic:
exact aeval_algebraMap_apply S (⟨x, _⟩ : K[x]) _

Premises used: Subtype.mk, Polynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
i : Fin (natDegree (minpoly K x))
rw :
  (Basis.mk ⋯ ⋯ : (a : Fin (minpoly K x).natDegree) → ↥K[x]) i =
    HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
      (↑i : ℕ)
rw₁ rw₂ :
  HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
      (↑i : ℕ) =
    HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
      (↑i : ℕ)
⊢ (powerBasisAux hx : (a : Fin (minpoly K x).natDegree) → ↥K[x]) i =
    HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x ⋯)
      (↑i : ℕ)

Tactic:
rw [adjoin.powerBasisAux, Basis.mk_apply]

Premises used: Module.Basis.mk_apply, Algebra.adjoin.powerBasisAux
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hx' : Eq (α := Subalgebra K S) K[x] ⊤
⊢ (ofAdjoinEqTop hx hx').gen = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
K : Type u_1
S : Type u_2
inst : Field K
inst_1 : CommRing S
inst_2 : Algebra K S
x : S
hx : IsIntegral K x
hx' : Eq (α := Subalgebra K S) K[x] ⊤
⊢ (ofAdjoinEqTop hx hx').dim = natDegree (minpoly K x)

Tactic:
rfl

Premises used: WithBot.recBotCoe, Polynomial.natDegree, WithBot.unbotD, rfl
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
⊢ Nontrivial S

Tactic:
nontriviality S
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
h : Nontrivial S
Q : R[X] := HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen
rw :
  Eq.{u_4 + 1} (α := A)
    ((aeval B.gen : (a : R[X]) → A)
        (HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen +
          minpoly R B.gen * (HPow.hPow (α := R[X]) X n /ₘ minpoly R B.gen)) :
      A)
    ((aeval B.gen : (a : R[X]) → A) Q : A)
⊢ B.gen ^ n = (aeval B.gen : (a : R[X]) → A) Q

Tactic:
rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly R B.gen)]

Premises used: Polynomial.aeval_X_pow, PowerBasis.gen, minpoly, HPow.hPow, Polynomial.modByMonic_add_div, Polynomial.X
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
h : Nontrivial S
Q : R[X] := HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen
⊢ Eq.{u_4 + 1} (α := A)
    ((aeval B.gen : (a : R[X]) → A)
        (HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen +
          minpoly R B.gen * (HPow.hPow (α := R[X]) X n /ₘ minpoly R B.gen)) :
      A)
    ((aeval B.gen : (a : R[X]) → A) Q : A)

Tactic:
simp [Q]
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
h : Nontrivial S
Q : R[X] := HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen
⊢ B.gen ^ n = (aeval B.gen : (a : R[X]) → A) Q

Tactic:
have : B.gen ^ n = aeval B.gen Q := by
    rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly R B.gen)]
    simp [Q]
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
h : Nontrivial S
Q : R[X] := HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen : (a : R[X]) → A) Q
pos :
  ∀ (hQ : Q = 0),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (B.gen ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
neg :
  ∀ (hQ : ¬Q = 0),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (B.gen ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
⊢ IsIntegral.{u_3, u_2} R (A := S)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (B.gen ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
by_cases hQ : Q = 0
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
h : Nontrivial S
Q : R[X] := HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen : (a : R[X]) → A) Q
hQ : Q = 0
⊢ IsIntegral.{u_3, u_2} R (A := S)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (B.gen ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
simp [this, hQ, isIntegral_zero]

Premises used: isIntegral_zero
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
h : Nontrivial S
Q : R[X] := HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen : (a : R[X]) → A) Q
hQ : ¬Q = 0
rw : Q.degree < degree (minpoly R B.gen)
⊢ Q.natDegree < B.dim

Tactic:
rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map,
      natDegree_lt_natDegree_iff hQ]

Premises used: minpoly.monic, Polynomial.natDegree_lt_natDegree_iff, Polynomial.Monic.natDegree_map, PowerBasis.natDegree_minpoly
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
h : Nontrivial S
Q : R[X] := HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen
this_1 : B.gen ^ n = (aeval B.gen : (a : R[X]) → A) Q
hQ : ¬Q = 0
this : Nontrivial R := ⋯
⊢ Q.degree < degree (minpoly R B.gen)

Tactic:
degree_modByMonic_lt _ (minpoly.monic hB)

Premises used: minpoly.monic, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
h : Nontrivial S
Q : R[X] := HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen
this_1 : B.gen ^ n = (aeval B.gen : (a : R[X]) → A) Q
hQ : ¬Q = 0
this : Nontrivial R := ⋯
⊢ Q.degree < degree (minpoly R B.gen)

Tactic:
exact degree_modByMonic_lt _ (minpoly.monic hB)

Premises used: minpoly.monic, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.RingTheory.Adjoin.PowerBasis
Goal:
S : Type u_2
inst : CommRing S
R : Type u_3
inst_1 : CommRing R
inst_2 : Algebra R S
A : Type u_4
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : PowerBasis S A
hB : IsIntegral R B.gen
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
i : Fin B.dim
h : Nontrivial S
Q : R[X] := HPow.hPow (α := R[X]) X n %ₘ minpoly R B.gen
this : B.gen ^ n = (aeval B.gen : (a : R[X]) → A) Q
hQ : ¬Q = 0
⊢ Q.natDegree < B.dim

Tactic:
have hlt : Q.natDegree < B.dim := by
    rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map,
      natDegree_lt_natDegree_iff hQ]
    letI : Nontrivial R := Nontrivial.of_polynomial_ne hQ
    exact degree_modByMonic_lt _ (minpoly.monic hB)