awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
⊢ Module.Finite R V

Tactic:
exact Module.Finite.trans S V

Premises used: Module.Finite.trans
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
⊢ Etale R V

Tactic:
Algebra.Etale.comp R S V

Premises used: Algebra.Etale.comp
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
⊢ Etale R V

Tactic:
exact Algebra.Etale.comp R S V

Premises used: Algebra.Etale.comp
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
⊢ IsFiniteSplit V (V ⊗[R] S)

Tactic:
.of_algEquiv e.symm

Premises used: AlgEquiv.symm, Algebra.IsFiniteSplit.of_algEquiv
-- Module: Mathlib.RingTheory.TotallySplit
Goal:
n_1 : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_5 : CommRing S] [inst_6 : Algebra R S] [Etale R S] [Module.Finite R S]
    (hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑n_1 : (p : PrimeSpectrum R) → ℕ)),
    ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra R T) (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ :
      Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Etale R S
inst_4 : Module.Finite R S
hn : Eq (α := (p : PrimeSpectrum R) → ℕ) (Module.rankAtStalk S) (↑(n_1 + 1) : (p : PrimeSpectrum R) → ℕ)
h : Nontrivial R
this_1 : Nontrivial S
U : Type u
w : CommRing U
w_1 : Algebra S U
e_1 : S ⊗[R] S ≃ₐ[S] S × U
algInst : Algebra (S × U) U := RingHom.toAlgebra (RingHom.snd S U)
this_2 : IsScalarTower S (S × U) U
this_3 : Etale S U
this_4 : Module.Finite S U
this_5 : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n_1 + 1
this : Eq (α := (p : PrimeSpectrum S) → ℕ) (Module.rankAtStalk U) (↑n_1 : (p : PrimeSpectrum S) → ℕ)
V : Type u
w_2 : CommRing V
w_3 : Algebra S V
w_4 : Module.FaithfullyFlat S V
w_5 : Module.Finite S V
w_6 : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst_1 : Algebra R V :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S V) (algebraMap R S))
scalarTowerInst : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  AlgEquiv.trans (A₂ := V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.symm (TensorProduct.cancelBaseChange R S V V S) : V ⊗[R] S ≃ₐ[V] V ⊗[S] (S ⊗[R] S))
    (AlgEquiv.trans (TensorProduct.congr AlgEquiv.refl e_1 : V ⊗[S] (S ⊗[R] S) ≃ₐ[V] V ⊗[S] (S × U))
        (AlgEquiv.trans (TensorProduct.prodRight S V V S U : V ⊗[S] (S × U) ≃ₐ[V] V ⊗[S] S × V ⊗[S] U)
            (AlgEquiv.trans (AlgEquiv.prodCongr (TensorProduct.rid S V V) f)
                (AlgEquiv.trans (AlgEquiv.prodCongr (AlgEquiv.symm (AlgEquiv.funUnique V Unit V)) AlgEquiv.refl)
                  (AlgEquiv.symm (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V))) :
              (V ⊗[S] S × V ⊗[S] U) ≃ₐ[V] Unit ⊕ Fin n → V) :
          V ⊗[S] (S × U) ≃ₐ[V] Unit ⊕ Fin n → V) :
      V ⊗[S] (S ⊗[R] S) ≃ₐ[V] Unit ⊕ Fin n → V)
⊢ IsFiniteSplit V (V ⊗[R] S)

Tactic:
exact .of_algEquiv e.symm
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : PowerBasis R S
a :
  ∀ (i j : Fin h.dim),
    Eq (α := R)
      ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) i
          j :
        R)
      ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
          (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
        R)
⊢ Eq (α := Matrix (Fin h.dim) (Fin h.dim) R)
    ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) :
      Matrix (Fin h.dim) (Fin h.dim) R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R) fun (i j : Fin h.dim) ↦
        (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ))) :
      Matrix (Fin h.dim) (Fin h.dim) R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : PowerBasis R S
i j : Fin h.dim
a :
  Eq (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ))) : R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
a₃ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R) (HMul.hMul (β := S) (h.gen ^ (↑i : ℕ)) ((h.basis : (a : Fin h.dim) → S) j : S)) : R)
    ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
a₄ a₅ :
  Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
    ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
⊢ Eq (α := R)
    ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) i
        j :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)

Tactic:
rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]

Premises used: Algebra.traceForm_toMatrix, pow_add, Matrix.of_apply, PowerBasis.basis_eq_pow
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
⊢ 0 < pb.dim

Tactic:
have d_pos : 0 < pb.dim := PowerBasis.dim_pos pb
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
⊢ 0 < natDegree (minpoly K pb.gen)

Tactic:
simpa
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
⊢ 0 < natDegree (minpoly K pb.gen)

Tactic:
have d_pos' : 0 < (minpoly K pb.gen).natDegree := by simpa
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < natDegree (minpoly K pb.gen)
⊢ Nonempty (Fin pb.dim)

Tactic:
haveI : Nonempty (Fin pb.dim) := ⟨⟨0, d_pos⟩⟩
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < natDegree (minpoly K pb.gen)
this : Nonempty (Fin pb.dim)
rw :
  Matrix.trace (n := Fin pb.dim)
      (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
        pb.gen) =
    -nextCoeff (minpoly K pb.gen)
