awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α := 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 ⋯) : (a : C) → Matrix (↥s) (↥s) A) x)
      (⇑e : (a : A) → B))
    ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x)
have pos : ∀ (i j : ↥s),
  Eq.{u_8 + 1} (α := 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) i j :
      B)
    ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x i j : B)
Tactic: ext i j
-- 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 neg : ¬∃ (s : Finset C), Nonempty (Basis (↥s) A C)
Tactic: rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]
-- 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: classical
  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
  · obtain ⟨s, ⟨b⟩⟩ := h
    letI : Algebra A B := RingHom.toAlgebra e
    letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
    rw [AddMonoidHom.map_trace]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
  rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]
  intro ⟨s, ⟨b⟩⟩
  exact h ⟨s, ⟨b.mapCoeffs e (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
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: classical
  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
  · obtain ⟨s, ⟨b⟩⟩ := h
    letI : Algebra A B := RingHom.toAlgebra e
    letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
    rw [AddMonoidHom.map_trace]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
  rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]
  intro ⟨s, ⟨b⟩⟩
  exact h ⟨s, ⟨b.mapCoeffs e (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
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 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)
have neg₂ : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)), ¬∃ (s : Finset C), Nonempty (Basis (↥s) A C)
Tactic: classical
  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
  · obtain ⟨s, ⟨b⟩⟩ := h
    letI : Algebra A B := RingHom.toAlgebra e
    letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
    rw [AddMonoidHom.map_trace]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
  rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]
  intro ⟨s, ⟨b⟩⟩
  exact h ⟨s, ⟨b.mapCoeffs e (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
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 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)
neg₂ : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)), ¬∃ (s : Finset C), Nonempty (Basis (↥s) A 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 neg₃ : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)) (s : Finset C) (b : Basis (↥s) A C), False
Tactic: classical
  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
  · obtain ⟨s, ⟨b⟩⟩ := h
    letI : Algebra A B := RingHom.toAlgebra e
    letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
    rw [AddMonoidHom.map_trace]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
  rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]
  intro ⟨s, ⟨b⟩⟩
  exact h ⟨s, ⟨b.mapCoeffs e (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
A₂ : Type u_9
B₂ : Type u_10
inst : CommRing A₁
inst_1 : CommRing B₁
inst_2 : CommRing A₂
inst_3 : CommRing B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
x : B₁
this : Algebra A₁ B₂ :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Eq.{u_7 + 1} (α := A₁) ((trace A₁ B₁ : (a : B₁) → A₁) x : A₁)
    ((e₁.symm : (a : A₂) → A₁) ((trace A₂ B₂ : (a : B₂) → A₂) ((e₂ : (a : B₁) → B₂) x : B₂) : A₂) : A₁)
have rw : Eq.{u_7 + 1} (α := A₁) ((trace A₁ B₂ : (a : B₂) → A₁) ((e' : (a : B₁) → B₂) x : B₂) : A₁)
  ((trace A₁ B₂ : (a : B₂) → A₁) ((e₂ : (a : B₁) → B₂) x : B₂) : A₁)
Tactic: rw [← Algebra.trace_eq_of_ringEquiv e₁ he, ← Algebra.trace_eq_of_algEquiv e',
    RingEquiv.symm_apply_apply]
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ Eq.{u_7 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((Algebra.trace K L : (a : L) → K) pb.gen : K) : E)
    (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen : E)
have rw : (aroots (minpoly K pb.gen) E).Nodup
Tactic: rw [pb.trace_gen_eq_sum_roots hE, Fintype.sum_equiv pb.liftEquiv', Finset.sum_mem_multiset,
    Finset.sum_eq_multiset_sum, Multiset.toFinset_val, Multiset.dedup_eq_self.mpr _,
    Multiset.map_id]
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
rw : (aroots (minpoly K pb.gen) E).Nodup
⊢ Eq.{u_7 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((Algebra.trace K L : (a : L) → K) pb.gen : K) : E)
    (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen : E)
have f : { x : E // x ∈ aroots (minpoly K pb.gen) E } → E
Tactic: rw [pb.trace_gen_eq_sum_roots hE, Fintype.sum_equiv pb.liftEquiv', Finset.sum_mem_multiset,
    Finset.sum_eq_multiset_sum, Multiset.toFinset_val, Multiset.dedup_eq_self.mpr _,
    Multiset.map_id]
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
rw : (aroots (minpoly K pb.gen) E).Nodup
f : { x : E // x ∈ aroots (minpoly K pb.gen) E } → E
⊢ Eq.{u_7 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((Algebra.trace K L : (a : L) → K) pb.gen : K) : E)
    (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen : E)
have hfg : ∀ (x : { x : E // x ∈ aroots (minpoly K pb.gen) E }), _root_.id (↑x : E) = _root_.id (↑x : E)
Tactic: rw [pb.trace_gen_eq_sum_roots hE, Fintype.sum_equiv pb.liftEquiv', Finset.sum_mem_multiset,
    Finset.sum_eq_multiset_sum, Multiset.toFinset_val, Multiset.dedup_eq_self.mpr _,
    Multiset.map_id]
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
rw : (aroots (minpoly K pb.gen) E).Nodup
f : { x : E // x ∈ aroots (minpoly K pb.gen) E } → E
hfg : ∀ (x : { x : E // x ∈ aroots (minpoly K pb.gen) E }), _root_.id (↑x : E) = _root_.id (↑x : E)
⊢ Eq.{u_7 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((Algebra.trace K L : (a : L) → K) pb.gen : K) : E)
    (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen : E)
have h : ∀ (x : L →ₐ[K] E),
  Eq.{u_7 + 1} (α := E) ((x : (a : L) → E) pb.gen : E)
    (_root_.id (↑((pb.liftEquiv' : (a : L →ₐ[K] E) → { y : E // y ∈ (minpoly K pb.gen).aroots E }) x) : E) : E)
Tactic: rw [pb.trace_gen_eq_sum_roots hE, Fintype.sum_equiv pb.liftEquiv', Finset.sum_mem_multiset,
    Finset.sum_eq_multiset_sum, Multiset.toFinset_val, Multiset.dedup_eq_self.mpr _,
    Multiset.map_id]
-- 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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
⊢ Eq.{u_7 + 1} (α := E) ((σ : (a : L) → E) pb.gen : E)
    (_root_.id (↑((pb.liftEquiv' : (a : L →ₐ[K] E) → { y : E // y ∈ (minpoly K pb.gen).aroots E }) σ) : E) : E)
have h : Eq.{u_7 + 1} (α := E) ((σ : (a : L) → E) pb.gen : E) (_root_.id ((σ : (a : L) → E) pb.gen) : E)
Tactic: rw [PowerBasis.liftEquiv'_apply_coe, id_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
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
pb : PowerBasis K L
hE : Splits (Polynomial.map (algebraMap K E) (minpoly K pb.gen))
hfx : IsSeparable K pb.gen
this_1 : DecidableEq E := Classical.decEq E
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Eq.{u_7 + 1} (α := E) ((σ : (a : L) → E) pb.gen : E) (_root_.id ((σ : (a : L) → E) pb.gen) : E)
⊢ Eq.{u_7 + 1} (α := E) ((σ : (a : L) → E) pb.gen : E)
    (_root_.id (↑((pb.liftEquiv' : (a : L →ₐ[K] E) → { y : E // y ∈ (minpoly K pb.gen).aroots E }) σ) : E) : E)
have h₁ : Eq.{u_7 + 1} (α := E) ((σ : (a : L) → E) pb.gen : E) ((σ : (a : L) → E) pb.gen : E)
Tactic: rw [PowerBasis.liftEquiv'_apply_coe, id_def]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
⊢ ∑ σ : F →ₐ[K] E, (σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) =
    HSMul.hSMul (β := E) (finrank L F) (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen)
have this : FiniteDimensional L F
Tactic: haveI : FiniteDimensional L F := FiniteDimensional.right K L F
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this : FiniteDimensional L F
⊢ ∑ σ : F →ₐ[K] E, (σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) =
    HSMul.hSMul (β := E) (finrank L F) (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen)
have this₁ : Algebra.IsSeparable L F
Tactic: haveI : Algebra.IsSeparable L F := Algebra.isSeparable_tower_top_of_isSeparable K L F
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ ∑ σ : F →ₐ[K] E, (σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) =
    HSMul.hSMul (β := E) (finrank L F) (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen)
have rw : Eq.{u_7 + 1} (α := E)
  (∑ a : L →ₐ[K] E,
    ∑ s : F →ₐ[L] E,
      (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) a s) :
          (a : L) → E)
        pb.gen)
  (∑ x : L →ₐ[K] E, HSMul.hSMul (β := E) (finrank L F) ((x : (a : L) → E) pb.gen : E))
Tactic: rw [Fintype.sum_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,
    ← Finset.univ_sigma_univ, Finset.sum_sigma, ← Finset.sum_nsmul]
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
rw :
  Eq.{u_7 + 1} (α := E)
    (∑ a : L →ₐ[K] E,
      ∑ s : F →ₐ[L] E,
        (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) a s) :
            (a : L) → E)
          pb.gen)
    (∑ x : L →ₐ[K] E, HSMul.hSMul (β := E) (finrank L F) ((x : (a : L) → E) pb.gen : E))
⊢ ∑ σ : F →ₐ[K] E, (σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) =
    HSMul.hSMul (β := E) (finrank L F) (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen)
have rw₁ : ∀ (x : F →ₐ[K] E),
  Eq.{u_7 + 1} (α := E) ((x : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) : E)
    ((Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E)
            ((algHomEquivSigma : (a : F →ₐ[K] E) → (f : L →ₐ[K] E) × (F →ₐ[L] E)) x) :
          (a : L) → E)
        pb.gen :
      E)
Tactic: rw [Fintype.sum_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,
    ← Finset.univ_sigma_univ, Finset.sum_sigma, ← Finset.sum_nsmul]
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ Eq.{u_7 + 1} (α := E)
    (∑ a : L →ₐ[K] E,
      ∑ s : F →ₐ[L] E,
        (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) a s) :
            (a : L) → E)
          pb.gen)
    (∑ x : L →ₐ[K] E, HSMul.hSMul (β := E) (finrank L F) ((x : (a : L) → E) pb.gen : E))
have refine : ∀ (σ : L →ₐ[K] E),
  Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ →
    ∑ s : F →ₐ[L] E,
        (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) σ s) :
            (a : L) → E)
          pb.gen =
      HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
Tactic: refine Finset.sum_congr rfl fun σ _ => ?_
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this_3 : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ
this : Algebra L E := σ.toAlgebra
⊢ ∑ s : F →ₐ[L] E,
      (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) σ s) :
          (a : L) → E)
        pb.gen =
    HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
have simp_rw : ∑ x : F →ₐ[L] E, (σ : (a : L) → E) pb.gen = HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
Tactic: simp_rw [Finset.sum_const, Finset.card_univ, ← AlgHom.card L F E]
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this_3 : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ
this : Algebra L E := σ.toAlgebra
simp_rw simp_rw₁ :
  ∑ x : F →ₐ[L] E, (σ : (a : L) → E) pb.gen = HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
⊢ ∑ s : F →ₐ[L] E,
      (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) σ s) :
          (a : L) → E)
        pb.gen =
    HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
have simp_rw₂ : HSMul.hSMul (β := E) (Finset.card (α := F →ₐ[L] E) Finset.univ) ((σ : (a : L) → E) pb.gen : E) =
  HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
Tactic: simp_rw [Finset.sum_const, Finset.card_univ, ← AlgHom.card L F E]
-- 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 L F
inst_5 : Algebra K F
inst_6 : IsScalarTower K L F
E : Type u_7
inst_7 : Field E
inst_8 : Algebra K E
inst_9 : IsAlgClosed E
inst_10 : FiniteDimensional K F
inst_11 : Algebra.IsSeparable K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this_3 : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ
this : Algebra L E := σ.toAlgebra
simp_rw simp_rw₁ :
  ∑ x : F →ₐ[L] E, (σ : (a : L) → E) pb.gen = HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
simp_rw₂ :
  HSMul.hSMul (β := E) (Finset.card (α := F →ₐ[L] E) Finset.univ) ((σ : (a : L) → E) pb.gen : E) =
    HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
⊢ ∑ s : F →ₐ[L] E,
      (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) σ s) :
          (a : L) → E)
        pb.gen =
    HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
have simp_rw₃ : HSMul.hSMul (β := E) (Fintype.card (F →ₐ[L] E)) ((σ : (a : L) → E) pb.gen : E) =
  HSMul.hSMul (β := E) (finrank L F) ((σ : (a : L) → E) pb.gen : E)
Tactic: simp_rw [Finset.sum_const, Finset.card_univ, ← AlgHom.card L F E]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_7
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : IsAlgClosed E
inst_6 : FiniteDimensional K L
inst_7 : Algebra.IsSeparable K L
x : L
⊢ Eq.{u_7 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((Algebra.trace K L : (a : L) → K) x : K) : E)
    (∑ σ : L →ₐ[K] E, (σ : (a : L) → E) x : E)
have hx : IsIntegral K x
Tactic: have hx := Algebra.IsSeparable.isIntegral K x