awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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)
⊢ normalizedTraceAux F K a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F K) : F)⁻¹ ((trace F K : (a : K) → F) a : F)
have 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)
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]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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)
⊢ normalizedTraceAux F K a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F K) : F)⁻¹ ((trace F K : (a : K) → F) a : F)
have 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)
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]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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)
⊢ normalizedTraceAux F K a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F K) : F)⁻¹ ((trace F K : (a : K) → F) a : F)
have 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)
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]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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)
⊢ normalizedTraceAux F K a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F K) : F)⁻¹ ((trace F K : (a : K) → F) a : F)
have 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)
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]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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)
⊢ normalizedTraceAux F K a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F K) : F)⁻¹ ((trace F K : (a : K) → F) a : F)
have 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)
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]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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)
⊢ normalizedTraceAux F K a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F K) : F)⁻¹ ((trace F K : (a : K) → F) a : F)
have 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)
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]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
have this : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
Tactic: have : FiniteDimensional F F⟮a⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral a)
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
have this₁ : FiniteDimensional.{u_1, u_2} F ↥F⟮b⟯
Tactic: have : FiniteDimensional F F⟮b⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral b)
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this_1 : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮b⟯
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
have ha : a ∈ E
Tactic: have ha : a ∈ E := (le_sup_left : F⟮a⟯ ≤ E) <| mem_adjoin_simple_self F a
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this_1 : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮b⟯
ha : a ∈ E
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
have hb : b ∈ E
Tactic: have hb : b ∈ E := (le_sup_right : F⟮b⟯ ≤ E) <| mem_adjoin_simple_self F b
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (hypothesis)
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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this_1 : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
have hab : a + b ∈ E
Tactic: have hab : a + b ∈ E := IntermediateField.add_mem E ha hb
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this_1 : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) a ha
b' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) b hb
ab' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a + b) hab
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
have rw : normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F K b
Tactic: rw [normalizedTraceAux_intermediateField F K a',
      normalizedTraceAux_intermediateField F K b',
      normalizedTraceAux_intermediateField F K ab',
      normalizedTraceAux_eq_of_finiteDimensional F a',
      normalizedTraceAux_eq_of_finiteDimensional F b',
      normalizedTraceAux_eq_of_finiteDimensional F ab',
      ← smul_add, ← map_add, AddMemClass.mk_add_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this_1 : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) a ha
b' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) b hb
ab' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a + b) hab
rw : normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F K b
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
have rw₁ : normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F (↥E) b'
Tactic: rw [normalizedTraceAux_intermediateField F K a',
      normalizedTraceAux_intermediateField F K b',
      normalizedTraceAux_intermediateField F K ab',
      normalizedTraceAux_eq_of_finiteDimensional F a',
      normalizedTraceAux_eq_of_finiteDimensional F b',
      normalizedTraceAux_eq_of_finiteDimensional F ab',
      ← smul_add, ← map_add, AddMemClass.mk_add_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this_1 : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) a ha
b' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) b hb
ab' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a + b) hab
rw : normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F K b
rw₁ : normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F (↥E) b'
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
have rw₂ : normalizedTraceAux F (↥E) ab' = normalizedTraceAux F (↥E) a' + normalizedTraceAux F (↥E) b'
Tactic: rw [normalizedTraceAux_intermediateField F K a',
      normalizedTraceAux_intermediateField F K b',
      normalizedTraceAux_intermediateField F K ab',
      normalizedTraceAux_eq_of_finiteDimensional F a',
      normalizedTraceAux_eq_of_finiteDimensional F b',
      normalizedTraceAux_eq_of_finiteDimensional F ab',
      ← smul_add, ← map_add, AddMemClass.mk_add_mk]
-- Lean 4 proof step from Mathlib.FieldTheory.NormalizedTrace (goal)
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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this_1 : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮b⟯
ha : a ∈ E
hb : b ∈ E
hab : a + b ∈ E
a' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) a ha
b' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) b hb
ab' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a + b) hab
rw : normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F K b
rw₁ : normalizedTraceAux F K (a + b) = normalizedTraceAux F (↥E) a' + normalizedTraceAux F (↥E) b'
rw₂ : normalizedTraceAux F (↥E) ab' = normalizedTraceAux F (↥E) a' + normalizedTraceAux F (↥E) b'
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
have rw₃ : normalizedTraceAux F (↥E) ab' =
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) a' : F) +
    normalizedTraceAux F (↥E) b'
Tactic: rw [normalizedTraceAux_intermediateField F K a',
      normalizedTraceAux_intermediateField F K b',
      normalizedTraceAux_intermediateField F K ab',
      normalizedTraceAux_eq_of_finiteDimensional F a',
      normalizedTraceAux_eq_of_finiteDimensional F b',
      normalizedTraceAux_eq_of_finiteDimensional F ab',
      ← smul_add, ← map_add, AddMemClass.mk_add_mk]