rw₁ :
  -coeff
        (charpoly (n := Fin pb.dim)
          (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
              (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
            pb.gen))
        (Fintype.card (Fin pb.dim) - 1) =
    -nextCoeff (minpoly K pb.gen)
rw₂ : -coeff (minpoly K pb.gen) (Fintype.card (Fin pb.dim) - 1) = -nextCoeff (minpoly K pb.gen)
rw₃ : -coeff (minpoly K pb.gen) (Fintype.card (Fin (natDegree (minpoly K pb.gen))) - 1) = -nextCoeff (minpoly K pb.gen)
rw₄ : -coeff (minpoly K pb.gen) (natDegree (minpoly K pb.gen) - 1) = -nextCoeff (minpoly K pb.gen)
rw₅ rw₆ : -nextCoeff (minpoly K pb.gen) = -nextCoeff (minpoly K pb.gen)
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)

Tactic:
rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, ←
    pb.natDegree_minpoly, Fintype.card_fin, ← nextCoeff_of_natDegree_pos d_pos']

Premises used: Fintype.card_fin, Polynomial.nextCoeff_of_natDegree_pos, Matrix.trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, PowerBasis.basis, Algebra.trace_eq_matrix_trace, PowerBasis.natDegree_minpoly
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
F : Type u_6
inst_2 : Field F
inst_3 : Algebra K S
inst_4 : Algebra K F
inst_5 : Nontrivial S
pb : PowerBasis K S
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K pb.gen))
rw : (algebraMap K F : (a : K) → F) (-nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
rw₁ : -(algebraMap K F : (a : K) → F) (nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
rw₂ : -nextCoeff (Polynomial.map (algebraMap K F) (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
rw₃ : - -(roots (Polynomial.map (algebraMap K F) (minpoly K pb.gen))).sum = (aroots (minpoly K pb.gen) F).sum
rw₄ rw₅ : (roots (Polynomial.map (algebraMap K F) (minpoly K pb.gen))).sum = (aroots (minpoly K pb.gen) F).sum
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K S : (a : S) → K) pb.gen : K) = (aroots (minpoly K pb.gen) F).sum

Tactic:
rw [PowerBasis.trace_gen_eq_nextCoeff_minpoly, map_neg,
    ← nextCoeff_map_eq, hf.nextCoeff_eq_neg_sum_roots_of_monic
      ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _),
    neg_neg]

Premises used: minpoly.monic, PowerBasis.isIntegral_gen, PowerBasis.trace_gen_eq_nextCoeff_minpoly, neg_neg, map_neg, Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic, Polynomial.nextCoeff_map_eq, Polynomial.Monic.map
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : ¬IsIntegral K x
h : ¬∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)
⊢ Eq.{u_4 + 1} (α := K) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) (0 : K)

Tactic:
rw [trace_eq_zero_of_not_exists_basis, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, Algebra.trace_eq_zero_of_not_exists_basis
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : ¬IsIntegral K x
h : ∀ (hx : ∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)), IsIntegral K x
⊢ ¬∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)

Tactic:
contrapose hx
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : ∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)
h : ∀ (s : Finset ↥K⟮x⟯) (b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯), IsIntegral K x
⊢ IsIntegral K x

Tactic:
obtain ⟨s, ⟨b⟩⟩ := hx
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
⊢ IsIntegral K x

Tactic:
.of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_

Premises used: IntermediateField.adjoin, IsIntegral.of_mem_of_fg, Singleton.singleton, IntermediateField.toSubalgebra
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
h :
  Submodule.FG.{u_4, u_5} (R := K) (M := L)
    ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (toSubalgebra K⟮x⟯))
h₁ : Membership.mem (γ := Subalgebra K L) (toSubalgebra K⟮x⟯) x
⊢ IsIntegral K x

Tactic:
refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
⊢ Submodule.FG.{u_4, u_5} (R := K) (M := L)
    ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (toSubalgebra K⟮x⟯))

Tactic:
(Submodule.fg_iff_finiteDimensional _).mpr (b.finiteDimensional_of_finite)

Premises used: Iff.mpr, Module.Basis.finiteDimensional_of_finite, Submodule.fg_iff_finiteDimensional
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
⊢ Submodule.FG.{u_4, u_5} (R := K) (M := L)
    ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (toSubalgebra K⟮x⟯))

Tactic:
exact (Submodule.fg_iff_finiteDimensional _).mpr (b.finiteDimensional_of_finite)

Premises used: Iff.mpr, Submodule.fg_iff_finiteDimensional
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
⊢ Membership.mem (γ := Subalgebra K L) (toSubalgebra K⟮x⟯) x

Tactic:
subset_adjoin K _ (Set.mem_singleton x)

Premises used: Set.mem_singleton, Set.Mem, IntermediateField.subset_adjoin
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
⊢ Membership.mem (γ := Subalgebra K L) (toSubalgebra K⟮x⟯) x

Tactic:
exact subset_adjoin K _ (Set.mem_singleton x)

Premises used: Set.mem_singleton, IntermediateField.subset_adjoin
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
⊢ Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)

Tactic:
have injKxL := (algebraMap K⟮x⟯ L).injective
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
pos :
  ∀ (hx : IsIntegral K x),
    (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
      (aroots (minpoly K x) F).sum
neg :
  ∀ (hx : ¬IsIntegral K x),
    (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
      (aroots (minpoly K x) F).sum
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum

Tactic:
by_cases hx : IsIntegral K x

Premises used: IsIntegral