awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
mp :
  ∀ (i : Free.ChooseBasisIndex R S),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
                (x *
                  ∑ i : Free.ChooseBasisIndex R S,
                    HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
            (a : Free.ChooseBasisIndex R S) → R)
          i :
        R)
      (((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R) 0 : (a : Free.ChooseBasisIndex R S) → R) i : R)
mp₁ :
  Ne.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0
⊢ x = 0

Tactic:
refine (mul_eq_zero.mp (b.ext_elem fun i => ?_)).resolve_right (show ∑ i, v i • b i ≠ 0 from ?_)

Premises used: Module.Basis.ext_elem, mul_eq_zero, Iff.mp, Or.resolve_right
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
i : Free.ChooseBasisIndex R S
⊢ Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
              (x *
                ∑ i : Free.ChooseBasisIndex R S,
                  HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
          (a : Free.ChooseBasisIndex R S) → R)
        i :
      R)
    (((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R) 0 : (a : Free.ChooseBasisIndex R S) → R) i : R)

Tactic:
simpa only [map_zero, Pi.zero_apply] using congr_fun hv i

Premises used: Pi.zero_apply, map_zero, congr_fun
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
mp :
  ∀
    (sum_eq :
      Eq.{u_2 + 1} (α := S)
        (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S))
        0),
    v = 0
⊢ Ne.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0

Tactic:
contrapose v_ne with sum_eq
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
sum_eq :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0
mp :
  Eq.{u_2 + 1} (α := S) ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) v : S)
    ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
⊢ v = 0

Tactic:
apply b.equivFun.symm.injective

Premises used: LinearEquiv.symm, LinearEquiv.injective, Module.Basis.equivFun
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
sum_eq :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0
mp :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S) : S)
    ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
mp₁ : Eq.{u_2 + 1} (α := S) (0 : S) ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
mp₂ mp₃ : Eq.{u_2 + 1} (α := S) 0 0
⊢ Eq.{u_2 + 1} (α := S) ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) v : S)
    ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)

Tactic:
rw [b.equivFun_symm_apply, sum_eq, map_zero]

Premises used: Module.Basis.equivFun_symm_apply, map_zero
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
⊢ Ne.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) ↔ x ≠ 0

Tactic:
not_iff_not.mpr norm_eq_zero_iff

Premises used: not_iff_not, Iff.mpr, Algebra.norm_eq_zero_iff
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
⊢ Eq.{u_1 + 1} (α := R)
      (((LinearMap.det.{u_2, u_1} (M := S) (A := R) : MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
          ((mul R S : (a : S) → S →ₗ[R] S) x : S →ₗ[R] S) :
        R)
      (0 : R) ↔
    x = 0

Tactic:
norm_eq_zero_iff

Premises used: Algebra.norm_eq_zero_iff
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Finite ι
inst_4 : IsDomain R
inst_5 : IsDomain S
b : Basis ι R S
x : S
⊢ Free R S

Tactic:
haveI : Module.Free R S := Module.Free.of_basis b
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Finite ι
inst_4 : IsDomain R
inst_5 : IsDomain S
b : Basis ι R S
x : S
this : Free R S
⊢ Module.Finite R S

Tactic:
haveI : Module.Finite R S := Module.Finite.of_basis b
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Finite ι
inst_4 : IsDomain R
inst_5 : IsDomain S
b : Basis ι R S
x : S
this_1 : Free R S
this : Module.Finite R S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) ↔ x = 0

Tactic:
norm_eq_zero_iff

Premises used: Algebra.norm_eq_zero_iff
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Finite ι
inst_4 : IsDomain R
inst_5 : IsDomain S
b : Basis ι R S
x : S
this_1 : Free R S
this : Module.Finite R S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) ↔ x = 0

Tactic:
exact norm_eq_zero_iff

Premises used: Algebra.norm_eq_zero_iff
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Finite ι
inst_4 : IsDomain R
inst_5 : IsDomain S
b : Basis ι R S
x : S
⊢ Ne.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) ↔ x ≠ 0

Tactic:
not_iff_not.mpr (norm_eq_zero_iff_of_basis b)

