awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
hle : L ≤ E
L' : IntermediateField k ↥E := restrict hle
h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index
e_H : map (IsScalarTower.toAlgHom k (↥E) K) L' = L
⊢ Subgroup.index (G := Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k (↥E) K) L')) = L.fixingSubgroup.index

Tactic:
congr 2
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
hle : L ≤ E
L' : IntermediateField k ↥E := restrict hle
h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index
⊢ map (IsScalarTower.toAlgHom k (↥E) K) L' = L

Tactic:
lift_restrict hle

Premises used: IntermediateField.lift, Set.Mem, iSup, Subalgebra.val, IsScalarTower.toAlgHom, IntermediateField.normalClosure, IntermediateField.adjoin, IntermediateField.val, IntermediateField.lift_restrict
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
hle : L ≤ E
L' : IntermediateField k ↥E := restrict hle
h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index
⊢ map (IsScalarTower.toAlgHom k (↥E) K) L' = L

Tactic:
exact lift_restrict hle

Premises used: IntermediateField.lift_restrict
-- Module: Mathlib.FieldTheory.KrullTopology
Goal:
k : Type u_1
K : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
inst_3 : IsGalois k K
L : IntermediateField k K
hnfd : FiniteDimensional.{u_1, u_3} k ↥L
E : IntermediateField k K := normalClosure k (↥L) K
hle : L ≤ E
L' : IntermediateField k ↥E := restrict hle
h : Module.finrank.{u_1, u_3} k ↥L' * Module.finrank.{u_3, u_3} ↥L' ↥E = Module.finrank.{u_1, u_3} k ↥E
rw :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' * Nat.card.{u_3} ↥L'.fixingSubgroup = Module.finrank.{u_1, u_3} k ↥E),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
rw₁ rw₂ rw₃ :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' * Nat.card.{u_3} ↥L'.fixingSubgroup = Nat.card.{u_3} Gal(↥E/k)),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
rw₄ :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index),
    Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index
rw₅ :
  ∀ (h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index),
    Subgroup.index (G := Gal(K/k)) (fixingSubgroup (map (IsScalarTower.toAlgHom k (↥E) K) L')) = L.fixingSubgroup.index
e_H : ∀ (h : Module.finrank.{u_1, u_3} k ↥L' = L'.fixingSubgroup.index), map (IsScalarTower.toAlgHom k (↥E) K) L' = L
⊢ Module.finrank.{u_1, u_3} k ↥L = L.fixingSubgroup.index

Tactic:
classical
  rw [← IsGalois.card_fixingSubgroup_eq_finrank L', ← IsGalois.card_aut_eq_finrank k E] at h
  rw [← L'.fixingSubgroup.index_mul_card, Nat.mul_left_inj Finite.card_pos.ne'] at h
  rw [(restrict_algEquiv hle).toLinearEquiv.finrank_eq, h, ← L'.map_fixingSubgroup_index K]
  congr 2
  exact lift_restrict hle

Premises used: IsGalois.card_aut_eq_finrank, IsGalois.card_fixingSubgroup_eq_finrank, Subgroup.index_mul_card, Membership.mem, IntermediateField.fixingSubgroup, Subtype, LinearEquiv.finrank_eq, Finite.card_pos, LT.lt.ne', IntermediateField.map_fixingSubgroup_index, Nat.mul_left_inj, AlgEquiv.toLinearEquiv, IntermediateField.lift_restrict, IntermediateField.restrict_algEquiv
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n = 0
⊢ (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).Splits

Tactic:
simp only [hn, pow_zero, ← C.map_one, ← map_sub, Splits.C]

Premises used: Polynomial.C, map_sub, RingHom.map_one, pow_zero, Polynomial.Splits.C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
hn : n > 0
inr :
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).roots.card =
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
inr₁ :
  (nthRoots n a).card = (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
inr₂ :
  (if ∃ (α : K), α ^ n = a then n else 0) =
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).natDegree
inr₃ : (if ∃ (α : K), α ^ n = a then n else 0) = n
inr₄ inr₅ : n = n
⊢ (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X])).Splits

Tactic:
rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]

Premises used: Polynomial.natDegree_X_pow_sub_C, if_pos, Polynomial.splits_iff_card_roots, Polynomial.nthRoots, IsPrimitiveRoot.card_nthRoots
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
e : α ^ n = a
⊢ n = 0 ∨ n > 0

Tactic:
cases n.eq_zero_or_pos with
  | inl hn =>
    simp only [hn, pow_zero, ← C.map_one, ← map_sub, Splits.C]
  | inr hn =>
    rw [splits_iff_card_roots, ← nthRoots, hζ.card_nthRoots, natDegree_X_pow_sub_C, if_pos ⟨α, e⟩]

