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
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.{u_3, u_2} R (A := S)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (B.gen ^ ((↑I.1 : ℕ) + (↑I.2 : ℕ))) : 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)
              (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:
simp only [coe_basis, ← pow_add]

Premises used: PowerBasis.coe_basis, pow_add
-- 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.{u_3, u_2} R (A := S)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (B.gen ^ ((↑I.1 : ℕ) + (↑I.2 : ℕ))) : Fin B.dim →₀ S) :
          (a : Fin B.dim) → S)
        i :
      S)

Tactic:
repr_gen_pow_isIntegral hB hmin _ _

Premises used: PowerBasis.repr_gen_pow_isIntegral
-- 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.{u_3, u_2} R (A := S)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (B.gen ^ ((↑I.1 : ℕ) + (↑I.2 : ℕ))) : Fin B.dim →₀ S) :
          (a : Fin B.dim) → S)
        i :
      S)

Tactic:
exact repr_gen_pow_isIntegral hB hmin _ _

Premises used: PowerBasis.repr_gen_pow_isIntegral
-- 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 : 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)
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
h : Nontrivial A
revert :
  ∀
    (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))
    (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
⊢ ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
revert hx
-- 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 : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
h : Nontrivial 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))
    (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
Nat.case_strong_induction_on
    -- Porting note: had to hint what to induct on
    (p := fun n ↦ _ → ∀ (i : Fin B.dim), IsIntegral R (B.basis.repr (x ^ n) i))
    n ?_ fun n hn => ?_

Premises used: Nat.case_strong_induction_on
-- 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 : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
h : Nontrivial A
refine_1 :
  (∀ (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)) →
    ∀ (i : Fin B.dim),
      IsIntegral.{u_3, u_2} R (A := S)
        ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (HPow.hPow (β := ℕ) x 0) : Fin B.dim →₀ S) : (a : Fin B.dim) → S)
            i :
          S)
refine_2 :
  ∀ (n : ℕ)
    (hn :
      ∀ m ≤ n,
        (fun (n : ℕ) ↦
            (∀ (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)) →
              ∀ (i : Fin B.dim),
                IsIntegral.{u_3, u_2} R (A := S)
                  ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S))
          m),
    (fun (n : ℕ) ↦
        (∀ (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)) →
          ∀ (i : Fin B.dim),
            IsIntegral.{u_3, u_2} R (A := S)
              ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S))
      (n + 1)
⊢ ∀
    (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))
    (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
refine Nat.case_strong_induction_on
    -- Porting note: had to hint what to induct on
    (p := fun n ↦ _ → ∀ (i : Fin B.dim), IsIntegral R (B.basis.repr (x ^ n) i))
    n ?_ fun n hn => ?_

Premises used: Nat.case_strong_induction_on
-- 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 : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
h : Nontrivial A
h_1 :
  ∀ (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)
i : Fin B.dim
refine_1 : IsIntegral.{u_3, u_2} R (A := S) (if (⟨0, ⋯⟩ : Fin B.dim) = i then 1 else 0)
⊢ IsIntegral.{u_3, u_2} R (A := S)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (HPow.hPow (β := ℕ) x 0) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i :
      S)

Tactic:
rw [pow_zero, ← pow_zero B.gen, ← Fin.val_mk B.dim_pos, ← B.basis_eq_pow,
      B.basis.repr_self_apply]

Premises used: Module.Basis.repr_self_apply, PowerBasis.gen, Fin.val_mk, PowerBasis.basis, pow_zero, PowerBasis.basis_eq_pow, PowerBasis.dim_pos
-- 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 : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
h : Nontrivial A
h_1 :
  ∀ (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)
i : Fin B.dim
pos : (⟨0, ⋯⟩ : Fin B.dim) = i → IsIntegral.{u_3, u_2} R (A := S) 1
neg : ¬(⟨0, ⋯⟩ : Fin B.dim) = i → IsIntegral.{u_3, u_2} R (A := S) 0
⊢ IsIntegral.{u_3, u_2} R (A := S) (if (⟨0, ⋯⟩ : Fin B.dim) = i then 1 else 0)

Tactic:
split_ifs
-- 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 : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
h : Nontrivial A
h_1 :
  ∀ (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)
i : Fin B.dim
h_2 : (⟨0, ⋯⟩ : Fin B.dim) = i
⊢ IsIntegral.{u_3, u_2} R (A := S) 1

Tactic:
isIntegral_one

Premises used: isIntegral_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
x : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
h : Nontrivial A
h_1 :
  ∀ (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)
i : Fin B.dim
h_2 : (⟨0, ⋯⟩ : Fin B.dim) = i
⊢ IsIntegral.{u_3, u_2} R (A := S) 1

Tactic:
exact isIntegral_one

