awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hlt : Q.natDegree < B.dim
neg :
  IsIntegral.{u_3, u_2} R (A := S)
    (((B.basis.repr : (a : A) → Fin B.dim →₀ S) (∑ i ∈ Finset.range B.dim, Q.coeff i • B.gen ^ i) : (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:
rw [this, aeval_eq_sum_range' hlt]

Premises used: Polynomial.aeval_eq_sum_range'
-- 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
hlt : Q.natDegree < B.dim
neg :
  IsIntegral.{u_3, u_2} R (A := S)
    (∑ k ∈ Finset.range B.dim,
      (((B.basis.repr : (a : A) → Fin B.dim →₀ S) (Q.coeff k • B.gen ^ k) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i)
⊢ IsIntegral.{u_3, u_2} R (A := S)
    (((B.basis.repr : (a : A) → Fin B.dim →₀ S) (∑ i ∈ Finset.range B.dim, Q.coeff i • B.gen ^ i) : (a : Fin B.dim) → S)
        i :
      S)

Tactic:
simp only [map_sum, Finset.sum_apply']

Premises used: Finset.sum_apply', map_sum
-- 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
hlt : Q.natDegree < B.dim
⊢ IsIntegral.{u_3, u_2} R (A := S)
    (∑ k ∈ Finset.range B.dim,
      (((B.basis.repr : (a : A) → Fin B.dim →₀ S) (Q.coeff k • B.gen ^ k) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i)

Tactic:
IsIntegral.sum _ fun j hj => ?_

Premises used: IsIntegral.sum
-- 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
hlt : Q.natDegree < B.dim
neg :
  ∀ (j : ℕ) (hj : j ∈ Finset.range B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (Q.coeff j • B.gen ^ j) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i :
        S)
⊢ IsIntegral.{u_3, u_2} R (A := S)
    (∑ k ∈ Finset.range B.dim,
      (((B.basis.repr : (a : A) → Fin B.dim →₀ S) (Q.coeff k • B.gen ^ k) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i)

Tactic:
refine IsIntegral.sum _ fun j hj => ?_

Premises used: IsIntegral.sum
-- 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
hlt : Q.natDegree < B.dim
j : ℕ
hj : j ∈ Finset.range B.dim
⊢ j < B.dim

Tactic:
replace hj := Finset.mem_range.1 hj
-- 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
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
neg :
  IsIntegral R (A := S)
    ((HSMul.hSMul (α := S) (β := Fin B.dim →₀ S)
            ((algebraMap R S : (a : R) → S) (Q.coeff (↑(⟨j, hj⟩ : Fin B.dim) : ℕ)) : S)
            ((B.basis.repr : (a : A) → Fin B.dim →₀ S) ((B.basis : (a : Fin B.dim) → A) (⟨j, hj⟩ : Fin B.dim)) :
              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) (Q.coeff j • B.gen ^ j) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
rw [← Fin.val_mk hj, ← B.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply R S A, ←
    Algebra.smul_def, map_smul]

Premises used: Fin.val_mk, PowerBasis.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply, map_smul
-- 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
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
neg : IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) (if (⟨j, hj⟩ : Fin B.dim) = i then 1 else 0))
⊢ IsIntegral R (A := S)
    ((HSMul.hSMul (α := S) (β := Fin B.dim →₀ S)
            ((algebraMap R S : (a : R) → S) (Q.coeff (↑(⟨j, hj⟩ : Fin B.dim) : ℕ)) : S)
            ((B.basis.repr : (a : A) → Fin B.dim →₀ S) ((B.basis : (a : Fin B.dim) → A) (⟨j, hj⟩ : Fin B.dim)) :
              Fin B.dim →₀ S) :
          (a : Fin B.dim) → S)
        i :
      S)

Tactic:
simp only [algebraMap_smul, Finsupp.coe_smul, Pi.smul_apply, B.basis.repr_self_apply]

Premises used: Module.Basis.repr_self_apply, algebraMap_smul, PowerBasis.basis, Finsupp.coe_smul, Pi.smul_apply
-- 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
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
pos :
  ∀ (hij : (⟨j, hj⟩ : Fin B.dim) = i),
    IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) (if (⟨j, hj⟩ : Fin B.dim) = i then 1 else 0))
neg :
  ∀ (hij : ¬(⟨j, hj⟩ : Fin B.dim) = i),
    IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) (if (⟨j, hj⟩ : Fin B.dim) = i then 1 else 0))
⊢ IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) (if (⟨j, hj⟩ : Fin B.dim) = i then 1 else 0))

Tactic:
by_cases hij : (⟨j, hj⟩ : Fin _) = i

Premises used: Fin.mk
-- 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
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : (⟨j, hj⟩ : Fin B.dim) = i
pos : IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) 1)
⊢ IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) (if (⟨j, hj⟩ : Fin B.dim) = i then 1 else 0))

Tactic:
simp only [hij, if_true]

Premises used: if_true
-- 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
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : (⟨j, hj⟩ : Fin B.dim) = i
pos : IsIntegral.{u_3, u_2} R (A := S) ((algebraMap R S : (a : R) → S) (Q.coeff j) : S)
⊢ IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) 1)

