awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : ¬IsIntegral K x
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum

Tactic:
simp [minpoly.eq_zero hx, trace_gen_eq_zero hx, aroots_def]

Premises used: IntermediateField.AdjoinSimple.trace_gen_eq_zero, minpoly.eq_zero, Polynomial.aroots_def
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
pos : (aroots (minpoly K (adjoin.powerBasis hx).gen) F).sum = (aroots (minpoly K x) F).sum
pos₁ : Splits (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen))
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum

Tactic:
rw [← adjoin.powerBasis_gen hx, (adjoin.powerBasis hx).trace_gen_eq_sum_roots]

Premises used: IntermediateField.adjoin.powerBasis_gen, PowerBasis.trace_gen_eq_sum_roots, IntermediateField.adjoin.powerBasis
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
pos :
  (aroots (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x) : L)) F).sum =
    (aroots (minpoly K x) F).sum
⊢ (aroots (minpoly K (adjoin.powerBasis hx).gen) F).sum = (aroots (minpoly K x) F).sum

Tactic:
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]

Premises used: IntermediateField.adjoin.powerBasis_gen, minpoly.algebraMap_eq
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
pos :
  Splits (Polynomial.map (algebraMap K F) (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x) : L)))
⊢ Splits (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen))

Tactic:
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]

Premises used: IntermediateField.adjoin.powerBasis_gen, minpoly.algebraMap_eq
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
⊢ (aroots (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x) : L)) F).sum =
    (aroots (minpoly K x) F).sum

Tactic:
simp only [AdjoinSimple.algebraMap_gen _ _]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
⊢ (aroots (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x) : L)) F).sum =
    (aroots (minpoly K x) F).sum

Tactic:
try simp only [AdjoinSimple.algebraMap_gen _ _]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
pos : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
⊢ Splits (Polynomial.map (algebraMap K F) (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x) : L)))

Tactic:
simp only [AdjoinSimple.algebraMap_gen _ _]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
pos : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
⊢ Splits (Polynomial.map (algebraMap K F) (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x) : L)))

Tactic:
try simp only [AdjoinSimple.algebraMap_gen _ _]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
⊢ Splits (Polynomial.map (algebraMap K F) (minpoly K x))

Tactic:
hf
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
⊢ Splits (Polynomial.map (algebraMap K F) (minpoly K x))

Tactic:
exact hf
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
x : L
rw :
  (Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) ((Algebra.trace (↥K⟮x⟯) L : (a : L) → ↥K⟮x⟯) x : ↥K⟮x⟯) =
    HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)
⊢ (Algebra.trace K L : (a : L) → K) x =
    HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)

Tactic:
rw [← trace_trace (S := K⟮x⟯)]

Premises used: Algebra.trace_trace
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
x : L
rw : ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L)
| x

Tactic:
rw [← AdjoinSimple.algebraMap_gen K x]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
x : L
conv :
  (Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K)
      ((Algebra.trace (↥K⟮x⟯) L : (a : L) → ↥K⟮x⟯) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x)) :
        ↥K⟮x⟯) =
    HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)
⊢ (Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) ((Algebra.trace (↥K⟮x⟯) L : (a : L) → ↥K⟮x⟯) x : ↥K⟮x⟯) =
    HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)

Tactic:
conv in x => rw [← AdjoinSimple.algebraMap_gen K x]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
x : L
rw :
  (Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (HSMul.hSMul (β := ↥K⟮x⟯) (finrank (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) =
    HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)
rw₁ rw₂ :
  HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) =
    HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)
⊢ (Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K)
      ((Algebra.trace (↥K⟮x⟯) L : (a : L) → ↥K⟮x⟯) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x)) :
        ↥K⟮x⟯) =
    HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)

Tactic:
rw [trace_algebraMap, LinearMap.map_smul_of_tower]

Premises used: Algebra.trace_algebraMap, LinearMap.map_smul_of_tower
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : IsIntegral K x
⊢ (Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) = -nextCoeff (minpoly K x)

Tactic:
simpa [minpoly_gen K x] using PowerBasis.trace_gen_eq_nextCoeff_minpoly <| adjoin.powerBasis hx

