awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
inst_17 : Normal F E
σ : Gal(E/F)
⊢ (fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F)))
      ((fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁)) σ) =
    σ
have h : ∀ (a : E),
  Eq (α := E)
    (((fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F)))
            ((fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁)) σ) :
          (a : E) → E)
        a :
      E)
    ((σ : (a : E) → E) a : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
inst_17 : Normal F E
σ : Gal(E/F)
a : E
⊢ Eq (α := E)
    (((fun (σ : E →ₐ[F] K₁) ↦ (σ.restrictNormal' E : Gal(E/F)))
            ((fun (σ : Gal(E/F)) ↦ (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : E →ₐ[F] K₁)) σ) :
          (a : E) → E)
        a :
      E)
    ((σ : (a : E) → E) a : E)
have h : Eq (α := E) ((AlgHom.restrictNormal (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E)) E : (a : E) → E) a : E)
  ((σ : (a : E) → E) a : E)
Tactic: simp only [AlgHom.restrictNormal', AlgEquiv.coe_ofBijective]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
inst_17 : Normal F E
σ : Gal(E/F)
a : E
⊢ Eq (α := E) ((AlgHom.restrictNormal (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E)) E : (a : E) → E) a : E)
    ((σ : (a : E) → E) a : E)
have h : Eq.{u_3 + 1} (α := K₁)
  ((algebraMap E K₁ : (a : E) → K₁)
      ((AlgHom.restrictNormal (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E)) E : (a : E) → E) a : E) :
    K₁)
  ((algebraMap E K₁ : (a : E) → K₁) ((σ : (a : E) → E) a : E) : K₁)
Tactic: apply FaithfulSMul.algebraMap_injective E K₁
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_1
K : Type u_2
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Field K₃
inst_6 : Algebra F K₁
inst_7 : Algebra F K₂
inst_8 : Algebra F K₃
ϕ : K₁ →ₐ[F] K₂
χ : K₁ ≃ₐ[F] K₂
ψ : K₂ →ₐ[F] K₃
ω : K₂ ≃ₐ[F] K₃
E : Type u_6
inst_9 : Field E
inst_10 : Algebra F E
inst_11 : Algebra E K₁
inst_12 : Algebra E K₂
inst_13 : Algebra E K₃
inst_14 : IsScalarTower F E K₁
inst_15 : IsScalarTower F E K₂
inst_16 : IsScalarTower F E K₃
inst_17 : Normal F E
σ : Gal(E/F)
a : E
⊢ Eq.{u_3 + 1} (α := K₁)
    ((algebraMap E K₁ : (a : E) → K₁)
        ((AlgHom.restrictNormal (AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E)) E : (a : E) → E) a : E) :
      K₁)
    ((algebraMap E K₁ : (a : E) → K₁) ((σ : (a : E) → E) a : E) : K₁)
have h : Eq.{u_3 + 1} (α := K₁)
  ((AlgHom.comp (toAlgHom F E K₁) (↑σ : E →ₐ[F] E) : (a : E) → K₁) ((algebraMap E E : (a : E) → E) a : E) : K₁)
  ((algebraMap E K₁ : (a : E) → K₁) ((σ : (a : E) → E) a : E) : K₁)
