awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
y : AlgebraicClosure ↥F
hy : Membership.mem (γ := Multiset (AlgebraicClosure ↥F)) (aroots (minpoly K x) (AlgebraicClosure ↥F)) y
pos :
  ∀ (P : K[X]) (hP : Polynomial.map (algebraMap R K) (minpoly R x) = minpoly K x * P),
    Eq.{u_6 + 1} (α := AlgebraicClosure ↥F)
      ((aeval y : (a : K[X]) → AlgebraicClosure ↥F) (Polynomial.map (algebraMap R K) (minpoly R x)) :
        AlgebraicClosure ↥F)
      (0 : AlgebraicClosure ↥F)
⊢ Eq.{u_6 + 1} (α := AlgebraicClosure ↥F)
    ((aeval y : (a : K[X]) → AlgebraicClosure ↥F) (Polynomial.map (algebraMap R K) (minpoly R x)) : AlgebraicClosure ↥F)
    (0 : AlgebraicClosure ↥F)

Tactic:
obtain ⟨P, hP⟩ := minpoly.dvd K x (show aeval x ((minpoly R x).map (algebraMap R K)) = 0 by simp)

Premises used: minpoly.dvd
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
y : AlgebraicClosure ↥F
hy : Membership.mem (γ := Multiset (AlgebraicClosure ↥F)) (aroots (minpoly K x) (AlgebraicClosure ↥F)) y
P : K[X]
hP : Polynomial.map (algebraMap R K) (minpoly R x) = minpoly K x * P
⊢ Eq.{u_6 + 1} (α := AlgebraicClosure ↥F)
    ((aeval y : (a : K[X]) → AlgebraicClosure ↥F) (Polynomial.map (algebraMap R K) (minpoly R x)) : AlgebraicClosure ↥F)
    (0 : AlgebraicClosure ↥F)

Tactic:
simp [hP, aeval_mul, (mem_aroots'.mp hy).2]

Premises used: Polynomial.mem_aroots', Polynomial.aeval_mul, And.right, Iff.mp
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
L : Type u_6
K : Type u_7
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
pos :
  ∀ (h : FiniteDimensional K L),
    (norm K : (a : L) → K) x = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
neg :
  ∀ (h : ¬FiniteDimensional K L),
    (norm K : (a : L) → K) x = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
⊢ (norm K : (a : L) → K) x = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)

Tactic:
by_cases h : FiniteDimensional K L

Premises used: FiniteDimensional
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
neg : 1 = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
⊢ (norm K : (a : L) → K) x = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)

Tactic:
rw [norm_eq_one_of_not_module_finite h]

Premises used: Algebra.norm_eq_one_of_not_module_finite
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
pos : ∀ (hx : IsIntegral K x), 1 = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
neg : ∀ (hx : ¬IsIntegral K x), 1 = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
⊢ 1 = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)

Tactic:
by_cases hx : IsIntegral K x

Premises used: IsIntegral
-- Module: Mathlib.RingTheory.Norm.Transitivity
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 : FiniteDimensional (↥K⟮x⟯) L
⊢ FiniteDimensional.{u_7, u_6} K ↥K⟮x⟯

Tactic:
have : FiniteDimensional K K⟮x⟯ := adjoin.finiteDimensional hx
-- Module: Mathlib.RingTheory.Norm.Transitivity
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 : FiniteDimensional (↥K⟮x⟯) L
this : FiniteDimensional.{u_7, u_6} K ↥K⟮x⟯
⊢ FiniteDimensional K L

Tactic:
Finite.trans K⟮x⟯ L

Premises used: Membership.mem, Subtype, Module.Finite.trans, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.RingTheory.Norm.Transitivity
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 : FiniteDimensional (↥K⟮x⟯) L
this : FiniteDimensional.{u_7, u_6} K ↥K⟮x⟯
⊢ FiniteDimensional K L

Tactic:
exact Finite.trans K⟮x⟯ L

Premises used: Membership.mem, Subtype, Module.Finite.trans, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
⊢ ¬FiniteDimensional (↥K⟮x⟯) L

Tactic:
have h₁ : ¬ FiniteDimensional K⟮x⟯ L := fun H ↦ h <| by
        have : FiniteDimensional K K⟮x⟯ := adjoin.finiteDimensional hx
        exact Finite.trans K⟮x⟯ L
-- Module: Mathlib.RingTheory.Norm.Transitivity
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₁ : ¬FiniteDimensional (↥K⟮x⟯) L
⊢ 1 = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)

Tactic:
simp [finrank_of_not_finite h₁]

