awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
neg : 1 = HPow.hPow (α := K) 1 (finrank (↥K⟮x⟯) L)
⊢ 1 = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
have neg₁ : ¬Module.Finite.{u_7, u_6} K ↥K⟮x⟯
Tactic: rw [norm_eq_one_of_not_module_finite]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
⊢ ¬Module.Finite.{u_7, u_6} K ↥K⟮x⟯
have neg : ∀ (H : Module.Finite.{u_7, u_6} K ↥K⟮x⟯), IsIntegral K x
Tactic: refine fun H ↦ hx ?_
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : ¬FiniteDimensional K L
hx : ¬IsIntegral K x
H : Module.Finite.{u_7, u_6} K ↥K⟮x⟯
⊢ IsIntegral K x
have neg : IsIntegral K (A := ↥K⟮x⟯) (gen K x)
Tactic: rw [← isIntegral_gen]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K : (a : L) → K) x = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
have pos : (norm K : (a : L) → K) (↑(gen K x) : L) =
  HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
Tactic: nth_rw 1 [← coe_gen K x]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K : (a : L) → K) (↑(gen K x) : L) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
have pos : (norm K : (a : ↥F) → K) ((norm ↥F : (a : L) → ↥F) (↑(gen K x) : L) : ↥F) =
  HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
Tactic: rw [← norm_norm (S := F), ← IntermediateField.algebraMap_apply,
    norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow,
    finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
pos :
  (norm K : (a : ↥F) → K) ((norm ↥F : (a : L) → ↥F) (↑(gen K x) : L) : ↥F) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
⊢ (norm K : (a : L) → K) (↑(gen K x) : L) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
have pos₁ : (norm K : (a : ↥F) → K) ((norm ↥F : (a : L) → ↥F) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x)) : ↥F) =
  HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
Tactic: rw [← norm_norm (S := F), ← IntermediateField.algebraMap_apply,
    norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow,
    finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
pos :
  (norm K : (a : ↥F) → K) ((norm ↥F : (a : L) → ↥F) (↑(gen K x) : L) : ↥F) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
pos₁ :
  (norm K : (a : ↥F) → K) ((norm ↥F : (a : L) → ↥F) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x)) : ↥F) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
⊢ (norm K : (a : L) → K) (↑(gen K x) : L) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
have pos₂ : (norm K : (a : ↥F) → K) (HPow.hPow (α := ↥F) (gen K x) (Fintype.card.{u_6} (Free.ChooseBasisIndex (↥F) L))) =
  HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
Tactic: rw [← norm_norm (S := F), ← IntermediateField.algebraMap_apply,
    norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow,
    finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
pos :
  (norm K : (a : ↥F) → K) ((norm ↥F : (a : L) → ↥F) (↑(gen K x) : L) : ↥F) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
pos₁ :
  (norm K : (a : ↥F) → K) ((norm ↥F : (a : L) → ↥F) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x)) : ↥F) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
pos₂ :
  (norm K : (a : ↥F) → K) (HPow.hPow (α := ↥F) (gen K x) (Fintype.card.{u_6} (Free.ChooseBasisIndex (↥F) L))) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
⊢ (norm K : (a : L) → K) (↑(gen K x) : L) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
have pos₃ : HPow.hPow (α := K) ((norm K : (a : ↥F) → K) (gen K x) : K) (Fintype.card.{u_6} (Free.ChooseBasisIndex (↥F) L)) =
  HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
Tactic: rw [← norm_norm (S := F), ← IntermediateField.algebraMap_apply,
    norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow,
    finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
pos :
  (norm K : (a : ↥F) → K) ((norm ↥F : (a : L) → ↥F) (↑(gen K x) : L) : ↥F) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
pos₁ :
  (norm K : (a : ↥F) → K) ((norm ↥F : (a : L) → ↥F) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x)) : ↥F) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