Tactic:
rw [Algebra.smul_def, mul_one]

Premises used: Algebra.smul_def, mul_one
-- 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
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : (⟨j, hj⟩ : Fin B.dim) = i
⊢ IsIntegral.{u_3, u_2} R (A := S) ((algebraMap R S : (a : R) → S) (Q.coeff j) : S)

Tactic:
isIntegral_algebraMap

Premises used: isIntegral_algebraMap
-- 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
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : (⟨j, hj⟩ : Fin B.dim) = i
⊢ IsIntegral.{u_3, u_2} R (A := S) ((algebraMap R S : (a : R) → S) (Q.coeff j) : S)

Tactic:
exact isIntegral_algebraMap

Premises used: isIntegral_algebraMap
-- 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
hlt : Q.natDegree < B.dim
j : ℕ
hj : j < B.dim
hij : ¬(⟨j, hj⟩ : Fin B.dim) = i
⊢ IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) (if (⟨j, hj⟩ : Fin B.dim) = i then 1 else 0))

Tactic:
simp [hij, 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
x y : A
hx :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hy :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
i : Fin B.dim
rw :
  IsIntegral.{u_3, u_2} R (A := S)
    (∑ k ∈ SProd.sprod (α := Finset (Fin B.dim)) (β := Finset (Fin B.dim)) Finset.univ Finset.univ,
      (((B.basis.repr : (a : A) → Fin B.dim →₀ S)
              (HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                  ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) k.1 : S)
                  ((B.basis : (a : Fin B.dim) → A) k.1 : A) *
                HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                  ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) k.2 : S)
                  ((B.basis : (a : Fin B.dim) → A) k.2 : A)) :
            Fin B.dim →₀ S) :
          (a : Fin B.dim) → S)
        i)
⊢ IsIntegral.{u_3, u_2} R (A := S)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x * y) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
rw [← B.basis.sum_repr x, ← B.basis.sum_repr y, Finset.sum_mul_sum, ← Finset.sum_product',
    map_sum, Finset.sum_apply']

Premises used: Finset.sum_apply', PowerBasis.basis, map_sum, Finset.sum_product', Module.Basis.sum_repr, Finset.sum_mul_sum
-- 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
x y : A
hx :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hy :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
i : Fin B.dim
⊢ IsIntegral.{u_3, u_2} R (A := S)
    (∑ k ∈ SProd.sprod (α := Finset (Fin B.dim)) (β := Finset (Fin B.dim)) Finset.univ Finset.univ,
      (((B.basis.repr : (a : A) → Fin B.dim →₀ S)
              (HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                  ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) k.1 : S)
                  ((B.basis : (a : Fin B.dim) → A) k.1 : A) *
                HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                  ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) k.2 : S)
                  ((B.basis : (a : Fin B.dim) → A) k.2 : A)) :
            Fin B.dim →₀ S) :
          (a : Fin B.dim) → S)
        i)

Tactic:
IsIntegral.sum _ fun I _ => ?_

Premises used: IsIntegral.sum
-- 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
x y : A
hx :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hy :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
i : Fin B.dim
refine :
  ∀ I ∈ SProd.sprod (α := Finset (Fin B.dim)) (β := Finset (Fin B.dim)) Finset.univ Finset.univ,
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S)
                (HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.1 : S)
                    ((B.basis : (a : Fin B.dim) → A) I.1 : A) *
                  HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.2 : S)
                    ((B.basis : (a : Fin B.dim) → A) I.2 : A)) :
              Fin B.dim →₀ S) :
            (a : Fin B.dim) → S)
          i :
        S)