Tactic: rw [AlgHom.restrictNormal_commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_6
K : Type u_7
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Normal F K
⊢ Eq (α := Gal(K/F) →* Gal(K/F)) (restrictNormalHom K) (MonoidHom.id Gal(K/F))
have h : ∀ (f : Gal(K/F)) (x : K),
  Eq (α := K) ((((restrictNormalHom K : (a : Gal(K/F)) → Gal(K/F)) f : Gal(K/F)) : (a : K) → K) x : K)
    ((((MonoidHom.id Gal(K/F) : (a : Gal(K/F)) → Gal(K/F)) f : Gal(K/F)) : (a : K) → K) x : K)
Tactic: ext f x
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_6
K : Type u_7
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Normal F K
f : Gal(K/F)
x : K
⊢ Eq (α := K) ((((restrictNormalHom K : (a : Gal(K/F)) → Gal(K/F)) f : Gal(K/F)) : (a : K) → K) x : K)
    ((((MonoidHom.id Gal(K/F) : (a : Gal(K/F)) → Gal(K/F)) f : Gal(K/F)) : (a : K) → K) x : K)
have h : Eq (α := K) ((f.restrictNormal K : (a : K) → K) x : K) ((f : (a : K) → K) x : K)
Tactic: dsimp only [restrictNormalHom, MonoidHom.mk'_apply, MonoidHom.id_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_6
K : Type u_7
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Normal F K
f : Gal(K/F)
x : K
⊢ Eq (α := K) ((f.restrictNormal K : (a : K) → K) x : K) ((f : (a : K) → K) x : K)
have h : Eq (α := K) (((algebraMap K K : K →+* K) : (a : K) → K) ((f.restrictNormal K : (a : K) → K) x : K) : K)
  (((algebraMap K K : K →+* K) : (a : K) → K) ((f : (a : K) → K) x : K) : K)
Tactic: apply (algebraMap K K).injective
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_6
K : Type u_7
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Normal F K
f : Gal(K/F)
x : K
⊢ Eq (α := K) (((algebraMap K K : K →+* K) : (a : K) → K) ((f.restrictNormal K : (a : K) → K) x : K) : K)
    (((algebraMap K K : K →+* K) : (a : K) → K) ((f : (a : K) → K) x : K) : K)
have h : Eq (α := K) ((f : (a : K) → K) ((algebraMap K K : (a : K) → K) x : K) : K)
  (((algebraMap K K : K →+* K) : (a : K) → K) ((f : (a : K) → K) x : K) : K)
Tactic: rw [AlgEquiv.restrictNormal_commutes]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_6
K₁ : Type u_7
K₂ : Type u_8
K₃ : Type u_9
inst : Field F
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Field K₃
inst_4 : Algebra F K₁
inst_5 : Algebra F K₂
inst_6 : Algebra F K₃
inst_7 : Algebra K₁ K₂
inst_8 : Algebra K₁ K₃
inst_9 : Algebra K₂ K₃
inst_10 : IsScalarTower F K₁ K₃
inst_11 : IsScalarTower F K₁ K₂
inst_12 : IsScalarTower F K₂ K₃
inst_13 : IsScalarTower K₁ K₂ K₃
inst_14 : Normal F K₁
inst_15 : Normal F K₂
⊢ Eq (α := MonoidHom.{u_9, u_7} Gal(K₃/F) Gal(K₁/F)) (AlgEquiv.restrictNormalHom K₁)
    (MonoidHom.comp (N := Gal(K₂/F)) (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂))
have h : ∀ (f : Gal(K₃/F)) (x : K₁),
  Eq (α := K₁) ((((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₃/F)) → Gal(K₁/F)) f : Gal(K₁/F)) : (a : K₁) → K₁) x : K₁)
    ((((MonoidHom.comp (N := Gal(K₂/F)) (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂) :
                (a : Gal(K₃/F)) → Gal(K₁/F))
              f :
            Gal(K₁/F)) :
          (a : K₁) → K₁)
        x :
      K₁)
