awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
⊢ a ∈ E

Tactic:
have ha : 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
m : F
a : K
E : IntermediateField F K := F⟮a⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
ha : a ∈ E
⊢ m • a ∈ E

Tactic:
have hma : m • a ∈ E := smul_mem E ha
-- 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⟯
this : FiniteDimensional.{u_1, u_2} F ↥F⟮a⟯
ha : a ∈ E
hma : m • a ∈ E
a' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) a ha
ma' : ↥E := Subtype.mk (p := fun (x : K) ↦ x ∈ E) (m • a) hma
rw : normalizedTraceAux F K (m • a) = m • normalizedTraceAux F (↥E) a'
rw₁ : normalizedTraceAux F (↥E) ma' = m • normalizedTraceAux F (↥E) a'
rw₂ :
  normalizedTraceAux F (↥E) ma' =
    m • HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) a' : F)
rw₃ :
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) ma' : F) =
    m • HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) a' : F)
rw₄ :
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) ma' : F) =
    HSMul.hSMul (α := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹
      (HSMul.hSMul (β := F) m ((trace F ↥E : (a : ↥E) → F) a' : F))
rw₅ :
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) ma' : F) =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) (m • a') : F)
rw₆ rw₇ :
  HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_1, u_2} F ↥E) : F)⁻¹ ((trace F ↥E : (a : ↥E) → F) ma' : 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) (m • a) ⋯) : F)
⊢ normalizedTraceAux F K (m • a) = m • normalizedTraceAux F K a

Tactic:
rw [normalizedTraceAux_intermediateField F K a',
      normalizedTraceAux_intermediateField F K ma',
      normalizedTraceAux_eq_of_finiteDimensional F a',
      normalizedTraceAux_eq_of_finiteDimensional F ma',
      smul_comm, ← map_smul _ m, SetLike.mk_smul_mk]

Premises used: _private.0.Algebra.normalizedTraceAux_intermediateField, _private.0.Algebra.normalizedTraceAux_eq_of_finiteDimensional, SMulCommClass.smul_comm, SetLike.mk_smul_mk, map_smul
-- 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 : K
⊢ (normalizedTrace F K : (a : K) → F) 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
inst_3 : CharZero F
inst_4 : Algebra.IsIntegral F K
a : K
⊢ (normalizedTrace F K : (a : K) → F) a =
    HSMul.hSMul (α := F) (↑(Polynomial.natDegree (minpoly F a)) : F)⁻¹ (-Polynomial.nextCoeff (minpoly F a))

Tactic:
have ha : IsIntegral F a := IsIntegral.isIntegral a
  IntermediateField.adjoin.finrank ha ▸ trace_adjoinSimpleGen ha ▸ normalizedTrace_def F K a

Premises used: IntermediateField.adjoin.finrank, Algebra.IsIntegral.isIntegral, Eq.rec, Algebra.normalizedTrace_def, trace_adjoinSimpleGen
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
a : F
dsimp : normalizedTraceAux F F a = a
⊢ (normalizedTrace F F : (a : F) → F) a = a

Tactic:
dsimp [normalizedTrace]

Premises used: Algebra.normalizedTrace
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
a : F
rw : HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F F) : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₁ : HSMul.hSMul (α := F) (β := F) (↑1 : F)⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₂ : HSMul.hSMul (α := F) (β := F) 1⁻¹ ((trace F F : (a : F) → F) a : F) = a
rw₃ : HSMul.hSMul (α := F) (β := F) 1 ((trace F F : (a : F) → F) a : F) = a
rw₄ : (trace F F : (a : F) → F) a = a
rw₅ rw₆ : a = a
⊢ normalizedTraceAux F F a = a

Tactic:
rw [normalizedTraceAux_eq_of_finiteDimensional F a, Module.finrank_self F,
    Nat.cast_one, inv_one, one_smul, trace_self_apply]

Premises used: inv_one, Algebra.trace_self_apply, one_smul, _private.0.Algebra.normalizedTraceAux_eq_of_finiteDimensional, Module.finrank_self, Nat.cast_one
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_1
inst : Field F
inst_1 : CharZero F
⊢ Eq (α := F →ₗ[F] F) (normalizedTrace F F) LinearMap.id

