awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
n : ℕ
h_prime : Fact (Nat.Prime (n + 1))
hp : 1 < n + 1
h1 : (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).roots = val univ
h2 : (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree = n + 1
succ :
  (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).roots.card =
    (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₁ : Multiset.card (α := ZMod (n + 1)) (val univ) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₂ : Finset.card (α := ZMod (n + 1)) univ = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₃ : Fintype.card (ZMod (n + 1)) = (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).natDegree
succ₄ : Fintype.card (ZMod (n + 1)) = n + 1
succ₅ succ₆ : n + 1 = n + 1
⊢ (HPow.hPow (α := (ZMod (n + 1))[X]) X (n + 1) - X).Splits

Tactic:
rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]

Premises used: Finset.card_univ, Polynomial.splits_iff_card_roots, Finset.card_def, ZMod.card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
rw : HPow.hPow (α := (ZMod p)[X]) X p = HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p))
rw₁ rw₂ : HPow.hPow (α := (ZMod p)[X]) X p = HPow.hPow (α := (ZMod p)[X]) X p
⊢ HPow.hPow (α := (ZMod p)[X]) X (HPow.hPow (β := ℕ) p 1) = HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p))

Tactic:
rw [pow_one, ZMod.card p]

Premises used: pow_one, ZMod.card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := (ZMod p)[X]) X (HPow.hPow (β := ℕ) p 1) = HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p))
rw : IsSplittingField (ZMod p) (ZMod p) (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p)) - X)
⊢ IsSplittingField (ZMod p) (ZMod p) (HPow.hPow (α := (ZMod p)[X]) X (HPow.hPow (β := ℕ) p 1) - X)

Tactic:
rw [h]
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
h : HPow.hPow (α := (ZMod p)[X]) X (HPow.hPow (β := ℕ) p 1) = HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p))
⊢ IsSplittingField (ZMod p) (ZMod p) (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card (ZMod p)) - X)

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : Algebra (ZMod p) K
⊢ Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card K) - X))

Tactic:
(FiniteField.isSplittingField_sub K (ZMod p)).splits

Premises used: Polynomial.IsSplittingField.splits
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : Algebra (ZMod p) K
h : Fintype.card K = p ^ n
⊢ IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X)

Tactic:
h ▸ FiniteField.isSplittingField_sub K (ZMod p)

Premises used: Eq.rec, ZMod, FiniteField.isSplittingField_sub
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
inst_2 : Finite K
haveI :
  ∀ (this : Fintype K),
    Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Nat.card K) - X))
⊢ Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Nat.card K) - X))

Tactic:
haveI : Fintype K := Fintype.ofFinite K
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
inst_2 : Finite K
this : Fintype K
rw : Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card K) - X))
⊢ Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Nat.card K) - X))

Tactic:
rw [Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
inst_2 : Finite K
this : Fintype K
⊢ Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card K) - X))

Tactic:
(FiniteField.isSplittingField_sub K (ZMod p)).splits

Premises used: Polynomial.IsSplittingField.splits
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
inst_2 : Finite K
this : Fintype K
⊢ Splits (Polynomial.map (algebraMap (ZMod p) K) (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card K) - X))

Tactic:
exact (FiniteField.isSplittingField_sub K (ZMod p)).splits

Premises used: Polynomial.IsSplittingField.splits
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
h : Nat.card K = p ^ n
⊢ Finite K

Tactic:
haveI : Finite K := (Nat.card_pos_iff.mp (h ▸ pow_pos h_prime.1.pos n)).2
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this : Finite K
haveI : ∀ (this : Fintype K), IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X)
⊢ IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X)

Tactic:
haveI : Fintype K := Fintype.ofFinite K
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this_1 : Finite K
this : Fintype K
rw : IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card K) - X)
⊢ IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (p ^ n) - X)

Tactic:
rw [← h, Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this_1 : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card K) - X)

Tactic:
FiniteField.isSplittingField_sub K (ZMod p)

Premises used: ZMod, FiniteField.isSplittingField_sub
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
inst : Field K
inst_1 : Algebra (ZMod p) K
h : Nat.card K = p ^ n
this_1 : Finite K
this : Fintype K
⊢ IsSplittingField (ZMod p) K (HPow.hPow (α := (ZMod p)[X]) X (Fintype.card K) - X)