Tactic: ext f x
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_6
K₁ : Type u_7
K₂ : Type u_8
K₃ : Type u_9
inst : Field F
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Field K₃
inst_4 : Algebra F K₁
inst_5 : Algebra F K₂
inst_6 : Algebra F K₃
inst_7 : Algebra K₁ K₂
inst_8 : Algebra K₁ K₃
inst_9 : Algebra K₂ K₃
inst_10 : IsScalarTower F K₁ K₃
inst_11 : IsScalarTower F K₁ K₂
inst_12 : IsScalarTower F K₂ K₃
inst_13 : IsScalarTower K₁ K₂ K₃
inst_14 : Normal F K₁
inst_15 : Normal F K₂
f : Gal(K₃/F)
x : K₁
⊢ Eq (α := K₁) ((((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₃/F)) → Gal(K₁/F)) f : Gal(K₁/F)) : (a : K₁) → K₁) x : K₁)
    ((((MonoidHom.comp (N := Gal(K₂/F)) (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂) :
                (a : Gal(K₃/F)) → Gal(K₁/F))
              f :
            Gal(K₁/F)) :
          (a : K₁) → K₁)
        x :
      K₁)
have h : Eq.{u_9 + 1} (α := K₃)
  (((algebraMap K₁ K₃ : K₁ →+* K₃) : (a : K₁) → K₃)
      ((((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₃/F)) → Gal(K₁/F)) f : Gal(K₁/F)) : (a : K₁) → K₁) x : K₁) :
    K₃)
  (((algebraMap K₁ K₃ : K₁ →+* K₃) : (a : K₁) → K₃)
      ((((MonoidHom.comp (N := Gal(K₂/F)) (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂) :
                  (a : Gal(K₃/F)) → Gal(K₁/F))
                f :
              Gal(K₁/F)) :
            (a : K₁) → K₁)
          x :
        K₁) :
    K₃)
Tactic: apply (algebraMap K₁ K₃).injective
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
F : Type u_6
K₁ : Type u_7
K₂ : Type u_8
K₃ : Type u_9
inst : Field F
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Field K₃
inst_4 : Algebra F K₁
inst_5 : Algebra F K₂
inst_6 : Algebra F K₃
inst_7 : Algebra K₁ K₂
inst_8 : Algebra K₁ K₃
inst_9 : Algebra K₂ K₃
inst_10 : IsScalarTower F K₁ K₃
inst_11 : IsScalarTower F K₁ K₂
inst_12 : IsScalarTower F K₂ K₃
inst_13 : IsScalarTower K₁ K₂ K₃
inst_14 : Normal F K₁
inst_15 : Normal F K₂
f : Gal(K₃/F)
x : K₁
⊢ Eq.{u_9 + 1} (α := K₃)
    (((algebraMap K₁ K₃ : K₁ →+* K₃) : (a : K₁) → K₃)
        ((((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₃/F)) → Gal(K₁/F)) f : Gal(K₁/F)) : (a : K₁) → K₁) x : K₁) :
      K₃)
    (((algebraMap K₁ K₃ : K₁ →+* K₃) : (a : K₁) → K₃)
        ((((MonoidHom.comp (N := Gal(K₂/F)) (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂) :
                    (a : Gal(K₃/F)) → Gal(K₁/F))
                  f :
                Gal(K₁/F)) :
              (a : K₁) → K₁)
            x :
          K₁) :
      K₃)
have h : Eq.{u_9 + 1} (α := K₃)
  (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K₂ K₃) (algebraMap K₁ K₂) : K₁ →+* K₃) :
        (a : K₁) → K₃)
      ((((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₃/F)) → Gal(K₁/F)) f : Gal(K₁/F)) : (a : K₁) → K₁) x : K₁) :
    K₃)
  (((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K₂ K₃) (algebraMap K₁ K₂) : K₁ →+* K₃) :
        (a : K₁) → K₃)
      ((((MonoidHom.comp (N := Gal(K₂/F)) (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂) :
                  (a : Gal(K₃/F)) → Gal(K₁/F))
                f :
              Gal(K₁/F)) :
            (a : K₁) → K₁)
          x :
        K₁) :
    K₃)
