awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Norm.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 : Module.Finite K L
x : L
pos : ∀ (hx : x = 0), Eq.{u_4 + 1} (α := K) ((norm K : (a : L) → K) x⁻¹ : K) (((norm K : (a : L) → K) x)⁻¹ : K)
⊢ Eq.{u_4 + 1} (α := K) ((norm K : (a : L) → K) x⁻¹ : K) (((norm K : (a : L) → K) x)⁻¹ : K)
have neg : ∀ (hx : ¬x = 0), Eq.{u_4 + 1} (α := K) ((norm K : (a : L) → K) x⁻¹ : K) (((norm K : (a : L) → K) x)⁻¹ : K)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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
⊢ Eq.{u_4 + 1} (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) (1 : K)
have h : ¬∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)
Tactic: rw [norm_eq_one_of_not_exists_basis]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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
⊢ ¬∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)
have h : ∀ (hx : ∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)), IsIntegral K x
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
hx : ∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)
⊢ IsIntegral K x
have h : ∀ (s : Finset ↥K⟮x⟯) (b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯), IsIntegral K x
Tactic: obtain ⟨s, ⟨b⟩⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
⊢ IsIntegral K x
have h : Submodule.FG.{u_4, u_5} (R := K) (M := L)
  ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (toSubalgebra K⟮x⟯))
Tactic: refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
h :
  Submodule.FG.{u_4, u_5} (R := K) (M := L)
    ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (toSubalgebra K⟮x⟯))
⊢ IsIntegral K x
have h₁ : Membership.mem (γ := Subalgebra K L) (toSubalgebra K⟮x⟯) x
Tactic: refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (hypothesis)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
⊢ (algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) = (aroots (minpoly K x) F).prod
have injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
Tactic: have injKxL := (algebraMap K⟮x⟯ L).injective
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
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)
⊢ (algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) = (aroots (minpoly K x) F).prod
have pos : ∀ (hx : IsIntegral K x),
  (algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) = (aroots (minpoly K x) F).prod
Tactic: by_cases hx : IsIntegral K x
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
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)
pos :
  ∀ (hx : IsIntegral K x),
    (algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) =
      (aroots (minpoly K x) F).prod
⊢ (algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) = (aroots (minpoly K x) F).prod
have neg : ∀ (hx : ¬IsIntegral K x),
  (algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) = (aroots (minpoly K x) F).prod
Tactic: by_cases hx : IsIntegral K x
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
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) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) = (aroots (minpoly K x) F).prod
have pos : (aroots (minpoly K (adjoin.powerBasis hx).gen) F).prod = (aroots (minpoly K x) F).prod
Tactic: rw [← adjoin.powerBasis_gen hx, PowerBasis.norm_gen_eq_prod_roots]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
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).prod = (aroots (minpoly K x) F).prod
⊢ (algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) = (aroots (minpoly K x) F).prod
have pos₁ : Splits (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen))
Tactic: rw [← adjoin.powerBasis_gen hx, PowerBasis.norm_gen_eq_prod_roots]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
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 (adjoin.powerBasis hx).gen) F).prod = (aroots (minpoly K x) F).prod
have pos : (aroots (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L)) F).prod =
  (aroots (minpoly K x) F).prod
Tactic: rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
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 (adjoin.powerBasis hx).gen))
have pos : Splits
  (Polynomial.map (algebraMap K F)
    (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L)))
Tactic: rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
F : Type u_6
inst_3 : Field F
inst_4 : Algebra R F
pb : PowerBasis R S
hE : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ Eq.{u_6 + 1} (α := F) ((algebraMap R F : (a : R) → F) ((norm R : (a : S) → R) pb.gen : R) : F)
    (∏ σ : S →ₐ[R] F, (σ : (a : S) → F) pb.gen : F)
