awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Normal.Defs
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
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₁)
⊢ 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:
apply FaithfulSMul.algebraMap_injective E K₁

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.FieldTheory.Normal.Defs
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
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₁)
⊢ 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:
rw [AlgHom.restrictNormal_commutes]

Premises used: AlgHom.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.Normal.Defs
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₁)
    ((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:
simp
-- Module: Mathlib.FieldTheory.Normal.Defs
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
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)
⊢ Eq (α := Gal(K/F) →* Gal(K/F)) (restrictNormalHom K) (MonoidHom.id Gal(K/F))

Tactic:
ext f x
-- Module: Mathlib.FieldTheory.Normal.Defs
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
h : Eq (α := K) ((f.restrictNormal K : (a : K) → K) x : K) ((f : (a : K) → K) 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:
dsimp only [restrictNormalHom, MonoidHom.mk'_apply, MonoidHom.id_apply]

Premises used: AlgEquiv.restrictNormalHom, MonoidHom.mk'_apply, MonoidHom.id_apply
-- Module: Mathlib.FieldTheory.Normal.Defs
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
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)
⊢ Eq (α := K) ((f.restrictNormal K : (a : K) → K) x : K) ((f : (a : K) → K) x : K)

Tactic:
apply (algebraMap K K).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.Normal.Defs
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
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)
⊢ 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:
rw [AlgEquiv.restrictNormal_commutes]

Premises used: AlgEquiv.restrictNormal_commutes
-- Module: Mathlib.FieldTheory.Normal.Defs
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 : (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:
simp only [Algebra.algebraMap_self, RingHom.id_apply]

Premises used: RingHom.id_apply, Algebra.algebraMap_self
-- Module: Mathlib.FieldTheory.Normal.Defs
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₂
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₁)
⊢ 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₂))

Tactic:
ext f x
-- Module: Mathlib.FieldTheory.Normal.Defs
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₁
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₃)
⊢ 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:
apply (algebraMap K₁ K₃).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.FieldTheory.Normal.Defs
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₁
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₃)
⊢ 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:
rw [IsScalarTower.algebraMap_eq K₁ K₂ K₃]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.FieldTheory.Normal.Defs
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₃)
    (((@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:
simp only [AlgEquiv.restrictNormalHom, MonoidHom.mk'_apply, RingHom.coe_comp, Function.comp_apply,
    ← algebraMap_apply, AlgEquiv.restrictNormal_commutes, MonoidHom.coe_comp]

Premises used: MonoidHom.coe_comp, AlgEquiv.restrictNormalHom, MonoidHom.mk'_apply, AlgEquiv.restrictNormal_commutes, RingHom.coe_comp, Function.comp_apply, IsScalarTower.algebraMap_apply
-- Module: Mathlib.FieldTheory.Normal.Defs
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))
rw₁ 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))
⊢ 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))

Tactic:
rw [IsScalarTower.AlgEquiv.restrictNormalHom_comp F K₁ K₂ K₃, MonoidHom.comp_apply]

Premises used: IsScalarTower.AlgEquiv.restrictNormalHom_comp, MonoidHom.comp_apply
-- 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
a : K
⊢ 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:
rfl

Premises used: _private.0.Algebra.normalizedTraceAux, rfl
-- 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
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 ⋯)
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)
⊢ normalizedTraceAux.{u_1, u_2} F K ((f : (a : E) → K) a : K) = normalizedTraceAux F E a

Tactic:
simp_rw [normalizedTraceAux, ← LinearEquiv.finrank_eq e.toLinearEquiv]

Premises used: LinearEquiv.finrank_eq, _private.0.Algebra.normalizedTraceAux, AlgEquiv.toLinearEquiv
-- 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
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 ⋯)
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)
⊢ 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:
congr
-- 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
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 ⋯)
⊢ 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:
trace_eq_of_algEquiv e <| AdjoinSimple.gen F a

Premises used: Algebra.trace_eq_of_algEquiv, Set.Mem, IntermediateField.AdjoinSimple.gen, setOf
-- 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
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 ⋯)
⊢ 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:
exact trace_eq_of_algEquiv e <| AdjoinSimple.gen F a

Premises used: Algebra.trace_eq_of_algEquiv, IntermediateField.AdjoinSimple.gen
-- 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
E : IntermediateField F K
a : ↥E
⊢ normalizedTraceAux F K (↑a : K) = normalizedTraceAux F (↥E) a

Tactic:
normalizedTraceAux_map F K E.val a

Premises used: _private.0.Algebra.normalizedTraceAux_map, IntermediateField.val
-- 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
⊢ 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)
-- 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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
⊢ FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯

Tactic:
have : FiniteDimensional F F⟮a⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral a)
-- 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 : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
⊢ FiniteDimensional.{u_1, u_2} F ↥F⟮b⟯

Tactic:
have : FiniteDimensional F F⟮b⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral b)
-- 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 : 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⟯
⊢ a ∈ E

Tactic:
have ha : a ∈ E := (le_sup_left : F⟮a⟯ ≤ E) <| mem_adjoin_simple_self F a
-- 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 : 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
⊢ b ∈ E

Tactic:
have hb : b ∈ E := (le_sup_right : F⟮b⟯ ≤ E) <| mem_adjoin_simple_self F b
-- 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 : 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
⊢ a + b ∈ E

Tactic:
have hab : a + b ∈ E := IntermediateField.add_mem E ha hb
-- 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 : 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'
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'
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) +
      HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) b' : F)
rw₅ :
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) ab' : F) =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) a' : F) +
      HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) b' : F)
rw₆ :
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) ab' : F) =
    HSMul.hSMul (α := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹
      (HAdd.hAdd (α := F) (β := F) ((trace F ↥E : (a : ↥E) → F) a' : F) ((trace F ↥E : (a : ↥E) → F) b' : F))
rw₇ :
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) ab' : F) =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) (a' + b') : F)
rw₈ rw₉ :
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) ab' : F) =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹
      ((trace F ↥E : (a : ↥E) → F) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (a + b) ⋯) : F)
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K 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]

Premises used: _private.0.Algebra.normalizedTraceAux_intermediateField, map_add, _private.0.Algebra.normalizedTraceAux_eq_of_finiteDimensional, AddMemClass.mk_add_mk, smul_add
-- 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 : Algebra.IsIntegral F K
m : F
a : K
dsimp : normalizedTraceAux F K (m • a) = m • normalizedTraceAux F K a
⊢ normalizedTraceAux F K (m • a) = HSMul.hSMul (α := F) ((RingHom.id F : (a : F) → F) m : F) (normalizedTraceAux F K a)

Tactic:
dsimp only [AddHom.toFun_eq_coe, AddHom.coe_mk, RingHom.id_apply]

Premises used: RingHom.id_apply, AddHom.toFun_eq_coe, AddHom.coe_mk
-- 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 : Algebra.IsIntegral F K
m : F
a : K
E : IntermediateField F K := F⟮a⟯
⊢ FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯

Tactic:
have : FiniteDimensional F F⟮a⟯ := adjoin.finiteDimensional (IsIntegral.isIntegral a)