pos₂ :
  (norm K : (a : ↥F) → K) (HPow.hPow (α := ↥F) (gen K x) (Fintype.card.{u_6} (Free.ChooseBasisIndex (↥F) L))) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
pos₃ :
  HPow.hPow (α := K) ((norm K : (a : ↥F) → K) (gen K x) : K) (Fintype.card.{u_6} (Free.ChooseBasisIndex (↥F) L)) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
⊢ (norm K : (a : L) → K) (↑(gen K x) : L) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
have pos₄ : HPow.hPow (α := K) ((norm K : (a : ↥F) → K) (gen K x) : K) (Fintype.card.{u_6} (Free.ChooseBasisIndex (↥F) L)) =
  HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (Fintype.card.{u_6} (Free.ChooseBasisIndex (↥K⟮x⟯) L))
Tactic: rw [← norm_norm (S := F), ← IntermediateField.algebraMap_apply,
    norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow,
    finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_8
inst_3 : Field F
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 : L) → K) x : K) = (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L
have rw : (algebraMap K F : (a : K) → F) (HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)) =
  (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L
Tactic: rw [norm_eq_norm_adjoin K x, map_pow, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots _ hF]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_8
inst_3 : Field F
inst_4 : Algebra K F
x : L
hF : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
rw :
  (algebraMap K F : (a : K) → F) (HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)) =
    (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L
⊢ (algebraMap K F : (a : K) → F) ((norm K : (a : L) → K) x : K) = (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L
have rw₁ : HPow.hPow (α := F) ((algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) : F) (finrank (↥K⟮x⟯) L) =
  (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L
Tactic: rw [norm_eq_norm_adjoin K x, map_pow, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots _ hF]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F : Type u_8
inst_3 : Field F
inst_4 : Algebra K F
x : L
hF : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
rw :
  (algebraMap K F : (a : K) → F) (HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)) =
    (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L
rw₁ :
  HPow.hPow (α := F) ((algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) : F)
      (finrank (↥K⟮x⟯) L) =
    (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L
⊢ (algebraMap K F : (a : K) → F) ((norm K : (a : L) → K) x : K) = (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L
have rw₂ : (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L = (aroots (minpoly K x) F).prod ^ finrank (↥K⟮x⟯) L
Tactic: rw [norm_eq_norm_adjoin K x, map_pow, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots _ hF]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (hypothesis)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_9
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : FiniteDimensional K L
inst_6 : Algebra.IsSeparable K L
inst_7 : IsAlgClosed E
x : L
⊢ Eq.{u_9 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((norm K : (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
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_9
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : FiniteDimensional K L
inst_6 : Algebra.IsSeparable K L
inst_7 : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ Eq.{u_9 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((norm K : (a : L) → K) x : K) : E)
    (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) x : E)
have rw : HPow.hPow (α := E) (∏ σ : ↥K⟮x⟯ →ₐ[K] E, (σ : (a : ↥K⟮x⟯) → E) (adjoin.powerBasis hx).gen) (finrank (↥K⟮x⟯) L) =
  ∏ σ : L →ₐ[K] E, (σ : (a : L) → E) x
Tactic: rw [norm_eq_norm_adjoin K x, map_pow, ← adjoin.powerBasis_gen hx,
    norm_eq_prod_embeddings_gen E (adjoin.powerBasis hx) (IsAlgClosed.splits _)]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_9
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : FiniteDimensional K L
inst_6 : Algebra.IsSeparable K L
inst_7 : IsAlgClosed E
x : L
hx : IsIntegral K x
rw :
  HPow.hPow (α := E) (∏ σ : ↥K⟮x⟯ →ₐ[K] E, (σ : (a : ↥K⟮x⟯) → E) (adjoin.powerBasis hx).gen) (finrank (↥K⟮x⟯) L) =
    ∏ σ : L →ₐ[K] E, (σ : (a : L) → E) x
⊢ Eq.{u_9 + 1} (α := E) ((algebraMap K E : (a : K) → E) ((norm K : (a : L) → K) x : K) : E)
    (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) x : E)
have rw₁ : IsSeparable K (adjoin.powerBasis hx).gen
Tactic: rw [norm_eq_norm_adjoin K x, map_pow, ← adjoin.powerBasis_gen hx,
    norm_eq_prod_embeddings_gen E (adjoin.powerBasis hx) (IsAlgClosed.splits _)]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (hypothesis)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E : Type u_9
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : FiniteDimensional K L
inst_6 : Algebra.IsSeparable K L
inst_7 : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ IsSeparable K (adjoin.powerBasis hx).gen
have this : Algebra.IsSeparable.{u_7, u_6} K ↥K⟮x⟯
Tactic: haveI := Algebra.isSeparable_tower_bot_of_isSeparable K K⟮x⟯ L
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : L
⊢ Eq.{u_6 + 1} (α := L) ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K) : L)
    (∏ σ : Gal(L/K), (σ : (a : L) → L) x : L)
have a : Eq (α := AlgebraicClosure L)
  ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
      ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
    AlgebraicClosure L)
  ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) (∏ σ : Gal(L/K), (σ : (a : L) → L) x) :
    AlgebraicClosure L)
Tactic: apply FaithfulSMul.algebraMap_injective L (AlgebraicClosure L)
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : L
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) (∏ σ : Gal(L/K), (σ : (a : L) → L) x) :
      AlgebraicClosure L)
have a : Eq (α := AlgebraicClosure L)
  ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
      ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
    AlgebraicClosure L)
  (∏ x_1 : Gal(L/K), (algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) ((x_1 : (a : L) → L) x) :
    AlgebraicClosure L)