⊢ IsIntegral.{u_3, u_2} R (A := S)
    (∑ k ∈ SProd.sprod (α := Finset (Fin B.dim)) (β := Finset (Fin B.dim)) Finset.univ Finset.univ,
      (((B.basis.repr : (a : A) → Fin B.dim →₀ S)
              (HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                  ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) k.1 : S)
                  ((B.basis : (a : Fin B.dim) → A) k.1 : A) *
                HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                  ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) k.2 : S)
                  ((B.basis : (a : Fin B.dim) → A) k.2 : A)) :
            Fin B.dim →₀ S) :
          (a : Fin B.dim) → S)
        i)

Tactic:
refine IsIntegral.sum _ fun I _ => ?_

Premises used: IsIntegral.sum
-- 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
x y : A
hx :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hy :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
i : Fin B.dim
I : Fin B.dim × Fin B.dim
h : I ∈ SProd.sprod (α := Finset (Fin B.dim)) (β := Finset (Fin B.dim)) Finset.univ Finset.univ
simp :
  IsIntegral R
    (HMul.hMul (α := S) ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.2 : S)
      (HMul.hMul (α := S) (β := S)
        ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.1 : S)
        ((((B.basis.repr : (a : A) → Fin B.dim →₀ S)
                  (HMul.hMul (α := A) (β := A) ((B.basis : (a : Fin B.dim) → A) I.1 : A)
                    ((B.basis : (a : Fin B.dim) → A) I.2 : A)) :
                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)
              (HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                  ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.1 : S)
                  ((B.basis : (a : Fin B.dim) → A) I.1 : A) *
                HSMul.hSMul.{u_2, u_4, u_4} (α := S) (β := A)
                  ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.2 : S)
                  ((B.basis : (a : Fin B.dim) → A) I.2 : A)) :
            Fin B.dim →₀ S) :
          (a : Fin B.dim) → S)
        i :
      S)

Tactic:
simp only [Algebra.smul_mul_assoc, Algebra.mul_smul_comm, map_smulₛₗ, RingHom.id_apply,
    Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul]

Premises used: Algebra.mul_smul_comm, RingHom.id_apply, MulActionSemiHomClass.map_smulₛₗ, Finsupp.coe_smul, Algebra.smul_mul_assoc, smul_eq_mul, Pi.smul_apply
-- 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
x y : A
hx :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hy :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
i : Fin B.dim
I : Fin B.dim × Fin B.dim
h : I ∈ SProd.sprod (α := Finset (Fin B.dim)) (β := Finset (Fin B.dim)) Finset.univ Finset.univ
⊢ IsIntegral R
    (HMul.hMul (α := S) ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.2 : S)
      (HMul.hMul (α := S) (β := S)
        ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.1 : S)
        ((((B.basis.repr : (a : A) → Fin B.dim →₀ S)
                  (HMul.hMul (α := A) (β := A) ((B.basis : (a : Fin B.dim) → A) I.1 : A)
                    ((B.basis : (a : Fin B.dim) → A) I.2 : A)) :
                Fin B.dim →₀ S) :
              (a : Fin B.dim) → S)
            i :
          S)))

Tactic:
(hy _).mul ((hx _).mul ?_)

Premises used: IsIntegral.mul
-- 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
x y : A
hx :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hy :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
i : Fin B.dim
I : Fin B.dim × Fin B.dim
h : I ∈ SProd.sprod (α := Finset (Fin B.dim)) (β := Finset (Fin B.dim)) Finset.univ Finset.univ
refine :
  IsIntegral.{u_3, u_2} R (A := S)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S)
              (HMul.hMul (α := A) (β := A) ((B.basis : (a : Fin B.dim) → A) I.1 : A)
                ((B.basis : (a : Fin B.dim) → A) I.2 : A)) :
            Fin B.dim →₀ S) :
          (a : Fin B.dim) → S)
        i :
      S)
⊢ IsIntegral R
    (HMul.hMul (α := S) ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) y : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.2 : S)
      (HMul.hMul (α := S) (β := S)
        ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) x : Fin B.dim →₀ S) : (a : Fin B.dim) → S) I.1 : S)
        ((((B.basis.repr : (a : A) → Fin B.dim →₀ S)
                  (HMul.hMul (α := A) (β := A) ((B.basis : (a : Fin B.dim) → A) I.1 : A)
                    ((B.basis : (a : Fin B.dim) → A) I.2 : A)) :
                Fin B.dim →₀ S) :
              (a : Fin B.dim) → S)
            i :
          S)))

Tactic:
refine (hy _).mul ((hx _).mul ?_)

Premises used: IsIntegral.mul