-- Mathlib/RingTheory/Trace/Basic.lean
theorem sum_embeddings_eq_finrank_mul [FiniteDimensional K F] [Algebra.IsSeparable K F]
    (pb : PowerBasis K L) :
    ∑ σ : F →ₐ[K] E, σ (algebraMap L F pb.gen) =
      finrank L F •
        (@Finset.univ _ (PowerBasis.AlgHom.fintype pb)).sum fun σ : L →ₐ[K] E => σ pb.gen

Proof state:
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen

Tactic:
letI : ∀ f : L →ₐ[K] E, Fintype (haveI := f.toRingHom.toAlgebra; AlgHom L F E) := ?_

Result:
case refine_2
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝² : FiniteDimensional L F
this✝¹ : Algebra.IsSeparable L F
this✝ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
this : (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E) := ?refine_1
⊢ ∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen

case refine_1
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E)

Proof state:
case refine_2.e_a
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝³ : FiniteDimensional L F
this✝² : Algebra.IsSeparable L F
this✝¹ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
this✝ : (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E) := ?refine_1
σ : L →ₐ[K] E
x✝ : σ ∈ Finset.univ
this : Algebra L E := σ.toAlgebra
⊢ Finset.univ.card = Fintype.card (F →ₐ[L] E)

Tactic:
exact Finset.card_univ (α := F →ₐ[L] E)

Result:
no goals

Proof state:
case refine_2
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝² : FiniteDimensional L F
this✝¹ : Algebra.IsSeparable L F
this✝ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
this : (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E) := fun σ => minpoly.AlgHom.fintype L F E
⊢ ∀ (x : F →ₐ[K] E), x ((algebraMap L F) pb.gen) = (algHomEquivSigma x).fst pb.gen

Tactic:
intro σ

Result:
case refine_2
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝² : FiniteDimensional L F
this✝¹ : Algebra.IsSeparable L F
this✝ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
this : (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E) := fun σ => minpoly.AlgHom.fintype L F E
σ : F →ₐ[K] E
⊢ σ ((algebraMap L F) pb.gen) = (algHomEquivSigma σ).fst pb.gen

Proof state:
case refine_2
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝³ : FiniteDimensional L F
this✝² : Algebra.IsSeparable L F
this✝¹ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
this✝ : (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E) := ?refine_1
σ : L →ₐ[K] E
x✝ : σ ∈ Finset.univ
this : Algebra L E := σ.toAlgebra
⊢ Finset.univ.card • σ pb.gen = finrank L F • σ pb.gen

Tactic:
congr

Result:
case refine_2.e_a
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝³ : FiniteDimensional L F
this✝² : Algebra.IsSeparable L F
this✝¹ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
this✝ : (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E) := ?refine_1
σ : L →ₐ[K] E
x✝ : σ ∈ Finset.univ
this : Algebra L E := σ.toAlgebra
⊢ Finset.univ.card = finrank L F

Proof state:
case refine_2
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝² : FiniteDimensional L F
this✝¹ : Algebra.IsSeparable L F
this✝ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
this : (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E) := fun σ => minpoly.AlgHom.fintype L F E
σ : F →ₐ[K] E
⊢ σ ((algebraMap L F) pb.gen) = (algHomEquivSigma σ).fst pb.gen

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

Result:
no goals

Proof state:
case refine_2
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝² : FiniteDimensional L F
this✝¹ : Algebra.IsSeparable L F
this✝ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
this : (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E) := ?refine_1
⊢ ∑ a : L →ₐ[K] E, ∑ s : F →ₐ[L] E, ⟨a, s⟩.fst pb.gen = ∑ x : L →ₐ[K] E, finrank L F • x pb.gen

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

Result:
case refine_2
K : Type u_4
L : Type u_5
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Algebra K L
F : Type u_6
inst✝⁸ : Field F
inst✝⁷ : Algebra L F
inst✝⁶ : Algebra K F
inst✝⁵ : IsScalarTower K L F
E : Type u_7
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K F
inst✝ : Algebra.IsSeparable K F
pb : PowerBasis K L
this✝² : FiniteDimensional L F
this✝¹ : Algebra.IsSeparable L F
this✝ : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
this : (f : L →ₐ[K] E) → Fintype (F →ₐ[L] E) := ?refine_1
σ : L →ₐ[K] E
x✝ : σ ∈ Finset.univ
⊢ ∑ s : F →ₐ[L] E, ⟨σ, s⟩.fst pb.gen = finrank L F • σ pb.gen