Premises used: Module.finrank_of_not_finite
-- Module: Mathlib.RingTheory.Norm.Transitivity
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)
neg₁ : ¬Module.Finite.{u_7, u_6} K ↥K⟮x⟯
⊢ 1 = HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)

Tactic:
rw [norm_eq_one_of_not_module_finite]

Premises used: Algebra.norm_eq_one_of_not_module_finite
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
⊢ 1 = HPow.hPow (α := K) 1 (finrank (↥K⟮x⟯) L)

Tactic:
simp
-- Module: Mathlib.RingTheory.Norm.Transitivity
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⟯

Tactic:
fun H ↦ hx ?_

Premises used: Not
-- Module: Mathlib.RingTheory.Norm.Transitivity
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 : ∀ (H : Module.Finite.{u_7, u_6} K ↥K⟮x⟯), IsIntegral K x
⊢ ¬Module.Finite.{u_7, u_6} K ↥K⟮x⟯

Tactic:
refine fun H ↦ hx ?_
-- Module: Mathlib.RingTheory.Norm.Transitivity
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⟯
neg : IsIntegral K (A := ↥K⟮x⟯) (gen K x)
⊢ IsIntegral K x

Tactic:
rw [← isIntegral_gen]

Premises used: IntermediateField.AdjoinSimple.isIntegral_gen
-- Module: Mathlib.RingTheory.Norm.Transitivity
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 (A := ↥K⟮x⟯) (gen K x)

Tactic:
IsIntegral.isIntegral (gen K x)

Premises used: Algebra.IsIntegral.isIntegral, IntermediateField.AdjoinSimple.gen
-- Module: Mathlib.RingTheory.Norm.Transitivity
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 (A := ↥K⟮x⟯) (gen K x)

Tactic:
exact IsIntegral.isIntegral (gen K x)

Premises used: Algebra.IsIntegral.isIntegral, IntermediateField.AdjoinSimple.gen
-- Module: Mathlib.RingTheory.Norm.Transitivity
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 : L) → K) (↑(gen K x) : L) =
    HPow.hPow (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (gen K x) : K) (finrank (↥K⟮x⟯) L)
⊢ (norm K : (a : L) → K) x = 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]

Premises used: IntermediateField.AdjoinSimple.coe_gen
-- Module: Mathlib.RingTheory.Norm.Transitivity
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)
pos₄ 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))
⊢ (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:
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]

Premises used: Algebra.norm_algebraMap_of_basis, IntermediateField.AdjoinSimple.gen, Membership.mem, Subtype, map_pow, IntermediateField.algebraMap_apply, Module.finrank_eq_card_chooseBasisIndex, Algebra.norm_norm, Module.Free.chooseBasis
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
rw₂ rw₃ : (aroots (minpoly K x) F).prod ^ 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

Tactic:
rw [norm_eq_norm_adjoin K x, map_pow, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots _ hF]

Premises used: map_pow, Algebra.norm_eq_norm_adjoin, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
⊢ IsIntegral K x

Tactic:
have hx := Algebra.IsSeparable.isIntegral K x
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
rw₁ : IsSeparable K (adjoin.powerBasis hx).gen
⊢ 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)

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 _)]

Premises used: IntermediateField.adjoin.powerBasis_gen, map_pow, Algebra.norm_eq_norm_adjoin, IsAlgClosed.splits, IntermediateField.adjoin.powerBasis, Algebra.norm_eq_prod_embeddings_gen
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
⊢ 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:
(prod_embeddings_eq_finrank_pow L (L := K⟮x⟯) E (adjoin.powerBasis hx)).symm

Premises used: Set.Mem, IntermediateField.adjoin, IntermediateField.adjoin.powerBasis, Eq.symm, Algebra.prod_embeddings_eq_finrank_pow
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
⊢ 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:
exact (prod_embeddings_eq_finrank_pow L (L := K⟮x⟯) E (adjoin.powerBasis hx)).symm

Premises used: IntermediateField.adjoin.powerBasis, Eq.symm, Algebra.prod_embeddings_eq_finrank_pow
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
⊢ Algebra.IsSeparable.{u_7, u_6} K ↥K⟮x⟯

Tactic:
haveI := Algebra.isSeparable_tower_bot_of_isSeparable K K⟮x⟯ L
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
this : Algebra.IsSeparable.{u_7, u_6} K ↥K⟮x⟯
⊢ IsSeparable K (adjoin.powerBasis hx).gen

Tactic:
Algebra.IsSeparable.isSeparable K _