Tactic:
LinearMap.ext normalizedTrace_self_apply

Premises used: LinearMap.ext, Algebra.normalizedTrace_self_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
inst_3 : CharZero F
inst_4 : Algebra.IsIntegral F K
inst_5 : FiniteDimensional F K
a : K
⊢ (normalizedTrace F K : (a : K) → F) a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank F K) : F)⁻¹ ((trace F K : (a : K) → F) a : F)

Tactic:
normalizedTraceAux_eq_of_finiteDimensional F a

Premises used: _private.0.Algebra.normalizedTraceAux, _private.0.Algebra.normalizedTraceAux_eq_of_finiteDimensional
-- 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
inst_5 : FiniteDimensional F K
⊢ normalizedTrace F K = HSMul.hSMul (α := F) (β := K →ₗ[F] F) (↑(Module.finrank F K) : F)⁻¹ (trace F K)

Tactic:
LinearMap.ext <| normalizedTrace_eq_of_finiteDimensional_apply F

Premises used: LinearMap.ext, Algebra.normalizedTrace_eq_of_finiteDimensional_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
inst_3 : CharZero F
inst_4 : Algebra.IsIntegral F K
E : Type u_3
inst_5 : Field E
inst_6 : Algebra F E
inst_7 : Algebra.IsIntegral F E
f : E →ₐ[F] K
a : E
⊢ Eq.{u_1 + 1} (α := F) ((normalizedTrace F K : (a : K) → F) ((f : (a : E) → K) a : K) : F)
    ((normalizedTrace F E : (a : E) → F) a : F)

Tactic:
normalizedTraceAux_map F K f a

Premises used: _private.0.Algebra.normalizedTraceAux, _private.0.Algebra.normalizedTraceAux_map
-- 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
E : IntermediateField F K
a : ↥E
⊢ Eq.{u_1 + 1} (α := F) ((normalizedTrace F K : (a : K) → F) (↑a : K) : F) ((normalizedTrace F ↥E : (a : ↥E) → F) a : F)

Tactic:
normalizedTraceAux_intermediateField F K a

Premises used: _private.0.Algebra.normalizedTraceAux_intermediateField, _private.0.Algebra.normalizedTraceAux
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
a : E
⊢ Eq.{u_3 + 1} (α := F) ((normalizedTrace F K : (a : K) → F) ((algebraMap E K : (a : E) → K) a : K) : F)
    ((normalizedTrace F E : (a : E) → F) a : F)

Tactic:
normalizedTrace_map F K (IsScalarTower.toAlgHom F E K) a

Premises used: Algebra.normalizedTrace_map, IsScalarTower.toAlgHom
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
⊢ Eq (α := E →ₗ[F] F)
    (normalizedTrace F K ∘ₗ
      (↑F :
          {S M : Type u_4} →
            {M₂ : Type u_5} →
              [inst : Semiring F] →
                [inst_10 : Semiring S] →
                  [inst_11 : AddCommMonoid M] →
                    [inst_12 : AddCommMonoid M₂] →
                      [inst_13 : Module F M] →
                        [inst_14 : Module F M₂] →
                          [inst_15 : Module S M] →
                            [inst_16 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ F S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[F] M₂)
        (Algebra.linearMap E K))
    (normalizedTrace F E)

Tactic:
LinearMap.ext <| normalizedTrace_algebraMap_apply F E K

Premises used: LinearMap.ext, Algebra.normalizedTrace_algebraMap_apply
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F K
inst_8 : CharZero F
inst_9 : CharZero E
inst_10 : Algebra.IsIntegral E K
a : K
h : Membership.mem (γ := Subsemiring (Polynomial E)) (Polynomial.lifts (algebraMap F E)) (minpoly E a)
⊢ IsIntegral F a

Tactic:
have ha : IsIntegral F a := IsIntegral.isIntegral a
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F K
inst_8 : CharZero F
inst_9 : CharZero E
inst_10 : Algebra.IsIntegral E K
a : K
h : Membership.mem (γ := Subsemiring (Polynomial E)) (Polynomial.lifts (algebraMap F E)) (minpoly E a)
ha : IsIntegral F a
⊢ Eq.{u_4 + 1} (α := E) ((algebraMap F E : (a : F) → E) ((normalizedTrace F K : (a : K) → F) a : F) : E)
    ((normalizedTrace E K : (a : K) → E) a : E)

Tactic:
simp [normalizedTrace_minpoly F a, normalizedTrace_minpoly E a, ← minpoly.map_algebraMap ha h,
    (minpoly F a).nextCoeff_map_eq, map_mul, map_neg]

Premises used: map_neg, minpoly, map_mul, minpoly.map_algebraMap, Polynomial.nextCoeff_map_eq, Algebra.normalizedTrace_minpoly
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
⊢ FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯

Tactic:
have : FiniteDimensional E E⟮a⟯ :=
    IntermediateField.adjoin.finiteDimensional (IsIntegral.isIntegral a)
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
rw :
  (normalizedTrace F K : (a : K) → F) a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_3, u_5} F ↥E⟮a⟯) : F)⁻¹
      ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
