-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : CharZero F
inst_4 : FiniteDimensional F K
a : K
h : Ne.{u_1 + 1} (α := F) (↑(Module.finrank (↥F⟮a⟯) K) : F) 0
rw :
  normalizedTraceAux F K a =
    HMul.hMul (α := F) (β := F) ((↑(Module.finrank F K) : F)⁻¹ : F) ((trace F K : (a : K) → F) a : F)
rw₁ :
  normalizedTraceAux F K a =
    HMul.hMul (α := F) (β := F) ((trace F K : (a : K) → F) a : F) ((↑(Module.finrank F K) : F)⁻¹ : F)
rw₂ :
  normalizedTraceAux F K a =
    HDiv.hDiv (α := F) (β := F) ((trace F K : (a : K) → F) a : F) ((↑(Module.finrank F K) : F) : F)
rw₃ :
  normalizedTraceAux F K a =
    HSMul.hSMul (β := F) (Module.finrank (↥F⟮a⟯) K) ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F) /
      (↑(Module.finrank F K) : F)
rw₄ :
  normalizedTraceAux F K a =
    HSMul.hSMul (β := F) (Module.finrank (↥F⟮a⟯) K) ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F) /
      (↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯ * Module.finrank (↥F⟮a⟯) K) : F)
rw₅ :
  normalizedTraceAux F K a =
    HMul.hMul (α := F) (β := F) ((↑(Module.finrank (↥F⟮a⟯) K) : F) : F)
        ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F) /
      (↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯ * Module.finrank (↥F⟮a⟯) K) : F)
rw₆ :
  normalizedTraceAux F K a =
    HMul.hMul (α := F) (β := F) ((↑(Module.finrank (↥F⟮a⟯) K) : F) : F)
        ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F) /
      HMul.hMul (α := F) (↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯) : F) (↑(Module.finrank (↥F⟮a⟯) K) : F)
rw₇ :
  normalizedTraceAux F K a =
    HMul.hMul (α := F) (β := F) ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F)
        ((↑(Module.finrank (↥F⟮a⟯) K) : F) : F) /
      HMul.hMul (α := F) (↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯) : F) (↑(Module.finrank (↥F⟮a⟯) K) : F)
rw₈ :
  normalizedTraceAux F K a =
    HDiv.hDiv (α := F) (β := F) ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F)
      ((↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯) : F) : F)
rw₉ :
  normalizedTraceAux F K a =
    HMul.hMul (α := F) (β := F) ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F)
      ((↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯) : F)⁻¹ : F)
rw₁₀ :
  normalizedTraceAux F K a =
    HMul.hMul (α := F) (β := F) ((↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯) : F)⁻¹ : F)
      ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F)
rw₁₁ :
  normalizedTraceAux F K a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯) : F)⁻¹
      ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F)
rw₁₂ rw₁₃ :
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯) : F)⁻¹
      ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F) =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯) : F)⁻¹
      ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F)
⊢ normalizedTraceAux F K a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F K) : F)⁻¹ ((trace F K : (a : K) → F) a : F)

Tactic:
rw [smul_eq_mul, mul_comm, ← div_eq_mul_inv, trace_eq_trace_adjoin F a,
    ← Module.finrank_mul_finrank F F⟮a⟯ K, nsmul_eq_mul, Nat.cast_mul, mul_comm,
    mul_div_mul_right _ _ h, div_eq_mul_inv, mul_comm, ← smul_eq_mul, normalizedTraceAux_def]

Premises used: mul_div_mul_right, Membership.mem, Subtype, trace_eq_trace_adjoin, div_eq_mul_inv, Nat.cast_mul, Module.finrank_mul_finrank, IntermediateField.adjoin, mul_comm, nsmul_eq_mul, smul_eq_mul, Singleton.singleton, _private.0.Algebra.normalizedTraceAux_def