Tactic: rw [IsScalarTower.algebraMap_eq K₁ K₂ K₃]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
K₁ : Type u_6
K₂ : Type u_7
F : Type u_8
K₃ : Type u_9
inst : Field F
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Field K₃
inst_4 : Algebra F K₁
inst_5 : Algebra F K₂
inst_6 : Algebra F K₃
inst_7 : Algebra K₁ K₂
inst_8 : Algebra K₁ K₃
inst_9 : Algebra K₂ K₃
inst_10 : IsScalarTower F K₁ K₃
inst_11 : IsScalarTower F K₁ K₂
inst_12 : IsScalarTower F K₂ K₃
inst_13 : IsScalarTower K₁ K₂ K₃
inst_14 : Normal F K₁
inst_15 : Normal F K₂
f : Gal(K₃/F)
⊢ Eq.{u_6 + 1} (α := Gal(K₁/F)) ((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₃/F)) → Gal(K₁/F)) f : Gal(K₁/F))
    ((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₂/F)) → Gal(K₁/F))
        ((AlgEquiv.restrictNormalHom K₂ : (a : Gal(K₃/F)) → Gal(K₂/F)) f) :
      Gal(K₁/F))
have rw : Eq.{u_6 + 1} (α := Gal(K₁/F))
  ((MonoidHom.comp (N := Gal(K₂/F)) (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂) :
        (a : Gal(K₃/F)) → Gal(K₁/F))
      f :
    Gal(K₁/F))
  ((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₂/F)) → Gal(K₁/F))
      ((AlgEquiv.restrictNormalHom K₂ : (a : Gal(K₃/F)) → Gal(K₂/F)) f) :
    Gal(K₁/F))
Tactic: rw [IsScalarTower.AlgEquiv.restrictNormalHom_comp F K₁ K₂ K₃, MonoidHom.comp_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.Normal.Defs (goal)
Goal:
K₁ : Type u_6
K₂ : Type u_7
F : Type u_8
K₃ : Type u_9
inst : Field F
inst_1 : Field K₁
inst_2 : Field K₂
inst_3 : Field K₃
inst_4 : Algebra F K₁
inst_5 : Algebra F K₂
inst_6 : Algebra F K₃
inst_7 : Algebra K₁ K₂
inst_8 : Algebra K₁ K₃
inst_9 : Algebra K₂ K₃
inst_10 : IsScalarTower F K₁ K₃
inst_11 : IsScalarTower F K₁ K₂
inst_12 : IsScalarTower F K₂ K₃
inst_13 : IsScalarTower K₁ K₂ K₃
inst_14 : Normal F K₁
inst_15 : Normal F K₂
f : Gal(K₃/F)
rw :
  Eq.{u_6 + 1} (α := Gal(K₁/F))
    ((MonoidHom.comp (N := Gal(K₂/F)) (AlgEquiv.restrictNormalHom K₁) (AlgEquiv.restrictNormalHom K₂) :
          (a : Gal(K₃/F)) → Gal(K₁/F))
        f :
      Gal(K₁/F))
    ((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₂/F)) → Gal(K₁/F))
        ((AlgEquiv.restrictNormalHom K₂ : (a : Gal(K₃/F)) → Gal(K₂/F)) f) :
      Gal(K₁/F))
⊢ Eq.{u_6 + 1} (α := Gal(K₁/F)) ((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₃/F)) → Gal(K₁/F)) f : Gal(K₁/F))
    ((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₂/F)) → Gal(K₁/F))
        ((AlgEquiv.restrictNormalHom K₂ : (a : Gal(K₃/F)) → Gal(K₂/F)) f) :
      Gal(K₁/F))
have rw₁ : Eq.{u_6 + 1} (α := Gal(K₁/F))
  ((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₂/F)) → Gal(K₁/F))
      ((AlgEquiv.restrictNormalHom K₂ : (a : Gal(K₃/F)) → Gal(K₂/F)) f) :
    Gal(K₁/F))
  ((AlgEquiv.restrictNormalHom K₁ : (a : Gal(K₂/F)) → Gal(K₁/F))
      ((AlgEquiv.restrictNormalHom K₂ : (a : Gal(K₃/F)) → Gal(K₂/F)) f) :
    Gal(K₁/F))