Premises used: not_iff_not, Iff.mpr, Algebra.norm_eq_zero_iff_of_basis
-- Module: Mathlib.RingTheory.Norm.Basic
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)
neg : ∀ (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)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.Norm.Basic
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
hx : x = 0
⊢ Eq.{u_4 + 1} (α := K) ((norm K : (a : L) → K) x⁻¹ : K) (((norm K : (a : L) → K) x)⁻¹ : K)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Norm.Basic
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
hx : ¬x = 0
⊢ Eq.{u_4 + 1} (α := K)
    ((fun (a : K) ↦ HMul.hMul (β := K) a ((norm K : (a : L) → K) x : K)) ((norm K : (a : L) → K) x⁻¹))
    ((fun (a : K) ↦ HMul.hMul (β := K) a ((norm K : (a : L) → K) x : K)) ((norm K : (a : L) → K) x)⁻¹)

Tactic:
simp [hx, ← map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.Norm.Basic
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
hx : ¬x = 0
⊢ Eq.{u_4 + 1} (α := K) ((norm K : (a : L) → K) x⁻¹ : K) (((norm K : (a : L) → K) x)⁻¹ : K)

Tactic:
exact mul_left_injective₀ (norm_ne_zero_iff.mpr hx) (by simp [hx, ← map_mul])

Premises used: Iff.mpr, mul_left_injective₀, Algebra.norm_ne_zero_iff
-- Module: Mathlib.RingTheory.Norm.Basic
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
h : ¬∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)
⊢ Eq.{u_4 + 1} (α := K) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) (1 : K)

Tactic:
rw [norm_eq_one_of_not_exists_basis]

Premises used: Algebra.norm_eq_one_of_not_exists_basis
-- Module: Mathlib.RingTheory.Norm.Basic
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
h : ∀ (hx : ∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)), IsIntegral K x
⊢ ¬∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)

Tactic:
contrapose hx
-- Module: Mathlib.RingTheory.Norm.Basic
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⟯)
h : ∀ (s : Finset ↥K⟮x⟯) (b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯), IsIntegral K x
⊢ IsIntegral K x

Tactic:
obtain ⟨s, ⟨b⟩⟩ := hx
-- Module: Mathlib.RingTheory.Norm.Basic
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

Tactic:
.of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_

Premises used: IntermediateField.adjoin, IsIntegral.of_mem_of_fg, Singleton.singleton, IntermediateField.toSubalgebra
-- Module: Mathlib.RingTheory.Norm.Basic
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⟯))
h₁ : Membership.mem (γ := Subalgebra K L) (toSubalgebra K⟮x⟯) x
⊢ IsIntegral K x

Tactic:
refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_
-- Module: Mathlib.RingTheory.Norm.Basic
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⟯
⊢ Submodule.FG.{u_4, u_5} (R := K) (M := L)
    ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (toSubalgebra K⟮x⟯))

Tactic:
(Submodule.fg_iff_finiteDimensional _).mpr (b.finiteDimensional_of_finite)

Premises used: Iff.mpr, Module.Basis.finiteDimensional_of_finite, Submodule.fg_iff_finiteDimensional
-- Module: Mathlib.RingTheory.Norm.Basic
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⟯
⊢ Submodule.FG.{u_4, u_5} (R := K) (M := L)
    ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (toSubalgebra K⟮x⟯))

Tactic:
exact (Submodule.fg_iff_finiteDimensional _).mpr (b.finiteDimensional_of_finite)

Premises used: Iff.mpr, Submodule.fg_iff_finiteDimensional
-- Module: Mathlib.RingTheory.Norm.Basic
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⟯
⊢ Membership.mem (γ := Subalgebra K L) (toSubalgebra K⟮x⟯) x

Tactic:
IntermediateField.subset_adjoin K _ (Set.mem_singleton x)

Premises used: Set.mem_singleton, Set.Mem, IntermediateField.subset_adjoin
-- Module: Mathlib.RingTheory.Norm.Basic
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⟯
⊢ Membership.mem (γ := Subalgebra K L) (toSubalgebra K⟮x⟯) x

Tactic:
exact IntermediateField.subset_adjoin K _ (Set.mem_singleton x)

Premises used: Set.mem_singleton, IntermediateField.subset_adjoin
-- Module: Mathlib.RingTheory.Norm.Basic
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))
⊢ Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)

