awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
pos :
  Eq.{u_8 + 1} (α := B)
    ((e : (a : A) → B)
        (Matrix.trace.{u_9, u_7} (n := ↥s) ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x)) :
      B)
    (Matrix.trace.{u_9, u_8} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x) : B)
⊢ Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)

Tactic:
rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]

Premises used: Module.Basis.mapCoeffs, Algebra.trace_eq_matrix_trace, RingEquiv.symm
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
pos :
  Eq.{u_8 + 1} (α := B)
    (Matrix.trace.{u_9, u_8} (n := ↥s)
      (Matrix.map.{u_7, u_8, u_9, u_9} (α := A)
        ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x) (⇑e : (a : A) → B)))
    (Matrix.trace.{u_9, u_8} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x))
⊢ Eq.{u_8 + 1} (α := B)
    ((e : (a : A) → B)
        (Matrix.trace.{u_9, u_7} (n := ↥s) ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x)) :
      B)
    (Matrix.trace.{u_9, u_8} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x) : B)

Tactic:
rw [AddMonoidHom.map_trace]

Premises used: AddMonoidHom.map_trace
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
pos :
  Eq (α := Matrix.{u_9, u_9, u_8} (↥s) (↥s) B)
    (Matrix.map.{u_7, u_8, u_9, u_9} (α := A) ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x)
      (⇑e : (a : A) → B))
    ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x)
⊢ Eq.{u_8 + 1} (α := B)
    (Matrix.trace.{u_9, u_8} (n := ↥s)
      (Matrix.map.{u_7, u_8, u_9, u_9} (α := A)
        ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x) (⇑e : (a : A) → B)))
    (Matrix.trace.{u_9, u_8} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x))

Tactic:
congr
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
pos :
  ∀ (i j : ↥s),
    Eq.{u_8 + 1} (α := B)
      (Matrix.map.{u_7, u_8, u_9, u_9} (α := A)
          ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x) (⇑e : (a : A) → B) i j :
        B)
      ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x i j : B)
⊢ Eq (α := Matrix.{u_9, u_9, u_8} (↥s) (↥s) B)
    (Matrix.map.{u_7, u_8, u_9, u_9} (α := A) ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x)
      (⇑e : (a : A) → B))
    ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x)

Tactic:
ext i j
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
i j : ↥s
⊢ Eq.{u_8 + 1} (α := B)
    (Matrix.map.{u_7, u_8, u_9, u_9} (α := A) ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x)
        (⇑e : (a : A) → B) i j :
      B)
    ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x i j : B)

Tactic:
simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]

Premises used: Algebra.leftMulMatrix_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)
neg : ¬∃ (s : Finset C), Nonempty (Basis (↥s) A C)
⊢ Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)

Tactic:
rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]

Premises used: LinearMap.zero_apply, map_zero, Algebra.trace_eq_zero_of_not_exists_basis
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)
s : Finset C
b : Basis (↥s) A C
⊢ ∀ (c : A) (x : C), HSMul.hSMul.{u_8, u_9, u_9} (α := B) ((e : (a : A) → B) c : B) x = c • x

Tactic:
simp [Algebra.smul_def, ← he]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)
s : Finset C
b : Basis (↥s) A C
⊢ False

Tactic:
exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩

Premises used: Module.Basis.mapCoeffs, Nonempty.intro, Exists.intro
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
pos :
  ∀ (h : ∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
    Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)
neg neg₁ :
  ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
    Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)
neg₂ : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)), ¬∃ (s : Finset C), Nonempty (Basis (↥s) A C)
neg₃ : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)) (s : Finset C) (b : Basis (↥s) A C), False
⊢ Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)

Tactic:
classical
  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
  · obtain ⟨s, ⟨b⟩⟩ := h
    letI : Algebra A B := RingHom.toAlgebra e
    letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
    rw [AddMonoidHom.map_trace]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
  rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]
  intro ⟨s, ⟨b⟩⟩
  exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩

Premises used: LinearMap.zero_apply, AddMonoidHom.map_trace, Finset, map_zero, Algebra.trace_eq_zero_of_not_exists_basis, Algebra.leftMulMatrix_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst : CommRing A₁
inst_1 : CommRing B₁
inst_2 : CommRing A₂
inst_3 : CommRing B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
x : B₁
this : Algebra A₁ B₂ :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
rw :
  Eq.{u_7 + 1} (α := A₁) ((trace A₁ B₂ : (a : B₂) → A₁) ((e' : (a : B₁) → B₂) x : B₂) : A₁)
    ((trace A₁ B₂ : (a : B₂) → A₁) ((e₂ : (a : B₁) → B₂) x : B₂) : A₁)
⊢ Eq.{u_7 + 1} (α := A₁) ((trace A₁ B₁ : (a : B₁) → A₁) x : A₁)
    ((e₁.symm : (a : A₂) → A₁) ((trace A₂ B₂ : (a : B₂) → A₂) ((e₂ : (a : B₁) → B₂) x : B₂) : A₂) : A₁)

Tactic:
rw [← Algebra.trace_eq_of_ringEquiv e₁ he, ← Algebra.trace_eq_of_algEquiv e',
    RingEquiv.symm_apply_apply]

Premises used: Algebra.trace_eq_of_ringEquiv, Algebra.trace_eq_of_algEquiv, RingEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A₁ : Type u_7
B₁ : Type u_8
A₂ : Type u_9
B₂ : Type u_10
inst : CommRing A₁
inst_1 : CommRing B₁
inst_2 : CommRing A₂
inst_3 : CommRing B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
x : B₁
this : Algebra A₁ B₂ :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Eq.{u_7 + 1} (α := A₁) ((trace A₁ B₂ : (a : B₂) → A₁) ((e' : (a : B₁) → B₂) x : B₂) : A₁)
    ((trace A₁ B₂ : (a : B₂) → A₁) ((e₂ : (a : B₁) → B₂) x : B₂) : A₁)

Tactic:
rfl
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
rw : (aroots (minpoly K pb.gen) E).Nodup
f : { x : E // x ∈ aroots (minpoly K pb.gen) E } → E
hfg : ∀ (x : { x : E // x ∈ aroots (minpoly K pb.gen) E }), _root_.id (↑x : E) = _root_.id (↑x : E)
h :
  ∀ (x : L →ₐ[K] E),
    Eq.{u_7 + 1} (α := E) ((x : (a : L) → E) pb.gen : E)
      (_root_.id (↑((pb.liftEquiv' : (a : L →ₐ[K] E) → { y : E // y ∈ (minpoly K pb.gen).aroots E }) x) : E) : E)
⊢ Eq.{u_7 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((Algebra.trace K L : (a : L) → K) pb.gen : K) : E)
    (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen : E)

Tactic:
rw [pb.trace_gen_eq_sum_roots hE, Fintype.sum_equiv pb.liftEquiv', Finset.sum_mem_multiset,
    Finset.sum_eq_multiset_sum, Multiset.toFinset_val, Multiset.dedup_eq_self.mpr _,
    Multiset.map_id]

Premises used: Iff.mpr, Multiset.map_id, PowerBasis.liftEquiv', Multiset.dedup_eq_self, Finset.sum_eq_multiset_sum, PowerBasis.trace_gen_eq_sum_roots, Finset.sum_mem_multiset, Fintype.sum_equiv, Multiset.toFinset_val
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ (aroots (minpoly K pb.gen) E).Nodup

Tactic:
nodup_roots ((separable_map _).mpr hfx)

Premises used: Iff.mpr, Polynomial.nodup_roots, Polynomial.separable_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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ (aroots (minpoly K pb.gen) E).Nodup

Tactic:
exact nodup_roots ((separable_map _).mpr hfx)

Premises used: Iff.mpr, Polynomial.nodup_roots, Polynomial.separable_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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
x : { x : E // x ∈ aroots (minpoly K pb.gen) E }
⊢ _root_.id (↑x : E) = _root_.id (↑x : E)

Tactic:
rfl
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Eq.{u_7 + 1} (α := E) ((σ : (a : L) → E) pb.gen : E) (_root_.id ((σ : (a : L) → E) pb.gen) : E)
h₁ h₂ : Eq.{u_7 + 1} (α := E) ((σ : (a : L) → E) pb.gen : E) ((σ : (a : L) → E) pb.gen : E)
⊢ Eq.{u_7 + 1} (α := E) ((σ : (a : L) → E) pb.gen : E)
    (_root_.id (↑((pb.liftEquiv' : (a : L →ₐ[K] E) → { y : E // y ∈ (minpoly K pb.gen).aroots E }) σ) : E) : E)

Tactic:
rw [PowerBasis.liftEquiv'_apply_coe, id_def]

Premises used: id_def, PowerBasis.liftEquiv'_apply_coe
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
⊢ FiniteDimensional L F

Tactic:
haveI : FiniteDimensional L F := FiniteDimensional.right K L F
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this : FiniteDimensional L F
⊢ Algebra.IsSeparable L F

Tactic:
haveI : Algebra.IsSeparable L F := Algebra.isSeparable_tower_top_of_isSeparable K L F
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
rw :
  Eq.{u_7 + 1} (α := E)
    (∑ a : L →ₐ[K] E,
      ∑ s : F →ₐ[L] E,
        (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) a s) :
            (a : L) → E)
          pb.gen)
    (∑ x : L →ₐ[K] E, HSMul.hSMul (β := E) (finrank L F) ((x : (a : L) → E) pb.gen : E))
rw₁ :
  ∀ (x : F →ₐ[K] E),
    Eq.{u_7 + 1} (α := E) ((x : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) : E)
      ((Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E)
              ((algHomEquivSigma : (a : F →ₐ[K] E) → (f : L →ₐ[K] E) × (F →ₐ[L] E)) x) :
            (a : L) → E)
          pb.gen :
        E)
⊢ ∑ σ : F →ₐ[K] E, (σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) =
    HSMul.hSMul (β := E) (finrank L F) (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen)

Tactic:
rw [Fintype.sum_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,
    ← Finset.univ_sigma_univ, Finset.sum_sigma, ← Finset.sum_nsmul]

Premises used: Finset.sum_nsmul, algHomEquivSigma, PowerBasis.gen, Finset.sum_sigma, Sigma.fst, Finset.univ_sigma_univ, Fintype.sum_equiv, DFunLike.coe
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ Eq.{u_7 + 1} (α := E)
    (∑ a : L →ₐ[K] E,
      ∑ s : F →ₐ[L] E,
        (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) a s) :
            (a : L) → E)
          pb.gen)
    (∑ x : L →ₐ[K] E, HSMul.hSMul (β := E) (finrank L F) ((x : (a : L) → E) pb.gen : E))

Tactic:
Finset.sum_congr rfl fun σ _ => ?_

Premises used: Finset.sum_congr, rfl
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
refine :
  ∀ (σ : L →ₐ[K] E),
    Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ →
      ∑ s : F →ₐ[L] E,
          (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) σ s) :
              (a : L) → E)
            pb.gen =
        HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
⊢ Eq.{u_7 + 1} (α := E)
    (∑ a : L →ₐ[K] E,
      ∑ s : F →ₐ[L] E,
        (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) a s) :
            (a : L) → E)
          pb.gen)
    (∑ x : L →ₐ[K] E, HSMul.hSMul (β := E) (finrank L F) ((x : (a : L) → E) pb.gen : E))

Tactic:
refine Finset.sum_congr rfl fun σ _ => ?_

Premises used: Finset.sum_congr, rfl
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this_3 : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ
this : Algebra L E := σ.toAlgebra
simp_rw simp_rw₁ :
  ∑ x : F →ₐ[L] E, (σ : (a : L) → E) pb.gen = HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
simp_rw₂ :
  HSMul.hSMul (β := E) (Finset.card (α := F →ₐ[L] E) Finset.univ) ((σ : (a : L) → E) pb.gen : E) =
    HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
simp_rw₃ :
  HSMul.hSMul (β := E) (Fintype.card (F →ₐ[L] E)) ((σ : (a : L) → E) pb.gen : E) =
    HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
⊢ ∑ s : F →ₐ[L] E,
      (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) σ s) :
          (a : L) → E)
        pb.gen =
    HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)

Tactic:
simp_rw [Finset.sum_const, Finset.card_univ, ← AlgHom.card L F E]

Premises used: Finset.card_univ, AlgHom.card, Finset.sum_const
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : F →ₐ[K] E
⊢ Eq.{u_7 + 1} (α := E) ((σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) : E)
    ((Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E)
            ((algHomEquivSigma : (a : F →ₐ[K] E) → (f : L →ₐ[K] E) × (F →ₐ[L] E)) σ) :
          (a : L) → E)
        pb.gen :
      E)

Tactic:
simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.restrictDomain, AlgHom.comp_apply,
      IsScalarTower.coe_toAlgHom']

Premises used: IsScalarTower.coe_toAlgHom', algHomEquivSigma, AlgHom.comp_apply, Equiv.coe_fn_mk, AlgHom.restrictDomain
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
⊢ IsIntegral K x

Tactic:
have hx := Algebra.IsSeparable.isIntegral K 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis.{u_4, u_5} K ↥K⟮x⟯ := adjoin.powerBasis hx
rw :
  HSMul.hSMul (β := E) (finrank (↥K⟮x⟯) L) (∑ σ : ↥K⟮x⟯ →ₐ[K] E, (σ : (a : ↥K⟮x⟯) → E) pb.gen) =
    ∑ σ : L →ₐ[K] E, (σ : (a : L) → E) x
rw₁ : IsSeparable K pb.gen
⊢ Eq.{u_7 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((Algebra.trace K L : (a : L) → K) x : K) : E)
    (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) x : E)

Tactic:
rw [trace_eq_trace_adjoin K x, Algebra.smul_def, map_mul, ← adjoin.powerBasis_gen hx,
    trace_eq_sum_embeddings_gen E pb (IsAlgClosed.splits _), ← Algebra.smul_def,
    algebraMap_smul]

Premises used: IntermediateField.adjoin.powerBasis_gen, algebraMap_smul, trace_eq_trace_adjoin, map_mul, IsAlgClosed.splits, Algebra.smul_def, trace_eq_sum_embeddings_gen
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
hx : IsIntegral K x
pb : PowerBasis.{u_4, u_5} K ↥K⟮x⟯ := adjoin.powerBasis hx
⊢ HSMul.hSMul (β := E) (finrank (↥K⟮x⟯) L) (∑ σ : ↥K⟮x⟯ →ₐ[K] E, (σ : (a : ↥K⟮x⟯) → E) pb.gen) =
    ∑ σ : L →ₐ[K] E, (σ : (a : L) → E) x

Tactic:
(sum_embeddings_eq_finrank_mul L E pb).symm

Premises used: Set.Mem, sum_embeddings_eq_finrank_mul, IntermediateField.adjoin, Eq.symm