Premises used: isIntegral_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
x : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
h : Nontrivial A
h_1 :
  ∀ (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)
i : Fin B.dim
h_2 : ¬(⟨0, ⋯⟩ : Fin B.dim) = i
⊢ IsIntegral.{u_3, u_2} R (A := S) 0

Tactic:
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 : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n : ℕ
h : Nontrivial A
h_1 :
  ∀ (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)
i : Fin B.dim
h_2 : ¬(⟨0, ⋯⟩ : Fin B.dim) = i
⊢ IsIntegral.{u_3, u_2} R (A := S) 0

Tactic:
exact 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 : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n_1 : ℕ
h : Nontrivial A
n : ℕ
hn :
  ∀ m ≤ n,
    (fun (n : ℕ) ↦
        (∀ (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)) →
          ∀ (i : Fin B.dim),
            IsIntegral.{u_3, u_2} R (A := S)
              ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S))
      m
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)
refine_2 :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n * x) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
⊢ ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ (n + 1)) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- 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 : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n_1 : ℕ
h : Nontrivial A
n : ℕ
hn :
  ∀ m ≤ n,
    (fun (n : ℕ) ↦
        (∀ (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)) →
          ∀ (i : Fin B.dim),
            IsIntegral.{u_3, u_2} R (A := S)
              ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S))
      m
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)
⊢ ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n * x) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
repr_mul_isIntegral hB (fun _ => hn _ le_rfl (fun _ => hx _) _) hx hmin

Premises used: le_rfl, PowerBasis.repr_mul_isIntegral
-- 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 : A
hmin : Eq (α := S[X]) (minpoly S B.gen) (Polynomial.map (algebraMap R S) (minpoly R B.gen))
n_1 : ℕ
h : Nontrivial A
n : ℕ
hn :
  ∀ m ≤ n,
    (fun (n : ℕ) ↦
        (∀ (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)) →
          ∀ (i : Fin B.dim),
            IsIntegral.{u_3, u_2} R (A := S)
              ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S))
      m
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)
⊢ ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_2} R (A := S)
      ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x ^ n * x) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)

Tactic:
exact repr_mul_isIntegral hB (fun _ => hn _ le_rfl (fun _ => hx _) _) hx hmin

Premises used: le_rfl, PowerBasis.repr_mul_isIntegral
-- 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
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen : (a : R[X]) → S) P = B'.gen
hB : IsIntegral R B.gen
hmin : Eq (α := K[X]) (minpoly K B.gen) (Polynomial.map (algebraMap R K) (minpoly R B.gen))
i : Fin B.dim
j : Fin B'.dim
rw :
  IsIntegral.{u_3, u_1} R (A := K)
    (((B.basis.repr : (a : S) → Fin B.dim →₀ K) ((fun (i : Fin B'.dim) ↦ B'.gen ^ (↑i : ℕ)) j) : (a : Fin B.dim) → K)
        i :
      K)
⊢ IsIntegral R (B.basis.toMatrix (⇑B'.basis : (a : Fin B'.dim) → S) i j)