Tactic: rw [map_prod (algebraMap L (AlgebraicClosure L))]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : L
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∏ x_1 : Gal(L/K), (algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) ((x_1 : (a : L) → L) x) :
      AlgebraicClosure L)
have a : Eq (α := AlgebraicClosure L)
  ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
      ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
    AlgebraicClosure L)
  (∏ x_1 : L →ₐ[K] AlgebraicClosure L, (x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
Tactic: rw [← Fintype.prod_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : L
a :
  Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∏ x_1 : L →ₐ[K] AlgebraicClosure L, (x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∏ x_1 : Gal(L/K), (algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) ((x_1 : (a : L) → L) x) :
      AlgebraicClosure L)
have a₁ : (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L
Tactic: rw [← Fintype.prod_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : L
a :
  Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∏ x_1 : L →ₐ[K] AlgebraicClosure L, (x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
a₁ : (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∏ x_1 : Gal(L/K), (algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) ((x_1 : (a : L) → L) x) :
      AlgebraicClosure L)
have a₂ : ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
  Eq (α := AlgebraicClosure L) ((x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((((Normal.algHomEquivAut K (AlgebraicClosure L) L : (a : L →ₐ[K] AlgebraicClosure L) → Gal(L/K)) x_1 :
              Gal(L/K)) :
            (a : L) → L)
          x) :
      AlgebraicClosure L)
Tactic: rw [← Fintype.prod_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : L
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∏ x_1 : L →ₐ[K] AlgebraicClosure L, (x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
have a : Eq (α := AlgebraicClosure L)
  ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
      ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
    AlgebraicClosure L)
  ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L) ((norm K : (a : L) → K) x) : AlgebraicClosure L)
Tactic: rw [← norm_eq_prod_embeddings _ _ x, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Transitivity (goal)
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : IsGalois K L
x : L
a :
  Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L) ((norm K : (a : L) → K) x) : AlgebraicClosure L)
⊢ Eq (α := AlgebraicClosure L)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L)
        ((algebraMap K L : (a : K) → L) ((norm K : (a : L) → K) x : K)) :
      AlgebraicClosure L)
    (∏ x_1 : L →ₐ[K] AlgebraicClosure L, (x_1 : (a : L) → AlgebraicClosure L) x : AlgebraicClosure L)
have a₁ : Eq.{u_6 + 1} (α := AlgebraicClosure L)
  ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L) ((norm K : (a : L) → K) x) : AlgebraicClosure L)
  ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L) ((norm K : (a : L) → K) x) : AlgebraicClosure L)