Premises used: Polynomial.C, Polynomial.natDegree_X_pow_sub_C, map_sub, RingHom.map_one, if_pos, Polynomial.splits_iff_card_roots, pow_zero, Polynomial.nthRoots, IsPrimitiveRoot.card_nthRoots, Polynomial.Splits.C, Nat.eq_zero_or_pos
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
rw :
  Eq.{u + 1} (α := K[X])
    (Multiset.prod
      (Multiset.map
        ((fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) ∘ fun (x : ℕ) ↦ ζ ^ x * α)
        (Multiset.range n)))
    (∏ i ∈ Finset.range n, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) (ζ ^ i * α) : K[X]))
⊢ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]) =
    ∏ i ∈ Finset.range n, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) (ζ ^ i * α) : K[X])

Tactic:
rw [(X_pow_sub_C_splits_of_isPrimitiveRoot hζ e).eq_prod_roots_of_monic
    (monic_X_pow_sub_C _ hn.ne'), ← nthRoots, hζ.nthRoots_eq e, Multiset.map_map]

Premises used: X_pow_sub_C_splits_of_isPrimitiveRoot, Polynomial.monic_X_pow_sub_C, Polynomial.nthRoots, LT.lt.ne', Polynomial.Splits.eq_prod_roots_of_monic, Multiset.map_map, IsPrimitiveRoot.nthRoots_eq
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
ζ : K
hζ : IsPrimitiveRoot ζ n
α a : K
hn : 0 < n
e : α ^ n = a
⊢ Eq.{u + 1} (α := K[X])
    (Multiset.prod
      (Multiset.map
        ((fun (x : K) ↦ HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) ∘ fun (x : ℕ) ↦ ζ ^ x * α)
        (Multiset.range n)))
    (∏ i ∈ Finset.range n, HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) (ζ ^ i * α) : K[X]))

Tactic:
rfl
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
⊢ Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)

Tactic:
have h := FaithfulSMul.algebraMap_injective R K
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
⊢ Function.Injective (Polynomial.map i)

Tactic:
map_injective i h

Premises used: Polynomial.map_injective
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
apply_fun :
  Polynomial.map i (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) =
    Polynomial.map i
      (∏ i ∈ Finset.range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ζ ^ i * α) : R[X]))
⊢ HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) =
    ∏ i ∈ Finset.range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ζ ^ i * α) : R[X])

Tactic:
apply_fun Polynomial.map i using map_injective i h

Premises used: Polynomial.map_injective, Polynomial.map
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective (α := R) (β := K) (⇑(algebraMap R K) : (a : R) → K)
⊢ Polynomial.map i (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])) =
    Polynomial.map i
      (∏ i ∈ Finset.range n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (ζ ^ i * α) : R[X]))

Tactic:
simpa only [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, map_mul, map_pow,
    Polynomial.map_prod, Polynomial.map_mul]
    using X_pow_sub_C_eq_prod' (hζ.map_of_injective h) hn <| map_pow i α n ▸ congrArg i e

Premises used: Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_X, map_pow, Polynomial.map_prod, map_mul, _private.0.X_pow_sub_C_eq_prod', Polynomial.map_sub, IsPrimitiveRoot.map_of_injective, Polynomial.map_C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
hm : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]))
hn :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])

Tactic:
rw [pow_zero, ← C.map_one, ← map_sub] at hm

Premises used: Polynomial.C, map_sub, RingHom.map_one, pow_zero
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
hm : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]))
hn :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hm₁ : Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])
⊢ ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))

Tactic:
rw [pow_zero, ← C.map_one, ← map_sub] at hm

Premises used: Polynomial.C, map_sub, RingHom.map_one, pow_zero
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
hm : Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])
hn :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ False

Tactic:
not_irreducible_C _ hm

Premises used: Polynomial.not_irreducible_C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
hm : Irreducible (M := K[X]) ((C : (a : K) → K[X]) (1 - a) : K[X])
hn :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ False

Tactic:
exact not_irreducible_C _ hm

Premises used: Polynomial.not_irreducible_C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n m : ℕ
a : K
hm : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X m) ((C : (a : K) → K[X]) a : K[X]))
hn :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X m) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ m ≠ 0

Tactic:
have hm' : m ≠ 0 := by
    rintro rfl
    rw [pow_zero, ← C.map_one, ← map_sub] at hm
    exact not_irreducible_C _ hm
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n m : ℕ
a : K
hm : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X m) ((C : (a : K) → K[X]) a : K[X]))
hn :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X m) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hm' : m ≠ 0
⊢ ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X m) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (α := (↥K⟮x⟯)[X]) (β := (↥K⟮x⟯)[X]) (Polynomial.map (algebraMap K ↥K⟮x⟯) (HPow.hPow (α := K[X]) X n))
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))

Tactic:
simpa only [Polynomial.map_pow, map_X] using hn