⊢ Eq.{u_3 + 1} (α := F) ((normalizedTrace F E : (a : E) → F) ((normalizedTrace E K : (a : K) → E) a : E) : F)
    ((normalizedTrace F K : (a : K) → F) a : F)

Tactic:
rw [normalizedTrace_def E K, inv_natCast_smul_eq (R := E) (S := F), map_smul,
    normalizedTrace_eq_of_finiteDimensional F E, LinearMap.smul_apply, ← smul_assoc,
    smul_eq_mul (a := _⁻¹), ← mul_inv, trace_trace, mul_comm,
    ← Nat.cast_mul, Module.finrank_mul_finrank, eq_comm]

Premises used: Algebra.normalizedTrace_eq_of_finiteDimensional, inv_natCast_smul_eq, smul_assoc, LinearMap.smul_apply, mul_inv, eq_comm, Algebra.trace_trace, Inv.inv, Nat.cast_mul, Module.finrank_mul_finrank, Algebra.normalizedTrace_def, mul_comm, smul_eq_mul, map_smul
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
⊢ FiniteDimensional.{u_3, u_5} F ↥E'

Tactic:
have : FiniteDimensional F E' := Module.Finite.trans E E⟮a⟯
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this_1 : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional.{u_3, u_5} F ↥E'
⊢ Module.finrank.{u_3, u_5} F ↥E⟮a⟯ = Module.finrank.{u_3, u_5} F ↥E'

Tactic:
have h_finrank_eq : Module.finrank F E⟮a⟯ = Module.finrank F E' := rfl
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this_1 : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional.{u_3, u_5} F ↥E'
h_finrank_eq : Module.finrank.{u_3, u_5} F ↥E⟮a⟯ = Module.finrank.{u_3, u_5} F ↥E'
⊢ Eq.{u_3 + 1} (α := F) ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
    ((trace F ↥E' : (a : ↥E') → F) (AdjoinSimple.gen E a) : F)

Tactic:
have h_trace_eq : trace F E⟮a⟯ (AdjoinSimple.gen E a) = trace F E' (AdjoinSimple.gen E a : E') :=
    rfl
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this_1 : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional.{u_3, u_5} F ↥E'
h_finrank_eq : Module.finrank.{u_3, u_5} F ↥E⟮a⟯ = Module.finrank.{u_3, u_5} F ↥E'
h_trace_eq :
  Eq.{u_3 + 1} (α := F) ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
    ((trace F ↥E' : (a : ↥E') → F) (AdjoinSimple.gen E a) : F)