Premises used: IntermediateField.minpoly_gen, PowerBasis.trace_gen_eq_nextCoeff_minpoly, IntermediateField.adjoin.powerBasis
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
x : L
rw :
  HMul.hMul (α := K) ((algebraMap ℕ K : (a : ℕ) → K) (finrank (↥K⟮x⟯) L) : K) (-nextCoeff (minpoly K x)) =
    (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x)
⊢ (Algebra.trace K L : (a : L) → K) x = (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x)

Tactic:
rw [trace_eq_trace_adjoin, trace_adjoinSimpleGen (.of_finite K x), Algebra.smul_def]

Premises used: trace_eq_trace_adjoin, Algebra.smul_def, IsIntegral.of_finite, trace_adjoinSimpleGen
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
x : L
⊢ HMul.hMul (α := K) ((algebraMap ℕ K : (a : ℕ) → K) (finrank (↥K⟮x⟯) L) : K) (-nextCoeff (minpoly K x)) =
    (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
inst_5 : FiniteDimensional K L
x : L
hF : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
rw :
  (algebraMap K F : (a : K) → F)
      (HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L)
        ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)) =
    finrank (↥K⟮x⟯) L • (aroots (minpoly K x) F).sum
rw₁ :
  (algebraMap K F : (a : K) → F)
      (HMul.hMul (α := K) (β := K) ((algebraMap ℕ K : (a : ℕ) → K) (finrank (↥K⟮x⟯) L) : K)
        ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)) =
    finrank (↥K⟮x⟯) L • (aroots (minpoly K x) F).sum
rw₂ :
  HMul.hMul (α := F) (β := F)
      ((algebraMap K F : (a : K) → F) ((algebraMap ℕ K : (a : ℕ) → K) (finrank (↥K⟮x⟯) L) : K) : F)
      ((algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) : F) =
    finrank (↥K⟮x⟯) L • (aroots (minpoly K x) F).sum
rw₃ :
  HSMul.hSMul (α := K) (β := F) ((algebraMap ℕ K : (a : ℕ) → K) (finrank (↥K⟮x⟯) L) : K)
      ((algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) : F) =
    finrank (↥K⟮x⟯) L • (aroots (minpoly K x) F).sum
rw₄ :
  HSMul.hSMul (α := K) ((algebraMap ℕ K : (a : ℕ) → K) (finrank (↥K⟮x⟯) L) : K) (aroots (minpoly K x) F).sum =
    finrank (↥K⟮x⟯) L • (aroots (minpoly K x) F).sum
rw₅ rw₆ : finrank (↥K⟮x⟯) L • (aroots (minpoly K x) F).sum = finrank (↥K⟮x⟯) L • (aroots (minpoly K x) F).sum
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K L : (a : L) → K) x : K) =
    finrank (↥K⟮x⟯) L • (aroots (minpoly K x) F).sum

Tactic:
rw [trace_eq_trace_adjoin K x, Algebra.smul_def, map_mul, ← Algebra.smul_def,
    IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots _ hF, IsScalarTower.algebraMap_smul]

Premises used: IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots, trace_eq_trace_adjoin, IsScalarTower.algebraMap_smul, map_mul, Algebra.smul_def
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
⊢ IsIntegral L x

Tactic:
have hx' : IsIntegral L x := hx.tower_top
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
rw :
  IsIntegral R
    (HSMul.hSMul (β := AlgebraicClosure F) (finrank (↥L⟮x⟯) F)
      (Multiset.sum (aroots (minpoly L x) (AlgebraicClosure F))))
rw₁ : Splits.{u_6} (R := AlgebraicClosure F) (Polynomial.map (algebraMap L (AlgebraicClosure F)) (minpoly L x))
⊢ IsIntegral.{u_1, u_5} R (A := L) ((trace L F : (a : F) → L) x : L)

Tactic:
rw [← isIntegral_algebraMap_iff (algebraMap L (AlgebraicClosure F)).injective, trace_eq_sum_roots]

Premises used: Algebra.algebraMap, trace_eq_sum_roots, RingHom.injective, isIntegral_algebraMap_iff, AlgebraicClosure
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ IsIntegral R
    (HSMul.hSMul (β := AlgebraicClosure F) (finrank (↥L⟮x⟯) F)
      (Multiset.sum (aroots (minpoly L x) (AlgebraicClosure F))))

