awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
| x
have rw : ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L)
Tactic: rw [← AdjoinSimple.algebraMap_gen K x]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ (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)
have 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)
Tactic: conv in x => rw [← AdjoinSimple.algebraMap_gen K x]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ (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)
have 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)
Tactic: rw [trace_algebraMap, LinearMap.map_smul_of_tower]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: rw [trace_algebraMap, LinearMap.map_smul_of_tower]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ (Algebra.trace K L : (a : L) → K) x = (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x)
have 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)
Tactic: rw [trace_eq_trace_adjoin, trace_adjoinSimpleGen (.of_finite K x), Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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))
⊢ (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
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ (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
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ (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
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ (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
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ (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
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ (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
have rw₅ : finrank (↥K⟮x⟯) L • (aroots (minpoly K x) F).sum = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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.{u_1, u_5} R (A := L) ((trace L F : (a : F) → L) x : L)
have hx' : IsIntegral L x
Tactic: have hx' : IsIntegral L x := hx.tower_top
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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.{u_1, u_5} R (A := L) ((trace L F : (a : F) → L) x : L)
have rw : IsIntegral R
  (HSMul.hSMul (β := AlgebraicClosure F) (finrank (↥L⟮x⟯) F) (Multiset.sum (aroots (minpoly L x) (AlgebraicClosure F))))
Tactic: rw [← isIntegral_algebraMap_iff (algebraMap L (AlgebraicClosure F)).injective, trace_eq_sum_roots]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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))))
⊢ IsIntegral.{u_1, u_5} R (A := L) ((trace L F : (a : F) → L) x : L)
have rw₁ : Splits.{u_6} (R := AlgebraicClosure F) (Polynomial.map (algebraMap L (AlgebraicClosure F)) (minpoly L x))
Tactic: rw [← isIntegral_algebraMap_iff (algebraMap L (AlgebraicClosure F)).injective, trace_eq_sum_roots]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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))))
have refine : ∀ (x_1 : AlgebraicClosure F),
  Membership.mem (γ := Multiset (AlgebraicClosure F)) (aroots (minpoly L x) (AlgebraicClosure F)) x_1 → IsIntegral R x_1
Tactic: refine (IsIntegral.multiset_sum ?_).nsmul _
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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
⊢ IsIntegral R y
have hy₁ : eval₂ (algebraMap L (AlgebraicClosure F)) y (minpoly L x) = 0
Tactic: rw [mem_roots_map (minpoly.ne_zero hx')] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ IsIntegral R y
have right : eval₂ (algebraMap R (AlgebraicClosure F)) y (minpoly R x) = 0
Tactic: use minpoly R x, minpoly.monic hx
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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
⊢ eval₂ (algebraMap R (AlgebraicClosure F)) y (minpoly R x) = 0
have hy₁ : 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 ⊢
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [Algebra.trace_apply, ← LinearMap.trace_conj' _ e.toLinearEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ 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)
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ 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)
have 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)
Tactic: by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨s, ⟨b⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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 := ⋯
⊢ 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)
have pos : Eq.{u_8 + 1} (α := B)
  ((e : (a : A) → B)
      (Matrix.trace.{u_9, u_7} (n := ↥s) ((leftMulMatrix (b.mapCoeffs e.symm sorry) : (a : C) → Matrix (↥s) (↥s) A) x)) :
    B)
  (Matrix.trace.{u_9, u_8} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x) : B)
Tactic: rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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 := ⋯
⊢ Eq.{u_8 + 1} (α := B)
    ((e : (a : A) → B)
        (Matrix.trace.{u_9, u_7} (n := ↥s) ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x)) :
      B)
    (Matrix.trace.{u_9, u_8} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x) : B)
have pos : Eq.{u_8 + 1} (α := B)
  (Matrix.trace.{u_9, u_8} (n := ↥s)
    (Matrix.map.{u_7, u_8, u_9, u_9} (α := A) ((leftMulMatrix (b.mapCoeffs e.symm sorry) : (a : C) → Matrix (↥s) (↥s) A) x)
      (⇑e : (a : A) → B)))
  (Matrix.trace.{u_9, u_8} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x))
Tactic: rw [AddMonoidHom.map_trace]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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 := ⋯
⊢ Eq.{u_8 + 1} (α := B)
    (Matrix.trace.{u_9, u_8} (n := ↥s)
      (Matrix.map.{u_7, u_8, u_9, u_9} (α := A)
        ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x) (⇑e : (a : A) → B)))
    (Matrix.trace.{u_9, u_8} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x))
have pos : Eq (α := Matrix.{u_9, u_9, u_8} (↥s) (↥s) B)
  (Matrix.map.{u_7, u_8, u_9, u_9} (α := A) ((leftMulMatrix (b.mapCoeffs e.symm sorry) : (a : C) → Matrix (↥s) (↥s) A) x)
    (⇑e : (a : A) → B))
  ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x)
Tactic: congr