a' : ↥E' := AdjoinSimple.gen E a
rw :
  Eq.{u_3 + 1} (α := F) ((normalizedTrace F K : (a : K) → F) a : F) ((normalizedTrace F K : (a : K) → F) (↑a' : K) : F)
⊢ (normalizedTrace F K : (a : K) → F) a =
    HSMul.hSMul (α := F) (β := F) (↑(Module.finrank.{u_3, u_5} F ↥E⟮a⟯) : F)⁻¹
      ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)

Tactic:
rw [h_finrank_eq, h_trace_eq, ← normalizedTrace_eq_of_finiteDimensional_apply F,
    ← normalizedTrace_intermediateField F K a']

Premises used: Algebra.normalizedTrace_intermediateField, Algebra.normalizedTrace_eq_of_finiteDimensional_apply
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : FiniteDimensional F E
inst_11 : Algebra.IsIntegral E K
inst_12 : CharZero E
a : K
this_1 : FiniteDimensional.{u_4, u_5} E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional.{u_3, u_5} F ↥E'
h_finrank_eq : Module.finrank.{u_3, u_5} F ↥E⟮a⟯ = Module.finrank.{u_3, u_5} F ↥E'
h_trace_eq :
  Eq.{u_3 + 1} (α := F) ((trace F ↥E⟮a⟯ : (a : ↥E⟮a⟯) → F) (AdjoinSimple.gen E a) : F)
    ((trace F ↥E' : (a : ↥E') → F) (AdjoinSimple.gen E a) : F)
a' : ↥E' := AdjoinSimple.gen E a
⊢ Eq.{u_3 + 1} (α := F) ((normalizedTrace F K : (a : K) → F) a : F) ((normalizedTrace F K : (a : K) → F) (↑a' : K) : F)

Tactic:
congr
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : Algebra.IsIntegral E K
inst_11 : CharZero E
a : K
⊢ Eq.{u_3 + 1} (α := F) ((normalizedTrace F E : (a : E) → F) ((normalizedTrace E K : (a : K) → E) a : E) : F)
    ((normalizedTrace F K : (a : K) → F) a : F)

Tactic:
let S : Set E := (minpoly E a).coeffs
  let E₀ := IntermediateField.adjoin F S
  have : FiniteDimensional F E₀ := IntermediateField.finiteDimensional_adjoin
    fun x _ ↦ Algebra.IsIntegral.isIntegral x
  have : Algebra.IsIntegral E₀ E := IsIntegral.tower_top F
  have : Algebra.IsIntegral E₀ K := IsIntegral.trans E
  have hsub : S ⊆ (algebraMap E₀ E).range :=
    Subalgebra.range_algebraMap E₀.toSubalgebra ▸ IntermediateField.subset_adjoin F S
  have hlifts := (Polynomial.lifts_iff_coeffs_subset_range _).mpr hsub
  (normalizedTrace_trans_apply_aux F E₀ K _ ▸
    normalizedTrace_algebraMap_apply F E₀ E _ ▸
    congrArg (normalizedTrace F E) (normalizedTrace_algebraMap_of_lifts E₀ E K a hlifts)).symm

Premises used: Iff.mpr, Algebra.IsIntegral.tower_top, Algebra.IsIntegral.isIntegral, Algebra.IsIntegral.trans, Eq.rec, IntermediateField.subset_adjoin, minpoly, IntermediateField.finiteDimensional_adjoin, SetLike.coe, Polynomial.coeffs, IntermediateField.adjoin, Eq.symm, Subalgebra.range_algebraMap, IntermediateField.toSubalgebra, Polynomial.lifts_iff_coeffs_subset_range
-- Module: Mathlib.FieldTheory.NormalizedTrace
Goal:
F : Type u_3
E : Type u_4
K : Type u_5
inst : Field F
inst_1 : Field E
inst_2 : Field K
inst_3 : Algebra F E
inst_4 : Algebra E K
inst_5 : Algebra F K
inst_6 : IsScalarTower F E K
inst_7 : Algebra.IsIntegral F E
inst_8 : Algebra.IsIntegral F K
inst_9 : CharZero F
inst_10 : Algebra.IsIntegral E K
inst_11 : CharZero E
⊢ Eq (α := K →ₗ[F] F)
    (normalizedTrace F E ∘ₗ
      (↑F :
          {S : Type u_4} →
            {M : Type u_5} →
              {M₂ : Type u_4} →
                [inst : Semiring F] →
                  [inst_12 : Semiring S] →
                    [inst_13 : AddCommMonoid M] →
                      [inst_14 : AddCommMonoid M₂] →
                        [inst_15 : Module F M] →
                          [inst_16 : Module F M₂] →
                            [inst_17 : Module S M] →
                              [inst_18 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ F S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[F] M₂)
        (normalizedTrace E K))
    (normalizedTrace F K)

Tactic:
LinearMap.ext <| normalizedTrace_trans_apply F E K

Premises used: LinearMap.ext, Algebra.normalizedTrace_trans_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
inst_3 : CharZero F
inst_4 : Algebra.IsIntegral F K
a : F
⊢ (normalizedTrace F K : (a : K) → F) ((algebraMap F K : (a : F) → K) a : K) = a

Tactic:
simp
-- 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
⊢ normalizedTrace F K ∘ₗ Algebra.linearMap F K = LinearMap.id

Tactic:
LinearMap.ext <| normalizedTrace_algebraMap_apply_eq_self F K

Premises used: LinearMap.ext, Algebra.normalizedTrace_algebraMap_apply_eq_self
-- 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
E : Type u_3
inst_5 : Field E
inst_6 : Algebra F E
inst_7 : Algebra.IsIntegral F E
f : E →ₐ[F] K
⊢ Eq (α := E →ₗ[F] F)
    (normalizedTrace F K ∘ₗ
      (↑f : [inst_8 : FunLike (E →ₐ[F] K) E K] → [SemilinearMapClass (E →ₐ[F] K) (RingHom.id F) E K] → E →ₗ[F] K))
    (normalizedTrace F E)

Tactic:
LinearMap.ext <| normalizedTrace_map F K f

Premises used: Algebra.normalizedTrace_map, LinearMap.ext
-- 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
⊢ Function.Surjective.{u_2 + 1, u_1 + 1} (α := K) (β := F) (⇑(normalizedTrace F K) : (a : K) → F)

Tactic:
fun a ↦ ⟨algebraMap F K a, normalizedTrace_algebraMap_apply_eq_self F K a⟩

Premises used: Algebra.algebraMap, Algebra.normalizedTrace_algebraMap_apply_eq_self, Exists.intro, DFunLike.coe, Function.Surjective
-- 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
⊢ Ne (α := K →ₗ[F] F) (normalizedTrace F K) 0

Tactic:
let ⟨a, ha⟩ := normalizedTrace_surjective F K 1
  DFunLike.ne_iff.mpr <| ⟨a, ha ▸ one_ne_zero⟩

Premises used: Iff.mpr, Algebra.normalizedTrace_surjective, _private.0.Algebra.normalizedTrace_ne_zero.match_1, Ne, DFunLike.ne_iff, Exists.intro, Algebra.normalizedTrace, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p q : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
inst_2 : PerfectRing M q
⊢ Bijective (β := M) fun (x : M) ↦ HPow.hPow (β := ℕ) x 1

Tactic:
simpa using bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p q : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
inst_2 : PerfectRing M q
simp_rw : Bijective (β := M) fun (x : M) ↦ (x ^ p) ^ q
⊢ Bijective (β := M) fun (x : M) ↦ x ^ (p * q)

Tactic:
simp_rw [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p q : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
inst_2 : PerfectRing M q
⊢ Bijective (β := M) fun (x : M) ↦ (x ^ p) ^ q

Tactic:
PerfectRing.bijective_frobenius.comp PerfectRing.bijective_frobenius

Premises used: PerfectRing.bijective_frobenius, Function.Bijective.comp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p q : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
inst_2 : PerfectRing M q
⊢ Bijective (β := M) fun (x : M) ↦ (x ^ p) ^ q

Tactic:
exact PerfectRing.bijective_frobenius.comp PerfectRing.bijective_frobenius

Premises used: PerfectRing.bijective_frobenius, Function.Bijective.comp
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p q : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
inst_2 : PerfectRing M q
n : ℕ
⊢ PerfectRing M (p ^ n)

Tactic:
n.recOn (inferInstanceAs (PerfectRing M 1)) fun n _ ↦ inferInstanceAs (PerfectRing M (p ^ n * p))

Premises used: Nat.recOn
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
p : ℕ
inst : CommMonoid M
inst_1 : PerfectRing M p
x : M
⊢ HPow.hPow (α := M) ((MulEquiv.symm (powMulEquiv M p) : (a : M) → M) x : M) p = x

Tactic:
(powMulEquiv M p).apply_symm_apply x

Premises used: powMulEquiv, MulEquiv.apply_symm_apply
-- Module: Mathlib.FieldTheory.Perfect
Goal:
M : Type u_1
inst : CommMonoid M
⊢ Eq (α := M ≃* M) (powMulEquiv M 1) (MulEquiv.refl M)

Tactic:
MulEquiv.ext pow_one

Premises used: pow_one, MulEquiv.ext