Tactic:
(IsIntegral.multiset_sum ?_).nsmul _

Premises used: IsIntegral.multiset_sum, IsIntegral.nsmul
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
refine :
  ∀ (x_1 : AlgebraicClosure F),
    Membership.mem (γ := Multiset (AlgebraicClosure F)) (aroots (minpoly L x) (AlgebraicClosure F)) x_1 →
      IsIntegral R x_1
⊢ IsIntegral R
    (HSMul.hSMul (β := AlgebraicClosure F) (finrank (↥L⟮x⟯) F)
      (Multiset.sum (aroots (minpoly L x) (AlgebraicClosure F))))

Tactic:
refine (IsIntegral.multiset_sum ?_).nsmul _

Premises used: IsIntegral.multiset_sum, IsIntegral.nsmul
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy : Membership.mem (γ := Multiset (AlgebraicClosure F)) (aroots (minpoly L x) (AlgebraicClosure F)) y
⊢ eval₂ (algebraMap L (AlgebraicClosure F)) y (minpoly L x) = 0

Tactic:
rw [mem_roots_map (minpoly.ne_zero hx')] at hy

Premises used: Polynomial.mem_roots_map, minpoly.ne_zero
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy : eval₂ (algebraMap L (AlgebraicClosure F)) y (minpoly L x) = 0
right : eval₂ (algebraMap R (AlgebraicClosure F)) y (minpoly R x) = 0
⊢ IsIntegral R y

Tactic:
use minpoly R x, minpoly.monic hx

Premises used: minpoly.monic, minpoly
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy : eval₂ (algebraMap L (AlgebraicClosure F)) y (minpoly L x) = 0
⊢ Eq.{u_6 + 1} (α := AlgebraicClosure F)
    ((aeval y : (a : L[X]) → AlgebraicClosure F) (minpoly L x) : AlgebraicClosure F) (0 : AlgebraicClosure F)

Tactic:
rw [← aeval_def] at hy ⊢

Premises used: Polynomial.aeval_def
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy :
  Eq.{u_6 + 1} (α := AlgebraicClosure F)
    ((aeval y : (a : L[X]) → AlgebraicClosure F) (minpoly L x) : AlgebraicClosure F) (0 : AlgebraicClosure F)
⊢ Eq.{u_6 + 1} (α := AlgebraicClosure F)
    ((aeval y : (a : R[X]) → AlgebraicClosure F) (minpoly R x) : AlgebraicClosure F) (0 : AlgebraicClosure F)

Tactic:
minpoly.aeval_of_isScalarTower R x y hy

Premises used: minpoly.aeval_of_isScalarTower
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
y : AlgebraicClosure F
hy :
  Eq.{u_6 + 1} (α := AlgebraicClosure F)
    ((aeval y : (a : L[X]) → AlgebraicClosure F) (minpoly L x) : AlgebraicClosure F) (0 : AlgebraicClosure F)
⊢ Eq.{u_6 + 1} (α := AlgebraicClosure F)
    ((aeval y : (a : R[X]) → AlgebraicClosure F) (minpoly R x) : AlgebraicClosure F) (0 : AlgebraicClosure F)

Tactic:
exact minpoly.aeval_of_isScalarTower R x y hy

Premises used: minpoly.aeval_of_isScalarTower
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_1
inst : CommRing R
L : Type u_5
inst_1 : Field L
F : Type u_6
inst_2 : Field F
inst_3 : Algebra R L
inst_4 : Algebra L F
inst_5 : Algebra R F
inst_6 : IsScalarTower R L F
inst_7 : FiniteDimensional L F
x : F
hx : IsIntegral R x
hx' : IsIntegral L x
⊢ Splits.{u_6} (R := AlgebraicClosure F) (Polynomial.map (algebraMap L (AlgebraicClosure F)) (minpoly L x))

Tactic:
apply IsAlgClosed.splits

Premises used: IsAlgClosed.splits
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A B
inst_4 : Algebra A C
e : B ≃ₐ[A] C
x : B
simp_rw :
  Eq.{u_7 + 1} (α := A)
    ((LinearMap.trace A C : (a : C →ₗ[A] C) → A) ((lmul A C : (a : C) → End A C) ((e : (a : B) → C) x : C) : End A C) :
      A)
    ((LinearMap.trace A C : (a : C →ₗ[A] C) → A)
        (((↑e : B ≃ₗ[A] C).conj : (a : End A B) → End A C) ((lmul A B : (a : B) → End A B) x) : End A C) :
      A)
⊢ Eq.{u_7 + 1} (α := A) ((trace A C : (a : C) → A) ((e : (a : B) → C) x : C) : A) ((trace A B : (a : B) → A) x : A)

Tactic:
simp_rw [Algebra.trace_apply, ← LinearMap.trace_conj' _ e.toLinearEquiv]

Premises used: LinearMap.trace_conj', AlgEquiv.toLinearEquiv, Algebra.trace_apply
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A B
inst_4 : Algebra A C
e : B ≃ₐ[A] C
x : B
h :
  Eq (α := C →ₗ[A] C) ((lmul A C : (a : C) → End A C) ((e : (a : B) → C) x : C) : End A C)
    (((↑e : B ≃ₗ[A] C).conj : (a : End A B) → End A C) ((lmul A B : (a : B) → End A B) x) : End A C)
⊢ Eq.{u_7 + 1} (α := A)
    ((LinearMap.trace A C : (a : C →ₗ[A] C) → A) ((lmul A C : (a : C) → End A C) ((e : (a : B) → C) x : C) : End A C) :
      A)
    ((LinearMap.trace A C : (a : C →ₗ[A] C) → A)
        (((↑e : B ≃ₗ[A] C).conj : (a : End A B) → End A C) ((lmul A B : (a : B) → End A B) x) : End A C) :
      A)

Tactic:
congr
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A B
inst_4 : Algebra A C
e : B ≃ₐ[A] C
x : B
h :
  ∀ (x_1 : C),
    Eq (α := C) ((((lmul A C : (a : C) → End A C) ((e : (a : B) → C) x : C) : End A C) : (a : C) → C) x_1 : C)
      (((((↑e : B ≃ₗ[A] C).conj : (a : End A B) → End A C) ((lmul A B : (a : B) → End A B) x) : End A C) : (a : C) → C)
          x_1 :
        C)
⊢ Eq (α := C →ₗ[A] C) ((lmul A C : (a : C) → End A C) ((e : (a : B) → C) x : C) : End A C)
    (((↑e : B ≃ₗ[A] C).conj : (a : End A B) → End A C) ((lmul A B : (a : B) → End A B) x) : End A C)

Tactic:
ext
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A B
inst_4 : Algebra A C
e : B ≃ₐ[A] C
x : B
x_1 : C
⊢ Eq (α := C) ((((lmul A C : (a : C) → End A C) ((e : (a : B) → C) x : C) : End A C) : (a : C) → C) x_1 : C)
    (((((↑e : B ≃ₗ[A] C).conj : (a : End A B) → End A C) ((lmul A B : (a : B) → End A B) x) : End A C) : (a : C) → C)
        x_1 :
      C)

Tactic:
simp
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
pos :
  ∀ (h : ∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
    Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)
neg :
  ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
    Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)
⊢ Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)

Tactic:
by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)

Premises used: Finset
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
h : ∃ (s : Finset C), Nonempty (Basis (↥s) B C)
pos :
  ∀ (s : Finset C) (b : Basis (↥s) B C),
    Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)
⊢ Eq.{u_8 + 1} (α := B) ((e : (a : A) → B) ((trace A C : (a : C) → A) x : A) : B) ((trace B C : (a : C) → B) x : B)

Tactic:
obtain ⟨s, ⟨b⟩⟩ := h
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
A : Type u_7
B : Type u_8
C : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
⊢ ∀ (c : B) (x : C), HSMul.hSMul.{u_7, u_9, u_9} (α := A) ((e.symm : (a : B) → A) c : A) x = c • x

Tactic:
simp [Algebra.smul_def, ← he]

Premises used: Algebra.smul_def