Premises used: Algebra.IsSeparable.isSeparable
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
this : Algebra.IsSeparable.{u_7, u_6} K ↥K⟮x⟯
⊢ IsSeparable K (adjoin.powerBasis hx).gen

Tactic:
exact Algebra.IsSeparable.isSeparable K _

Premises used: Algebra.IsSeparable.isSeparable
-- Module: Mathlib.RingTheory.Norm.Transitivity
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 L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) (∏ σ : Gal(L/K), (σ : (a : L) → L) x) :
      AlgebraicClosure 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)

Tactic:
apply FaithfulSMul.algebraMap_injective L (AlgebraicClosure L)

Premises used: FaithfulSMul.algebraMap_injective, AlgebraicClosure
-- Module: Mathlib.RingTheory.Norm.Transitivity
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 : Gal(L/K), (algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) ((x_1 : (a : L) → 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)
    ((algebraMap L (AlgebraicClosure L) : (a : L) → AlgebraicClosure L) (∏ σ : Gal(L/K), (σ : (a : L) → L) x) :
      AlgebraicClosure L)

Tactic:
rw [map_prod (algebraMap L (AlgebraicClosure L))]

Premises used: Algebra.algebraMap, map_prod, AlgebraicClosure
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
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)
⊢ 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 [← Fintype.prod_equiv (Normal.algHomEquivAut K (AlgebraicClosure L) L)]

Premises used: Normal.algHomEquivAut, Fintype.prod_equiv, AlgebraicClosure
-- Module: Mathlib.RingTheory.Norm.Transitivity
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)
a₁ 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)
⊢ 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 [← norm_eq_prod_embeddings _ _ x, ← IsScalarTower.algebraMap_apply]

Premises used: Algebra.norm_eq_prod_embeddings, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Norm.Transitivity
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
σ : L →ₐ[K] AlgebraicClosure L
⊢ Eq (α := AlgebraicClosure L) ((σ : (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)) σ :
              Gal(L/K)) :
            (a : L) → L)
          x) :
      AlgebraicClosure L)

Tactic:
simp only [Normal.algHomEquivAut, AlgHom.restrictNormal', Equiv.coe_fn_mk,
      AlgEquiv.coe_ofBijective, AlgHom.restrictNormal_commutes, algebraMap_self, RingHom.id_apply]

Premises used: Normal.algHomEquivAut, RingHom.id_apply, Algebra.algebraMap_self, AlgEquiv.coe_ofBijective, Equiv.coe_fn_mk, AlgHom.restrictNormal', AlgHom.restrictNormal_commutes
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin n
P : ↥R[X]_n
⊢ Module.Finite R ↥R[X]_n

Tactic:
.of_basis <| basis ..

Premises used: Polynomial.degreeLT.basis, Module.Finite.of_basis
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
i : Fin n
P : ↥R[X]_n
⊢ Free R ↥R[X]_n

Tactic:
.of_basis <| basis ..

Premises used: Polynomial.degreeLT.basis, Module.Free.of_basis
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
i : Fin n
P : ↥R[X]_n
⊢ (((Basis.repr (basis R n) : (a : ↥R[X]_n) → Fin n →₀ R) P : Fin n →₀ R) : (a : Fin n) → R) i =
    (↑P : R[X]).coeff (↑i : ℕ)

Tactic:
rfl

Premises used: Polynomial.coeff, rfl
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
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])

Tactic:
congr_arg _ (Basis.apply_eq_iff.2 <| Finsupp.ext fun j ↦ ?_)

Premises used: Iff.mpr, Finsupp.ext, congr_arg, Module.Basis.apply_eq_iff
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
i : Fin n
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 : ℕ)) ⋯) :
              Fin n →₀ R) :
            (a : Fin n) → R)
          j :
        R)
      ((Finsupp.single i 1 : (a : Fin n) → R) j : R)
⊢ (↑((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])

Tactic:
refine congr_arg _ (Basis.apply_eq_iff.2 <| Finsupp.ext fun j ↦ ?_)

Premises used: Iff.mpr, Finsupp.ext, congr_arg, Module.Basis.apply_eq_iff
-- Module: Mathlib.RingTheory.Polynomial.DegreeLT
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
i 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 : ℕ)) ⋯) :
            Fin n →₀ R) :
          (a : Fin n) → R)
        j :
      R)
    ((Finsupp.single i 1 : (a : Fin n) → R) j : R)

Tactic:
simp only [basis_repr, coeff_X_pow, eq_comm, Finsupp.single_apply, Fin.ext_iff]

Premises used: Fin.ext_iff, Polynomial.coeff_X_pow, eq_comm, Finsupp.single_apply, Polynomial.degreeLT.basis_repr