Tactic:
have injKxL := (algebraMap K⟮x⟯ L).injective
-- Module: Mathlib.RingTheory.Norm.Basic
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
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
⊢ (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

Premises used: IsIntegral
-- Module: Mathlib.RingTheory.Norm.Basic
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

Tactic:
simp [minpoly.eq_zero hx, IntermediateField.AdjoinSimple.norm_gen_eq_one hx, aroots_def]

Premises used: IntermediateField.AdjoinSimple.norm_gen_eq_one, minpoly.eq_zero, Polynomial.aroots_def
-- Module: Mathlib.RingTheory.Norm.Basic
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
pos₁ : Splits (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen))
⊢ (algebraMap K F : (a : K) → F) ((norm K : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K) = (aroots (minpoly K x) F).prod

Tactic:
rw [← adjoin.powerBasis_gen hx, PowerBasis.norm_gen_eq_prod_roots]

Premises used: IntermediateField.adjoin.powerBasis_gen, Algebra.PowerBasis.norm_gen_eq_prod_roots
-- Module: Mathlib.RingTheory.Norm.Basic
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 (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L)) F).prod =
    (aroots (minpoly K x) F).prod
⊢ (aroots (minpoly K (adjoin.powerBasis hx).gen) F).prod = (aroots (minpoly K x) F).prod

Tactic:
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]

Premises used: IntermediateField.adjoin.powerBasis_gen, minpoly.algebraMap_eq
-- Module: Mathlib.RingTheory.Norm.Basic
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 :
  Splits
    (Polynomial.map (algebraMap K F)
      (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L)))
⊢ Splits (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen))

Tactic:
rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]

Premises used: IntermediateField.adjoin.powerBasis_gen, minpoly.algebraMap_eq
-- Module: Mathlib.RingTheory.Norm.Basic
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 (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L)) F).prod =
    (aroots (minpoly K x) F).prod

Tactic:
simp only [AdjoinSimple.algebraMap_gen _ _, hf]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.RingTheory.Norm.Basic
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 (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (AdjoinSimple.gen K x) : L)))

Tactic:
simp only [AdjoinSimple.algebraMap_gen _ _, hf]

Premises used: IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.RingTheory.Norm.Basic
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 = ∏ σ : S →ₐ[R] F, (σ : (a : S) → F) pb.gen
⊢ 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)

Tactic:
rw [PowerBasis.norm_gen_eq_prod_roots pb hE]

Premises used: Algebra.PowerBasis.norm_gen_eq_prod_roots
-- Module: Mathlib.RingTheory.Norm.Basic
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)
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))
⊢ (aroots (minpoly R pb.gen) F).prod = ∏ σ : S →ₐ[R] F, (σ : (a : S) → F) pb.gen

Tactic:
rw [@Fintype.prod_equiv (S →ₐ[R] F) _ _ (PowerBasis.AlgHom.fintype pb) _ _ pb.liftEquiv'
    (fun σ => σ pb.gen) (fun x => x) ?_]

Premises used: PowerBasis.liftEquiv', Fintype.prod_equiv, PowerBasis.gen, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Norm.Basic
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
hfg : ∀ (x : { x : F // x ∈ aroots (minpoly R pb.gen) F }), (↑x : F) = _root_.id (↑x : F)
⊢ (aroots (minpoly R pb.gen) F).prod = ∏ x : { y : F // y ∈ (minpoly R pb.gen).aroots F }, (↑x : F)

Tactic:
rw [Finset.prod_mem_multiset, Finset.prod_eq_multiset_prod, Multiset.toFinset_val,
      Multiset.dedup_eq_self.mpr, Multiset.map_id]

Premises used: Iff.mpr, Multiset.map_id, Multiset.dedup_eq_self, Finset.prod_eq_multiset_prod, Finset.prod_mem_multiset, Multiset.toFinset_val
-- Module: Mathlib.RingTheory.Norm.Basic
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).Nodup

Tactic:
nodup_roots (.map hfx)

Premises used: Polynomial.Separable.map, Polynomial.nodup_roots
-- Module: Mathlib.RingTheory.Norm.Basic
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).Nodup

Tactic:
exact nodup_roots (.map hfx)

Premises used: Polynomial.Separable.map, Polynomial.nodup_roots