Premises used: Polynomial.map_pow, Polynomial.map_X
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
n m : ℕ
a : K
hm : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X m) ((C : (a : K) → K[X]) a : K[X]))
hn :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X m) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
hm' : m ≠ 0
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (n * m)) ((C : (a : K) → K[X]) a : K[X]))

Tactic:
simpa [pow_mul] using irreducible_comp (monic_X_pow_sub_C a hm') (monic_X_pow n) hm
    (by simpa only [Polynomial.map_pow, map_X] using hn)

Premises used: Polynomial.monic_X_pow, Polynomial.irreducible_comp, Polynomial.monic_X_pow_sub_C, pow_mul
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
hn : Odd (α := ℕ) 0
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 0 → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 0) ((C : (a : K) → K[X]) a : K[X]))

Tactic:
simp [← Nat.not_even_iff_odd] at hn

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
K : Type u
inst : Field K
hn : Odd (α := ℕ) 1
a : K
ha : ∀ (p : ℕ), Nat.Prime p → p ∣ 1 → ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) (β := ℕ) X 1) ((C : (a : K) → K[X]) a : K[X]))

Tactic:
simpa using irreducible_X_sub_C a

Premises used: Polynomial.irreducible_X_sub_C
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
K : Type u
inst : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
prime_mul : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (n * p)) ((C : (a : K) → K[X]) a : K[X]))
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (p * n)) ((C : (a : K) → K[X]) a : K[X]))

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
K : Type u
inst : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
prime_mul :
  ∀ (E : Type u) [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (n * p)) ((C : (a : K) → K[X]) a : K[X]))

Tactic:
apply X_pow_mul_sub_C_irreducible
      (X_pow_sub_C_irreducible_of_prime hp (ha p hp (dvd_mul_right _ _)))

Premises used: X_pow_sub_C_irreducible_of_prime, X_pow_mul_sub_C_irreducible, dvd_mul_right
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
K : Type u
inst : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
prime_mul :
  ∀ [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ ∀ [inst_1 : Field E] [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))

Tactic:
_
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
K : Type u
inst : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst_1 : Field E
prime_mul :
  ∀ [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))
⊢ ∀ [inst_2 : Algebra K E] (x : E),
    minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]) →
      Irreducible
        (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
          ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))

Tactic:
_
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
K : Type u
inst : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst_1 : Field E
inst_2 : Algebra K E
x : E
hx : minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬IsIntegral K x
⊢ False

Tactic:
simpa only [degree_zero, degree_X_pow_sub_C hp.pos,
        WithBot.natCast_ne_bot] using congr_arg degree (hx.symm.trans (dif_neg h))

Premises used: Nat.Prime.pos, WithBot.natCast_ne_bot, Polynomial.degree, Polynomial.degree_X_pow_sub_C, Polynomial.degree_zero, dif_neg, congr_arg, Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
K : Type u
inst : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst_1 : Field E
inst_2 : Algebra K E
x : E
hx : minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
⊢ IsIntegral K x

Tactic:
have : IsIntegral K x := not_not.mp fun h ↦ by
      simpa only [degree_zero, degree_X_pow_sub_C hp.pos,
        WithBot.natCast_ne_bot] using congr_arg degree (hx.symm.trans (dif_neg h))
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
K : Type u
inst : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst_1 : Field E
inst_2 : Algebra K E
x : E
hx : minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
this : IsIntegral K x
prime_mul : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : ↥K⟮x⟯), b ^ p ≠ AdjoinSimple.gen K x
⊢ Irreducible
    (HSub.hSub (β := (↥K⟮x⟯)[X]) (HPow.hPow (α := (↥K⟮x⟯)[X]) X n)
      ((C : (a : ↥K⟮x⟯) → (↥K⟮x⟯)[X]) (AdjoinSimple.gen K x) : (↥K⟮x⟯)[X]))

Tactic:
apply IH (Nat.odd_mul.mp hn).2

Premises used: Nat.odd_mul, And.right, Iff.mp
-- Module: Mathlib.FieldTheory.KummerExtension
Goal:
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K] (hn : Odd n) {a : K} (ha : ∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a),
    Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
K : Type u
inst : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst_1 : Field E
inst_2 : Algebra K E
x : E
hx : minpoly K x = HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
this : IsIntegral K x
q : ℕ
hq : Nat.Prime q
hqn : q ∣ n
b : ↥K⟮x⟯
hb : b ^ q = AdjoinSimple.gen K x
prime_mul : HPow.hPow (α := K) ((Algebra.norm K : (a : ↥K⟮x⟯) → K) b : K) q = a
⊢ False

Tactic:
apply ha q hq (dvd_mul_of_dvd_right hqn p) (Algebra.norm _ b)

Premises used: dvd_mul_of_dvd_right, Algebra.norm, DFunLike.coe