Tactic: rw [IsScalarTower.AlgEquiv.restrictNormalHom_comp F K₁ K₂ K₃, MonoidHom.comp_apply]
-- 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
E : Type u_3
inst_3 : Field E
inst_4 : Algebra F E
f : E →ₐ[F] K
a : E
e : AlgEquiv.{u_1, u_3, u_2} F ↥F⟮a⟯ ↥F⟮((f : (a : E) → K) a : K)⟯ := AlgEquiv.trans (equivMap F⟮a⟯ f) (equivOfEq ⋯)
⊢ normalizedTraceAux.{u_1, u_2} F K ((f : (a : E) → K) a : K) = normalizedTraceAux F E a
have simp_rw : HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_3} F ↥F⟮a⟯) : F)⁻¹
    ((trace F ↥F⟮((f : (a : E) → K) a : K)⟯ : (a : ↥F⟮(f : (a : E) → K) a⟯) → F)
        (AdjoinSimple.gen F ((f : (a : E) → K) a) : ↥F⟮((f : (a : E) → K) a : K)⟯) :
      F) =
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_3} F ↥F⟮a⟯) : F)⁻¹
    ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F)
Tactic: simp_rw [normalizedTraceAux, ← LinearEquiv.finrank_eq e.toLinearEquiv]
-- 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
E : Type u_3
inst_3 : Field E
inst_4 : Algebra F E
f : E →ₐ[F] K
a : E
e : AlgEquiv.{u_1, u_3, u_2} F ↥F⟮a⟯ ↥F⟮((f : (a : E) → K) a : K)⟯ := AlgEquiv.trans (equivMap F⟮a⟯ f) (equivOfEq ⋯)
⊢ HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_3} F ↥F⟮a⟯) : F)⁻¹
      ((trace F ↥F⟮((f : (a : E) → K) a : K)⟯ : (a : ↥F⟮(f : (a : E) → K) a⟯) → F)
          (AdjoinSimple.gen F ((f : (a : E) → K) a) : ↥F⟮((f : (a : E) → K) a : K)⟯) :
        F) =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_3} F ↥F⟮a⟯) : F)⁻¹
      ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F)
have e_a : Eq.{u_1 + 1} (α := F)
  ((trace F ↥F⟮((f : (a : E) → K) a : K)⟯ : (a : ↥F⟮(f : (a : E) → K) a⟯) → F)
      (AdjoinSimple.gen F ((f : (a : E) → K) a) : ↥F⟮((f : (a : E) → K) a : K)⟯) :
    F)
  ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F)
Tactic: congr
-- 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 : FiniteDimensional F K
a : K
⊢ normalizedTraceAux F K a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F K) : F)⁻¹ ((trace F K : (a : K) → F) a : F)
have h : Ne.{u_1 + 1} (α := F) (↑(Module.finrank (↥F⟮a⟯) K) : F) 0
Tactic: have h := (Nat.cast_ne_zero (R := F)).mpr <|
    Nat.pos_iff_ne_zero.mp <| Module.finrank_pos (R := F⟮a⟯) (M := K)
-- 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
⊢ 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 K) : F)⁻¹ : 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]
-- 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)
⊢ 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 K : (a : K) → F) a : F) ((↑(Module.finrank F K) : 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)
⊢ 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 K : (a : K) → F) a : F) ((↑(Module.finrank F K) : 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)
⊢ 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) (Module.finrank (↥F⟮a⟯) K) ((trace F ↥F⟮a⟯ : (a : ↥F⟮a⟯) → F) (AdjoinSimple.gen F a) : F) /
    (↑(Module.finrank F 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)
⊢ 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) (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)
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)
⊢ 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) /
    (↑(Module.finrank.{u_1, u_2} F ↥F⟮a⟯ * 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]