have rw : (aroots (minpoly R pb.gen) F).prod = ∏ σ : S →ₐ[R] F, (σ : (a : S) → F) pb.gen
Tactic: rw [PowerBasis.norm_gen_eq_prod_roots pb hE]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
F : Type u_6
inst_3 : Field F
inst_4 : Algebra R F
pb : PowerBasis R S
hE : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ (aroots (minpoly R pb.gen) F).prod = ∏ σ : S →ₐ[R] F, (σ : (a : S) → F) pb.gen
have rw : (aroots (minpoly R pb.gen) F).prod = ∏ x : { y : F // y ∈ (minpoly R pb.gen).aroots F }, (↑x : F)
Tactic: rw [@Fintype.prod_equiv (S →ₐ[R] F) _ _ (PowerBasis.AlgHom.fintype pb) _ _ pb.liftEquiv'
    (fun σ => σ pb.gen) (fun x => x) ?_]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
F : Type u_6
inst_3 : Field F
inst_4 : Algebra R F
pb : PowerBasis R S
hE : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
rw : (aroots (minpoly R pb.gen) F).prod = ∏ x : { y : F // y ∈ (minpoly R pb.gen).aroots F }, (↑x : F)
⊢ (aroots (minpoly R pb.gen) F).prod = ∏ σ : S →ₐ[R] F, (σ : (a : S) → F) pb.gen
have rw₁ : ∀ (x : S →ₐ[R] F),
  Eq.{u_6 + 1} (α := F) ((fun (σ : S →ₐ[R] F) ↦ ((σ : (a : S) → F) pb.gen : F)) x)
    ((fun (x : { y : F // y ∈ aroots (minpoly R pb.gen) F }) ↦ (↑x : F))
      ((pb.liftEquiv' : (a : S →ₐ[R] F) → { y : F // y ∈ (minpoly R pb.gen).aroots F }) x))
Tactic: rw [@Fintype.prod_equiv (S →ₐ[R] F) _ _ (PowerBasis.AlgHom.fintype pb) _ _ pb.liftEquiv'
    (fun σ => σ pb.gen) (fun x => x) ?_]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
F : Type u_6
inst_3 : Field F
inst_4 : Algebra R F
pb : PowerBasis R S
hE : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
⊢ (aroots (minpoly R pb.gen) F).prod = ∏ x : { y : F // y ∈ (minpoly R pb.gen).aroots F }, (↑x : F)
have rw : (aroots (minpoly R pb.gen) F).Nodup
Tactic: rw [Finset.prod_mem_multiset, Finset.prod_eq_multiset_prod, Multiset.toFinset_val,
      Multiset.dedup_eq_self.mpr, Multiset.map_id]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
F : Type u_6
inst_3 : Field F
inst_4 : Algebra R F
pb : PowerBasis R S
hE : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
rw : (aroots (minpoly R pb.gen) F).Nodup
⊢ (aroots (minpoly R pb.gen) F).prod = ∏ x : { y : F // y ∈ (minpoly R pb.gen).aroots F }, (↑x : F)
have hfg : ∀ (x : { x : F // x ∈ aroots (minpoly R pb.gen) F }), (↑x : F) = _root_.id (↑x : F)
Tactic: rw [Finset.prod_mem_multiset, Finset.prod_eq_multiset_prod, Multiset.toFinset_val,
      Multiset.dedup_eq_self.mpr, Multiset.map_id]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (hypothesis)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
⊢ ∏ σ : F →ₐ[K] E, (σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) =
    HPow.hPow (α := E) (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen) (finrank L F)
have this : FiniteDimensional L F
Tactic: haveI : FiniteDimensional L F := FiniteDimensional.right K L F
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (hypothesis)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional 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) =
    HPow.hPow (α := E) (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen) (finrank L F)
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.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional 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) =
    HPow.hPow (α := E) (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen) (finrank L F)
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, HPow.hPow (α := E) ((x : (a : L) → E) pb.gen : E) (finrank L F))
Tactic: rw [Fintype.prod_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,
    ← Finset.univ_sigma_univ, Finset.prod_sigma, ← Finset.prod_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional 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, HPow.hPow (α := E) ((x : (a : L) → E) pb.gen : E) (finrank L F))
⊢ ∏ σ : F →ₐ[K] E, (σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) =
    HPow.hPow (α := E) (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen) (finrank L F)
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.prod_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,
    ← Finset.univ_sigma_univ, Finset.prod_sigma, ← Finset.prod_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional 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, HPow.hPow (α := E) ((x : (a : L) → E) pb.gen : E) (finrank L F))
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 =
      HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (finrank L F)
Tactic: refine Finset.prod_congr rfl fun σ _ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional 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 =
    HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (finrank L F)
have simp_rw : HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (Finset.card (α := F →ₐ[L] E) Finset.univ) =
  HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (finrank L F)
Tactic: simp_rw [Finset.prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional 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
⊢ HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (Finset.card (α := F →ₐ[L] E) Finset.univ) =
    HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (finrank L F)
have e_a : Finset.card (α := F →ₐ[L] E) Finset.univ = finrank L F
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : T) → R) ((e : (a : S) → T) x : T) : R) ((norm R : (a : S) → R) x : R)
have simp_rw : Eq.{u_1 + 1} (α := R)
  (((LinearMap.det.{u_3, u_1} (M := T) (A := R) : MonoidHom.{u_3, u_1} (T →ₗ[R] T) R) : (a : T →ₗ[R] T) → R)
      ((lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) : End R T) :
    R)
  (((LinearMap.det.{u_3, u_1} (M := T) (A := R) : MonoidHom.{u_3, u_1} (T →ₗ[R] T) R) : (a : T →ₗ[R] T) → R)
      ((↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S)) :
    R)
Tactic: simp_rw [Algebra.norm_apply, ← LinearMap.det_conj _ e.toLinearEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det.{u_3, u_1} (M := T) (A := R) : MonoidHom.{u_3, u_1} (T →ₗ[R] T) R) : (a : T →ₗ[R] T) → R)
        ((lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) : End R T) :
      R)
    (((LinearMap.det.{u_3, u_1} (M := T) (A := R) : MonoidHom.{u_3, u_1} (T →ₗ[R] T) R) : (a : T →ₗ[R] T) → R)
        ((↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S)) :
      R)
have h : (lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) =
  (↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
x : S
⊢ (lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) =
    (↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S)
have h : ∀ (x_1 : T),
  Eq (α := T) ((((lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) : End R T) : (a : T) → T) x_1 : T)
    (((↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S) :
          (a : T) → T)
        x_1 :
      T)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring 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_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
have pos : ∀ (h : ∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
  Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
Tactic: by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring 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_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
have neg : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
  Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
Tactic: by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring 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_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
have pos : ∀ (s : Finset C) (b : Basis (↥s) B C),
  Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
Tactic: obtain ⟨s, ⟨b⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring 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_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
have pos : Eq.{u_9 + 1} (α := B)
  (det.{u_9, u_10} (n := ↥s)
    ((e.mapMatrix : (a : Matrix (↥s) (↥s) A) → Matrix (↥s) (↥s) B)
      ((leftMulMatrix (b.mapCoeffs e.symm sorry) : (a : C) → Matrix (↥s) (↥s) A) x)))
  (det.{u_9, u_10} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x))
Tactic: rw [Algebra.norm_eq_matrix_det b,
      Algebra.norm_eq_matrix_det (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he])),
      e.map_det]