Tactic:
rw [B.basis.toMatrix_apply, B'.coe_basis]

Premises used: PowerBasis.coe_basis, PowerBasis.basis, Module.Basis.toMatrix_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
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen : (a : R[X]) → S) P = B'.gen
hB : IsIntegral R B.gen
hmin : Eq (α := K[X]) (minpoly K B.gen) (Polynomial.map (algebraMap R K) (minpoly R B.gen))
i : Fin B.dim
j : Fin B'.dim
⊢ IsIntegral.{u_3, u_1} R (A := K)
    (((B.basis.repr : (a : S) → Fin B.dim →₀ K) ((fun (i : Fin B'.dim) ↦ B'.gen ^ (↑i : ℕ)) j) : (a : Fin B.dim) → K)
        i :
      K)

Tactic:
repr_pow_isIntegral hB (fun i => ?_) hmin _ _

Premises used: PowerBasis.repr_pow_isIntegral
-- 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
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen : (a : R[X]) → S) P = B'.gen
hB : IsIntegral R B.gen
hmin : Eq (α := K[X]) (minpoly K B.gen) (Polynomial.map (algebraMap R K) (minpoly R B.gen))
i : Fin B.dim
j : Fin B'.dim
refine :
  ∀ (i : Fin B.dim),
    IsIntegral.{u_3, u_1} R (A := K)
      ((((B.basis.repr : (a : S) → Fin B.dim →₀ K) B'.gen : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
⊢ IsIntegral.{u_3, u_1} R (A := K)
    (((B.basis.repr : (a : S) → Fin B.dim →₀ K) ((fun (i : Fin B'.dim) ↦ B'.gen ^ (↑i : ℕ)) j) : (a : Fin B.dim) → K)
        i :
      K)

Tactic:
refine repr_pow_isIntegral hB (fun i => ?_) hmin _ _

Premises used: PowerBasis.repr_pow_isIntegral
-- 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
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen : (a : R[X]) → S) P = B'.gen
hB : IsIntegral R B.gen
hmin : Eq (α := K[X]) (minpoly K B.gen) (Polynomial.map (algebraMap R K) (minpoly R B.gen))
i_1 : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
rw :
  IsIntegral.{u_3, u_1} R (A := K)
    (∑ k ∈ Finset.range (P.natDegree + 1),
      (((B.basis.repr : (a : S) → Fin B.dim →₀ K) (P.coeff k • B.gen ^ k) : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i)
⊢ IsIntegral.{u_3, u_1} R (A := K)
    ((((B.basis.repr : (a : S) → Fin B.dim →₀ K) B'.gen : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)

Tactic:
rw [← h, aeval_eq_sum_range, map_sum, Finset.sum_apply']

Premises used: Finset.sum_apply', map_sum, Polynomial.aeval_eq_sum_range
-- 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
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen : (a : R[X]) → S) P = B'.gen
hB : IsIntegral R B.gen
hmin : Eq (α := K[X]) (minpoly K B.gen) (Polynomial.map (algebraMap R K) (minpoly R B.gen))
i_1 : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
⊢ IsIntegral.{u_3, u_1} R (A := K)
    (∑ k ∈ Finset.range (P.natDegree + 1),
      (((B.basis.repr : (a : S) → Fin B.dim →₀ K) (P.coeff k • B.gen ^ k) : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i)

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

Premises used: IsIntegral.sum
-- 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
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen : (a : R[X]) → S) P = B'.gen
hB : IsIntegral R B.gen
hmin : Eq (α := K[X]) (minpoly K B.gen) (Polynomial.map (algebraMap R K) (minpoly R B.gen))
i_1 : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
refine :
  ∀ n ∈ Finset.range (P.natDegree + 1),
    IsIntegral.{u_3, u_1} R (A := K)
      ((((B.basis.repr : (a : S) → Fin B.dim →₀ K) (P.coeff n • B.gen ^ n) : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i :
        K)
⊢ IsIntegral.{u_3, u_1} R (A := K)
    (∑ k ∈ Finset.range (P.natDegree + 1),
      (((B.basis.repr : (a : S) → Fin B.dim →₀ K) (P.coeff k • B.gen ^ k) : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i)

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

Premises used: IsIntegral.sum
-- 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
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen : (a : R[X]) → S) P = B'.gen
hB : IsIntegral R B.gen
hmin : Eq (α := K[X]) (minpoly K B.gen) (Polynomial.map (algebraMap R K) (minpoly R B.gen))
i_1 : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
h_1 : n ∈ Finset.range (P.natDegree + 1)
rw :
  IsIntegral R (A := K)
    ((HSMul.hSMul (β := Fin B.dim →₀ K) (P.coeff n)
            ((B.basis.repr : (a : S) → Fin B.dim →₀ K) (B.gen ^ n) : Fin B.dim →₀ K) :
          (a : Fin B.dim) → K)
        i :
      K)
⊢ IsIntegral.{u_3, u_1} R (A := K)
    ((((B.basis.repr : (a : S) → Fin B.dim →₀ K) (P.coeff n • B.gen ^ n) : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)

Tactic:
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def, map_smul,
    algebraMap_smul]

Premises used: algebraMap_smul, Algebra.smul_def, IsScalarTower.algebraMap_apply, map_smul
-- 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
R : Type u_3
inst_3 : CommRing R
inst_4 : Algebra R S
inst_5 : Algebra R K
inst_6 : IsScalarTower R K S
B B' : PowerBasis K S
P : R[X]
h : (aeval B.gen : (a : R[X]) → S) P = B'.gen
hB : IsIntegral R B.gen
hmin : Eq (α := K[X]) (minpoly K B.gen) (Polynomial.map (algebraMap R K) (minpoly R B.gen))
i_1 : Fin B.dim
j : Fin B'.dim
i : Fin B.dim
n : ℕ
h_1 : n ∈ Finset.range (P.natDegree + 1)
⊢ IsIntegral R (A := K)
    ((HSMul.hSMul (β := Fin B.dim →₀ K) (P.coeff n)
            ((B.basis.repr : (a : S) → Fin B.dim →₀ K) (B.gen ^ n) : Fin B.dim →₀ K) :
          (a : Fin B.dim) → K)
        i :
      K)

Tactic:
(repr_gen_pow_isIntegral hB hmin _ _).smul _

Premises used: PowerBasis.repr_gen_pow_isIntegral, IsIntegral.smul