awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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))
⊢ (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 : ℕ)
have rw : (Basis.mk sorry sorry : (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 sorry) (↑i : ℕ)
Tactic: rw [adjoin.powerBasisAux, Basis.mk_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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 : ℕ)
⊢ (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 : ℕ)
have rw₁ : HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x sorry) (↑i : ℕ) =
  HPow.hPow (α := ↥K[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra K S) K[x] x_1) x sorry) (↑i : ℕ)
Tactic: rw [adjoin.powerBasisAux, Basis.mk_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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
⊢ 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)
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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
have 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)
Tactic: rw [← @aeval_X_pow R _ _ _ _ B.gen, ← modByMonic_add_div (X ^ n) (minpoly R B.gen)]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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
⊢ 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)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hQ : Q = 0
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hQ : Q = 0
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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
have rw : Q.degree < degree (minpoly R B.gen)
Tactic: rw [← B.natDegree_minpoly, hmin, (minpoly.monic hB).natDegree_map,
      natDegree_lt_natDegree_iff hQ]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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)
have hlt : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (B.gen ^ n) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
have 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)
Tactic: rw [this, aeval_eq_sum_range' hlt]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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)
    (((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)
have 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)
Tactic: simp only [map_sum, Finset.sum_apply']
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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)
have 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)
Tactic: refine IsIntegral.sum _ fun j hj => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (hypothesis)
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
⊢ 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)
have hj₁ : j < B.dim
Tactic: replace hj := Finset.mem_range.1 hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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
⊢ 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)
have 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)
Tactic: rw [← Fin.val_mk hj, ← B.basis_eq_pow, Algebra.smul_def, IsScalarTower.algebraMap_apply R S A, ←
    Algebra.smul_def, map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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
⊢ 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)
have neg : IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) (if (⟨j, hj⟩ : Fin B.dim) = i then 1 else 0))
Tactic: simp only [algebraMap_smul, Finsupp.coe_smul, Pi.smul_apply, B.basis.repr_self_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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
⊢ IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) (if (⟨j, hj⟩ : Fin B.dim) = i then 1 else 0))
have 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))
Tactic: by_cases hij : (⟨j, hj⟩ : Fin _) = i
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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))
⊢ IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) (if (⟨j, hj⟩ : Fin B.dim) = i then 1 else 0))
have 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))
Tactic: by_cases hij : (⟨j, hj⟩ : Fin _) = i
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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))
have pos : IsIntegral R (HSMul.hSMul (β := S) (Q.coeff j) 1)
Tactic: simp only [hij, if_true]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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) 1)
have pos : IsIntegral.{u_3, u_2} R (A := S) ((algebraMap R S : (a : R) → S) (Q.coeff j) : S)
Tactic: rw [Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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)
    ((((B.basis.repr : (a : A) → Fin B.dim →₀ S) (x * y) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
have 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)
Tactic: rw [← B.basis.sum_repr x, ← B.basis.sum_repr y, Finset.sum_mul_sum, ← Finset.sum_product',
    map_sum, Finset.sum_apply']
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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)
have 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)
Tactic: refine IsIntegral.sum _ fun I _ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.PowerBasis (goal)
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)
              (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)
have 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)))
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]