awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 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)))
have 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)
Tactic: refine (hy _).mul ((hx _).mul ?_)
-- 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)
              (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)
have 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)
Tactic: simp only [coe_basis, ← pow_add]
-- 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 : 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
⊢ ∀ (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)
have 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)
Tactic: revert hx
Cleared hypotheses: hx
-- 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 : 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)
have refine_1 : (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))
  0
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 => ?_
-- 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 : 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)
⊢ ∀
    (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)
have 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)
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 => ?_
-- 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 : 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
⊢ 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)
have refine_1 : IsIntegral.{u_3, u_2} R (A := S) (if (⟨0, sorry⟩ : Fin B.dim) = i then 1 else 0)
Tactic: rw [pow_zero, ← pow_zero B.gen, ← Fin.val_mk B.dim_pos, ← B.basis_eq_pow,
      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
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
⊢ IsIntegral.{u_3, u_2} R (A := S) (if (⟨0, ⋯⟩ : Fin B.dim) = i then 1 else 0)
have pos : (⟨0, sorry⟩ : Fin B.dim) = i → IsIntegral.{u_3, u_2} R (A := S) 1
Tactic: split_ifs
-- 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 : 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
⊢ IsIntegral.{u_3, u_2} R (A := S) (if (⟨0, ⋯⟩ : Fin B.dim) = i then 1 else 0)
have neg : ¬(⟨0, sorry⟩ : Fin B.dim) = i → IsIntegral.{u_3, u_2} R (A := S) 0
Tactic: split_ifs
-- 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 : 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 + 1)) : Fin B.dim →₀ S) : (a : Fin B.dim) → S) i : S)
have 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)
Tactic: rw [pow_succ]
-- 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
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 R (B.basis.toMatrix (⇑B'.basis : (a : Fin B'.dim) → S) i j)
have 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)
Tactic: rw [B.basis.toMatrix_apply, B'.coe_basis]
-- 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
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)
have 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)
Tactic: refine repr_pow_isIntegral hB (fun i => ?_) hmin _ _
-- 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
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)
    ((((B.basis.repr : (a : S) → Fin B.dim →₀ K) B'.gen : Fin B.dim →₀ K) : (a : Fin B.dim) → K) i : K)
have 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)
Tactic: rw [← h, aeval_eq_sum_range, map_sum, Finset.sum_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
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)
have 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)
Tactic: refine IsIntegral.sum _ fun n _ => ?_
-- 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
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.{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)
have 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)
Tactic: rw [Algebra.smul_def, IsScalarTower.algebraMap_apply R K S, ← Algebra.smul_def, map_smul,
    algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Singleton (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
x : ↥A[b]
⊢ Membership.mem (α := C) (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)]
    (((↑(AlgHom.comp (AlgHom.restrictScalars A (ofId B C)) (Subalgebra.val A[b])) : ↥A[b] →+* C) : (a : ↥A[b]) → C) x :
      C)
have f : ∀ (p : A[X]),
  Membership.mem (α := C) (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)]
    (((↑(AlgHom.comp (AlgHom.restrictScalars A (ofId B C)) (Subalgebra.val A[b])) : ↥A[b] →+* C) : (a : ↥A[b]) → C)
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[b] x) ((aeval b : (a : A[X]) → B) p) sorry :
          ↥A[b]) :
      C)