Tactic: rw [← norm_eq_prod_embeddings _ _ x, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
i : Fin n
⊢ (↑((basis R n : (a : Fin n) → ↥R[X]_n) i) : R[X]) =
    (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x)
          (HPow.hPow (α := R[X]) X (↑i : ℕ)) ⋯) :
      R[X])
have refine : ∀ (j : Fin n),
  Eq (α := R)
    ((((Basis.repr (basis R n) : (a : ↥R[X]_n) → Fin n →₀ R)
              (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submodule R R[X]) (R[X]_n) x)
                (HPow.hPow (α := R[X]) X (↑i : ℕ)) sorry) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        j :
      R)
    ((Finsupp.single i 1 : (a : Fin n) → R) j : R)
Tactic: refine congr_arg _ (Basis.apply_eq_iff.2 <| Finsupp.ext fun j ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin m
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n) (Fin.castAdd n i) : ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
have rw : Eq (α := ↥R[X]_m × ↥R[X]_n)
  ((Basis.reindex (Basis.prod (basis R m) (basis R n)) finSumFinEquiv : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n)
      (Fin.castAdd n i) :
    ↥R[X]_m × ↥R[X]_n)
  (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply,
    Sum.elim_inl, LinearMap.coe_inl, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin m
rw :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.reindex (Basis.prod (basis R m) (basis R n)) finSumFinEquiv : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n)
        (Fin.castAdd n i) :
      ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n) (Fin.castAdd n i) : ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
have rw₁ : Eq (α := ↥R[X]_m × ↥R[X]_n)
  ((Basis.prod (basis R m) (basis R n) : (a : Fin m ⊕ Fin n) → ↥R[X]_m × ↥R[X]_n)
      ((Equiv.symm finSumFinEquiv : (a : Fin (m + n)) → Fin m ⊕ Fin n) (Fin.castAdd n i) : Fin m ⊕ Fin n) :
    ↥R[X]_m × ↥R[X]_n)
  (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply,
    Sum.elim_inl, LinearMap.coe_inl, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.DegreeLT (goal)
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin m
rw :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.reindex (Basis.prod (basis R m) (basis R n)) finSumFinEquiv : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n)
        (Fin.castAdd n i) :
      ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
rw₁ :
  Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((Basis.prod (basis R m) (basis R n) : (a : Fin m ⊕ Fin n) → ↥R[X]_m × ↥R[X]_n)
        ((Equiv.symm finSumFinEquiv : (a : Fin (m + n)) → Fin m ⊕ Fin n) (Fin.castAdd n i) : Fin m ⊕ Fin n) :
      ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
⊢ Eq (α := ↥R[X]_m × ↥R[X]_n)
    ((basisProd R m n : (a : Fin (m + n)) → ↥R[X]_m × ↥R[X]_n) (Fin.castAdd n i) : ↥R[X]_m × ↥R[X]_n)
    (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
have rw₂ : Eq (α := ↥R[X]_m × ↥R[X]_n)
  ((Basis.prod (basis R m) (basis R n) : (a : Fin m ⊕ Fin n) → ↥R[X]_m × ↥R[X]_n) (Sum.inl i) : ↥R[X]_m × ↥R[X]_n)
  (((basis R m : (a : Fin m) → ↥R[X]_m) i, 0) : ↥R[X]_m × ↥R[X]_n)
Tactic: rw [basisProd, Basis.reindex_apply, finSumFinEquiv_symm_apply_castAdd, Basis.prod_apply,
    Sum.elim_inl, LinearMap.coe_inl, Function.comp_apply]