Tactic:
exact FiniteField.isSplittingField_sub K (ZMod p)

Premises used: ZMod, FiniteField.isSplittingField_sub
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
inst : Field K
inl : ∀ (val : Fintype K), (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits
inr : Infinite K → (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits
⊢ (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits

Tactic:
cases fintypeOrInfinite K

Premises used: fintypeOrInfinite
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
inst : Field K
val : Fintype K
⊢ Splits (Polynomial.map (algebraMap K K) (HPow.hPow (α := K[X]) X (Fintype.card K) - X))

Tactic:
have := (IsSplittingField.splits (L := K) (X ^ (Fintype.card K) - X : K[X]))
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
inst : Field K
val : Fintype K
this : Splits (Polynomial.map (algebraMap K K) (HPow.hPow (α := K[X]) X (Fintype.card K) - X))
⊢ (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits

Tactic:
simpa [Algebra.algebraMap_self, map_sub, map_pow, map_X] using this

Premises used: map_sub, Algebra.algebraMap_self, Polynomial.map_X, map_pow
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
inst : Field K
val : Infinite K
inr : (-(HPow.hPow (α := K[X]) X (Nat.card K) - X)).Splits
⊢ (HPow.hPow (α := K[X]) X (Nat.card K) - X).Splits

Tactic:
rw [← Polynomial.splits_neg_iff]

Premises used: Polynomial.splits_neg_iff
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
inst : Field K
val : Infinite K
⊢ (-(HPow.hPow (α := K[X]) X (Nat.card K) - X)).Splits

Tactic:
simpa [Nat.card_eq_zero_of_infinite, pow_zero, neg_sub] using Splits.X_sub_C (1 : K)

Premises used: neg_sub, Nat.card_eq_zero_of_infinite, pow_zero, Polynomial.Splits.X_sub_C, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K_1 : Type u_1
inst_1 : Field K_1
inst_2 : Algebra (ZMod p) K_1
K : Type u_2
K' : Type u_3
inst_3 : Field K
inst_4 : Field K'
inst_5 : Finite K'
inst_6 : Algebra K K'
intro : ∀ (val : Fintype K'), IsGalois K K'
⊢ IsGalois K K'

Tactic:
cases nonempty_fintype K'

Premises used: nonempty_fintype
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p : ℕ
h_prime : Fact (Nat.Prime p)
n : ℕ
K_1 : Type u_1
inst_1 : Field K_1
inst_2 : Algebra (ZMod p) K_1
K : Type u_2
K' : Type u_3
inst_3 : Field K
inst_4 : Field K'
inst_5 : Finite K'
inst_6 : Algebra K K'
val : Fintype K'
intro : ∀ (p : ℕ) (hp : CharP K p), IsGalois K K'
⊢ IsGalois K K'

Tactic:
obtain ⟨p, hp⟩ := CharP.exists K

Premises used: CharP.exists
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p_2 : ℕ
h_prime : Fact (Nat.Prime p_2)
n : ℕ
K_1 : Type u_1
inst_1 : Field K_1
inst_2 : Algebra (ZMod p_2) K_1
K : Type u_2
K' : Type u_3
inst_3 : Field K
inst_4 : Field K'
inst_5 : Finite K'
inst_6 : Algebra K K'
val : Fintype K'
p : ℕ
hp : CharP K p
⊢ CharP K p

Tactic:
haveI : CharP K p := hp
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p_2 : ℕ
h_prime : Fact (Nat.Prime p_2)
n : ℕ
K_1 : Type u_1
inst_1 : Field K_1
inst_2 : Algebra (ZMod p_2) K_1
K : Type u_2
K' : Type u_3
inst_3 : Field K
inst_4 : Field K'
inst_5 : Finite K'
inst_6 : Algebra K K'
val : Fintype K'
p : ℕ
hp : CharP K p
this : CharP K p
⊢ CharP K' p

Tactic:
haveI : CharP K' p := charP_of_injective_algebraMap' K p
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p_2 : ℕ
h_prime : Fact (Nat.Prime p_2)
n : ℕ
K_1 : Type u_1
inst_1 : Field K_1
inst_2 : Algebra (ZMod p_2) K_1
K : Type u_2
K' : Type u_3
inst_3 : Field K
inst_4 : Field K'
inst_5 : Finite K'
inst_6 : Algebra K K'
val : Fintype K'
p : ℕ
hp : CharP K p
this_1 : CharP K p
this : CharP K' p
⊢ IsGalois K K'

Tactic:
IsGalois.of_separable_splitting_field
    (galois_poly_separable p (Fintype.card K')
      (let ⟨n, _, hn⟩ := FiniteField.card K' p
      hn.symm ▸ dvd_pow_self p n.ne_zero))

Premises used: Dvd.dvd, PNat.ne_zero, Eq.rec, Fintype.card, dvd_pow_self, FiniteField.card, _private.0.GaloisField.instIsGaloisOfFinite.match_1, Eq.symm, IsGalois.of_separable_splitting_field, galois_poly_separable
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 p_2 : ℕ
h_prime : Fact (Nat.Prime p_2)
n : ℕ
K_1 : Type u_1
inst_1 : Field K_1
inst_2 : Algebra (ZMod p_2) K_1
K : Type u_2
K' : Type u_3
inst_3 : Field K
inst_4 : Field K'
inst_5 : Finite K'
inst_6 : Algebra K K'
val : Fintype K'
p : ℕ
hp : CharP K p
this_1 : CharP K p
this : CharP K' p
⊢ IsGalois K K'

Tactic:
exact IsGalois.of_separable_splitting_field
    (galois_poly_separable p (Fintype.card K')
      (let ⟨n, _, hn⟩ := FiniteField.card K' p
      hn.symm ▸ dvd_pow_self p n.ne_zero))

Premises used: Dvd.dvd, PNat.ne_zero, Eq.rec, Fintype.card, dvd_pow_self, FiniteField.card, _private.0.GaloisField.instIsGaloisOfFinite.match_1, Eq.symm, IsGalois.of_separable_splitting_field, galois_poly_separable
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
⊢ Finite K

Tactic:
have := Finite.of_injective _ (algebraMap K K').injective
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this : Finite K
have :
  ∀ (this : Fintype K),
    (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
      x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))

Tactic:
have := Fintype.ofFinite K
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this : Fintype K
have :
  ∀ (this : Fintype K'),
    (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
      x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))

Tactic:
have := Fintype.ofFinite K'
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
simp_rw :
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₁ : ∏ σ : Gal(K'/K), (σ : (a : K') → K') x = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₂ :
  ∏ i : Fin (Module.finrank K K'),
      (HPow.hPow (α := Gal(K'/K)) (frobeniusAlgEquivOfAlgebraic K K') (↑i : ℕ) : (a : K') → K') x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₃ :
  ∏ x_1 : Fin (Module.finrank K K'), (⇑(frobeniusAlgEquivOfAlgebraic K K') : (a : K') → K')^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₄ :
  ∏ x_1 : Fin (Module.finrank K K'), (fun (x : K') ↦ x ^ Fintype.card K)^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₅ :
  ∏ x_1 : Fin (Module.finrank K K'), x ^ Fintype.card K ^ (↑x_1 : ℕ) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₆ :
  HPow.hPow (β := ℕ) x (∑ i : Fin (Module.finrank K K'), Fintype.card K ^ (↑i : ℕ)) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₇ :
  HPow.hPow (β := ℕ) x (∑ i ∈ range (Module.finrank K K'), Fintype.card K ^ i) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₈ :
  x ^ ((Fintype.card K ^ Module.finrank K K' - 1) / (Fintype.card K - 1)) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))

Tactic:
simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]

Premises used: Fintype.one_lt_card, pow_iterate, Fin.sum_univ_eq_sum_range, FiniteField.coe_frobeniusAlgEquivOfAlgebraic, AlgEquiv.coe_pow, Module.card_eq_pow_finrank, Nat.geomSum_eq, Algebra.norm_eq_prod_automorphisms, Finset.prod_pow_eq_pow_sum, Function.Bijective.prod_comp, FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
simp_rw : Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ Nat.card.{u_2} K'ˣ / Nat.card.{u_1} Kˣ

Tactic:
simp_rw [Nat.card_units]

Premises used: Nat.card_units
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
have :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)

Tactic:
have := Fintype.ofFinite K'ˣ
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
⊢ Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} ≤
    (Nat.card K' - 1) / (Nat.card K - 1)

Tactic:
IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card

Premises used: Nat.card_le_card_of_injective, Algebra.algebraMap, Nat.sub_pos_of_lt, RingHom.injective, Nat.sub_le_sub_right, IsCyclic.card_pow_eq_one_le, Finite.one_lt_card, Nat.div_pos
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
h :
  Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) =
    Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)

Tactic:
convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card

Premises used: Nat.card_le_card_of_injective, Algebra.algebraMap, Nat.sub_pos_of_lt, RingHom.injective, Nat.sub_le_sub_right, IsCyclic.card_pow_eq_one_le, Finite.one_lt_card, Nat.div_pos
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
h :
  (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ).ncard =
    (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ).ncard
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) =
    Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}

Tactic:
rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]

Premises used: SetLike.coe_sort_coe, Nat.card_coe_set_eq, Set.ncard_coe_finset
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
h :
  (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) =
    (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
⊢ (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ).ncard =
    (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ).ncard

Tactic:
congr 1
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
h :
  ∀ (x : K'ˣ),
    x ∈ (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) ↔
      x ∈ (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
⊢ (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) =
    (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)

Tactic:
ext
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
x : K'ˣ
⊢ x ∈ (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) ↔
    x ∈ (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)

Tactic:
simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]

Premises used: Units.ext_iff, Algebra.algebraMap, Function.Injective.eq_iff, FiniteField.algebraMap_norm_eq_pow, RingHom.injective
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
have have₁ have₂ :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
h :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) =
      Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}
h₁ h₂ :
  ∀ (this : Fintype K'ˣ),
    (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ).ncard =
      (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ).ncard
h₃ h₄ :
  ∀ (this : Fintype K'ˣ),
    (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) =
      (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
h₅ :
  ∀ (this : Fintype K'ˣ) (x : K'ˣ),
    x ∈ (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) ↔
      x ∈ (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)

Tactic:
classical
    have := Fintype.ofFinite K'ˣ
    convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card
    rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]; congr 1; ext
    simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]

Premises used: Nat.card_le_card_of_injective, Units.ext_iff, SetLike.coe_sort_coe, Algebra.algebraMap, Nat.sub_pos_of_lt, Function.Injective.eq_iff, FiniteField.algebraMap_norm_eq_pow, Nat.card_coe_set_eq, RingHom.injective, Nat.sub_le_sub_right, Finite.one_lt_card, Nat.div_pos, Set.ncard_coe_finset
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
k : K
inl : ∃ (a : K'), Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : K') → K) a : K) (0 : K)
inr : ∀ (ne : k ≠ 0), ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k
⊢ ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k

Tactic:
obtain rfl | ne := eq_or_ne k 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
⊢ ∃ (a : K'), Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : K') → K) a : K) (0 : K)

Tactic:
⟨0, Algebra.norm_zero ..⟩

Premises used: Exists.intro, Algebra.norm_zero, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
⊢ ∃ (a : K'), Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : K') → K) a : K) (0 : K)

Tactic:
exact ⟨0, Algebra.norm_zero ..⟩
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
k : K
ne : k ≠ 0
inr :
  ∀ (x : K'ˣ)
    (eq : Eq.{u_1 + 1} (α := Kˣ) ((Units.map (Algebra.norm K) : (a : K'ˣ) → Kˣ) x : Kˣ) (Units.mk0 k ne : Kˣ)),
    ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k
⊢ ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k

Tactic:
have ⟨x, eq⟩ := unitsMap_norm_surjective K K' (Units.mk0 k ne)
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
k : K
ne : k ≠ 0
x : K'ˣ
eq : Eq.{u_1 + 1} (α := Kˣ) ((Units.map (Algebra.norm K) : (a : K'ˣ) → Kˣ) x : Kˣ) (Units.mk0 k ne : Kˣ)
⊢ ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k

Tactic:
⟨x, congr_arg (·.1) eq⟩

Premises used: Units.val, Exists.intro