Tactic: induction x using adjoin_singleton_induction with
      | f p => aesop (add norm [adjoin_singleton_eq_range_aeval, aeval_algebraMap_apply])
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Singleton (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
c : ↥A[((algebraMap B C : (a : B) → C) b : C)]
⊢ ∃ (a : ↥A[b]), (adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a = c
have obtain : ∀ (p : A[X]) (hp : ((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p = (↑c : C)),
  ∃ (a : ↥A[b]), (adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a = c
Tactic: obtain ⟨p, hp⟩ := adjoin_eq_exists_aeval A (algebraMap B C b) c
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Singleton (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
inst_7 : FaithfulSMul B C
⊢ RingEquiv.{u_2, u_3} ↥A[b] ↥A[((algebraMap B C : (a : B) → C) b : C)]
have apply : ∀ (y : ↥A[((algebraMap B C : (a : B) → C) b : C)]),
  ∃! a : ↥A[b], (adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a = y
Tactic: apply RingEquiv.ofBijective (RingHom.adjoinAlgebraMap b)
     ((Function.bijective_iff_existsUnique (adjoinAlgebraMap b)).mpr (fun y ↦ ?_))
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Singleton (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
inst_7 : FaithfulSMul B C
p : A[X]
⊢ ∃! a : ↥A[b],
    Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
      ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
        ↥A[((algebraMap B C : (a : B) → C) b : C)])
      (Subtype.mk (p := fun (x : C) ↦ Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
          (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) ⋯ :
        ↥A[((algebraMap B C : (a : B) → C) b : C)])
have h : (fun (a : ↥A[b]) ↦
      Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
        ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
          ↥A[((algebraMap B C : (a : B) → C) b : C)])
        (Subtype.mk (p := fun (x : C) ↦
            Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
            (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) sorry :
          ↥A[((algebraMap B C : (a : B) → C) b : C)]))
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[b] x) ((aeval b : (a : A[X]) → B) p) sorry) ∧
  ∀ (y : ↥A[b]),
    (fun (a : ↥A[b]) ↦
          Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
            ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
              ↥A[((algebraMap B C : (a : B) → C) b : C)])
            (Subtype.mk (p := fun (x : C) ↦
                Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
                (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) sorry :
              ↥A[((algebraMap B C : (a : B) → C) b : C)]))
        y →
      y = Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[b] x) ((aeval b : (a : A[X]) → B) p) sorry
Tactic: use ⟨p.aeval b, by simp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Singleton (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommSemiring A
inst_1 : CommSemiring B
inst_2 : CommSemiring C
inst_3 : Algebra A B
inst_4 : Algebra B C
inst_5 : Algebra A C
inst_6 : IsScalarTower A B C
b : B
inst_7 : FaithfulSMul B C
y : ↥A[((algebraMap B C : (a : B) → C) b : C)]
⊢ ∃! a : ↥A[b], (adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a = y
have f : ∀ (p : A[X]),
  ∃! a : ↥A[b],
    Eq.{u_3 + 1} (α := ↥A[((algebraMap B C : (a : B) → C) b : C)])
      ((adjoinAlgebraMap b : (a : ↥A[b]) → ↥A[(algebraMap B C : (a : B) → C) b]) a :
        ↥A[((algebraMap B C : (a : B) → C) b : C)])
      (Subtype.mk (p := fun (x : C) ↦ Membership.mem (γ := Subalgebra A C) A[((algebraMap B C : (a : B) → C) b : C)] x)
          (((aeval ((algebraMap B C : (a : B) → C) b) : A[X] →ₐ[A] C) : (a : A[X]) → C) p) sorry :
        ↥A[((algebraMap B C : (a : B) → C) b : C)])
Tactic: induction y using Algebra.adjoin_singleton_induction with | f p =>
  use ⟨p.aeval b, by simp⟩
  aesop (add norm [Polynomial.aeval_algebraMap_apply, Subtype.ext_iff])
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : CommSemiring C
inst_1 : CommSemiring D
inst_2 : CommSemiring E
inst_3 : Algebra C D
inst_4 : Algebra C E
inst_5 : Algebra D E
inst_6 : IsScalarTower C D E
S : Set E
this :
  Eq (α := Set E) (Set.range.{u_3, u_2 + 1} (ι := D) (⇑(algebraMap D E) : (a : D) → E))
    (Set.range (ι := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
      (⇑(algebraMap (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) E) :
        (a : ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) → E))
⊢ Eq (α := Subalgebra C E) (Subalgebra.restrictScalars C (adjoin D S))
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S))
have h : ∀ (x : E),
  Membership.mem (γ := Subalgebra C E) (Subalgebra.restrictScalars C (adjoin D S)) x ↔
    Membership.mem (γ := Subalgebra C E)
      (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤))
        (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S))
      x
Tactic: ext x