awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨x, congr_arg (·.1) eq⟩
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
rw : CharP (ZMod p) p
⊢ CharP K p

Tactic:
rw [← Algebra.charP_iff (ZMod p) K p]

Premises used: Algebra.charP_iff, ZMod
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP (ZMod p) p

Tactic:
ZMod.charP p

Premises used: ZMod.charP
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP (ZMod p) p

Tactic:
exact ZMod.charP p

Premises used: ZMod.charP
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
⊢ CharP K p

Tactic:
have : CharP K p := by rw [← Algebra.charP_iff (ZMod p) K p]; exact ZMod.charP p
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
rw : CharP (ZMod p) p
⊢ CharP K' p

Tactic:
rw [← Algebra.charP_iff (ZMod p) K' p]

Premises used: Algebra.charP_iff, ZMod
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ CharP (ZMod p) p

Tactic:
ZMod.charP p

Premises used: ZMod.charP
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ CharP (ZMod p) p

Tactic:
exact ZMod.charP p

Premises used: ZMod.charP
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this : CharP K p
⊢ CharP K' p

Tactic:
have : CharP K' p := by rw [← Algebra.charP_iff (ZMod p) K' p]; exact ZMod.charP p
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this_1 : CharP K p
this : CharP K' p
choose : (n : ℕ+) → (a : Nat.Prime p) → (hK : Fintype.card K = p ^ (↑n : ℕ)) → K ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'

Tactic:
choose n a hK using FiniteField.card K p

Premises used: FiniteField.card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this_1 : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
choose : (n' : ℕ+) → (a' : Nat.Prime p) → (hK' : Fintype.card K' = p ^ (↑n' : ℕ)) → K ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'

Tactic:
choose n' a' hK' using FiniteField.card K' p

Premises used: FiniteField.card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
hKK' : Fintype.card K = Fintype.card K'
this_1 : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ (↑n' : ℕ)
rw :
  (a : Nat.Prime p) →
    (hK : Fintype.card K = p ^ (↑n : ℕ)) →
      (n' : ℕ+) →
        (hKK' : p ^ (↑n : ℕ) = p ^ (↑n' : ℕ)) →
          (a' : Nat.Prime p) → (hK' : Fintype.card K' = p ^ (↑n' : ℕ)) → K ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'

Tactic:
rw [hK, hK'] at hKK'
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
this_1 : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hKK' : p ^ (↑n : ℕ) = p ^ (↑n' : ℕ)
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ (↑n' : ℕ)
have : (hGalK : K ≃ₐ[ZMod p] GaloisField p (↑n : ℕ)) → K ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'

Tactic:
have hGalK := GaloisField.algEquivGaloisFieldOfFintype p n hK
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
this_1 : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hKK' : p ^ (↑n : ℕ) = p ^ (↑n' : ℕ)
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ (↑n' : ℕ)
hGalK : K ≃ₐ[ZMod p] GaloisField p (↑n : ℕ)
have : (hK'Gal : GaloisField p (↑n' : ℕ) ≃ₐ[ZMod p] K') → K ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'

Tactic:
have hK'Gal := (GaloisField.algEquivGaloisFieldOfFintype p n' hK').symm
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
this_1 : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hKK' : p ^ (↑n : ℕ) = p ^ (↑n' : ℕ)
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ (↑n' : ℕ)
hGalK : K ≃ₐ[ZMod p] GaloisField p (↑n : ℕ)
hK'Gal : GaloisField p (↑n' : ℕ) ≃ₐ[ZMod p] K'
rw :
  (hKK' : p ^ (↑n' : ℕ) = p ^ (↑n' : ℕ)) →
    (a' : Nat.Prime p) →
      (hK' : Fintype.card K' = p ^ (↑n' : ℕ)) →
        (hGalK : K ≃ₐ[ZMod p] GaloisField p (↑n' : ℕ)) →
          (hK'Gal : GaloisField p (↑n' : ℕ) ≃ₐ[ZMod p] K') → K ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'

Tactic:
rw [Nat.pow_right_injective h_prime.out.one_lt hKK'] at *

Premises used: Nat.Prime.one_lt, Nat.pow_right_injective, Fact.out
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
p : ℕ
h_prime : Fact (Nat.Prime p)
inst_5 : Algebra (ZMod p) K
inst_6 : Algebra (ZMod p) K'
this_1 : CharP K p
this : CharP K' p
n : ℕ+
a : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hKK' : p ^ (↑n' : ℕ) = p ^ (↑n' : ℕ)
a' : Nat.Prime p
hK' : Fintype.card K' = p ^ (↑n' : ℕ)
hGalK : K ≃ₐ[ZMod p] GaloisField p (↑n' : ℕ)
hK'Gal : GaloisField p (↑n' : ℕ) ≃ₐ[ZMod p] K'
⊢ K ≃ₐ[ZMod p] K'

Tactic:
exact AlgEquiv.trans hGalK hK'Gal

Premises used: AlgEquiv.trans
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
choose : (p : ℕ) → (_char_p_K : CharP K p) → K ≃+* K'
⊢ K ≃+* K'

Tactic:
choose p _char_p_K using CharP.exists K

Premises used: CharP.exists
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
choose : (p' : ℕ) → (_char_p'_K' : CharP K' p') → K ≃+* K'
⊢ K ≃+* K'

Tactic:
choose p' _char_p'_K' using CharP.exists K'

Premises used: CharP.exists
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
choose : (n : ℕ+) → (hp : Nat.Prime p) → (hK : Fintype.card K = p ^ (↑n : ℕ)) → K ≃+* K'
⊢ K ≃+* K'

Tactic:
choose n hp hK using FiniteField.card K p

Premises used: FiniteField.card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
choose : (n' : ℕ+) → (hp' : Nat.Prime p') → (hK' : Fintype.card K' = p' ^ (↑n' : ℕ)) → K ≃+* K'
⊢ K ≃+* K'

Tactic:
choose n' hp' hK' using FiniteField.card K' p'

Premises used: FiniteField.card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ (↑n' : ℕ)
by_contra : ∀ (hne : ¬p = p'), False
⊢ p = p'

Tactic:
by_contra hne
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ (↑n' : ℕ)
hne : ¬p = p'
⊢ False

Tactic:
simpa [← hK, hK', hKK', hp'.ne_one] using Nat.coprime_pow_primes n n' hp hp' hne

Premises used: PNat.val, Nat.Prime.ne_one, Nat.coprime_pow_primes
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ (↑n' : ℕ)
⊢ p = p'

Tactic:
have hpp' : p = p' := by
    by_contra hne
    simpa [← hK, hK', hKK', hp'.ne_one] using Nat.coprime_pow_primes n n' hp hp' hne
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p'
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ (↑n' : ℕ)
hpp' : p = p'
rw :
  (_char_p'_K' : CharP K' p) →
    (n : ℕ+) →
      (hp : Nat.Prime p) →
        (hK : Fintype.card K = p ^ (↑n : ℕ)) →
          (n' : ℕ+) → (hp' : Nat.Prime p') → (hK' : Fintype.card K' = p' ^ (↑n' : ℕ)) → (hpp' : p = p') → K ≃+* K'
⊢ K ≃+* K'

Tactic:
rw [← hpp'] at _char_p'_K'
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ (↑n' : ℕ)
hpp' : p = p'
⊢ Fact (Nat.Prime p)

Tactic:
haveI := fact_iff.2 hp
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p_1 : ℕ
inst : Fact (Nat.Prime p_1)
n_1 : ℕ
K : Type u_1
K' : Type u_2
inst_1 : Field K
inst_2 : Field K'
inst_3 : Fintype K
inst_4 : Fintype K'
hKK' : Fintype.card K = Fintype.card K'
p : ℕ
_char_p_K : CharP K p
p' : ℕ
_char_p'_K' : CharP K' p
n : ℕ+
hp : Nat.Prime p
hK : Fintype.card K = p ^ (↑n : ℕ)
n' : ℕ+
hp' : Nat.Prime p'
hK' : Fintype.card K' = p' ^ (↑n' : ℕ)
hpp' : p = p'
this_1 : Fact (Nat.Prime p)
this_2 : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) K' := ZMod.algebra K' p
⊢ K ≃+* K'

Tactic:
exact ↑(algEquivOfCardEq p hKK')

Premises used: FiniteField.algEquivOfCardEq
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_3
inst_1 : AddCommGroup k
inst_2 : Finite k
inst_3 : Module (ZMod p) k
rw : p ^ Module.finrank (ZMod p) k = Nat.card (ZMod p) ^ Module.finrank (ZMod p) k
rw₁ rw₂ : p ^ Module.finrank (ZMod p) k = p ^ Module.finrank (ZMod p) k
⊢ p ^ Module.finrank (ZMod p) k = Nat.card k

Tactic:
rw [Module.natCard_eq_pow_finrank (K := ZMod p), Nat.card_zmod]

Premises used: Module.natCard_eq_pow_finrank, Nat.card_zmod
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : Type u_3
inst_1 : AddCommGroup k
inst_2 : Fintype k
inst_3 : Module (ZMod p) k
rw : Nat.card k = Fintype.card k
rw₁ rw₂ : Nat.card k = Nat.card k
⊢ p ^ Module.finrank (ZMod p) k = Fintype.card k

Tactic:
rw [pow_finrank_eq_natCard, Fintype.card_eq_nat_card]

Premises used: FiniteField.pow_finrank_eq_natCard, Fintype.card_eq_nat_card
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
⊢ Finite F

Tactic:
have := Finite.of_injective _ (algebraMap F L).injective
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this : Finite F
have : ∀ (this : Fintype F), Nonempty (K →ₐ[F] L)
⊢ Nonempty (K →ₐ[F] L)

Tactic:
have := Fintype.ofFinite F
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this : Fintype F
⊢ Module.Finite F K

Tactic:
have := Module.finite_of_finrank_pos (Nat.pos_of_dvd_of_pos h Module.finrank_pos)
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this : Module.Finite F K
⊢ Finite K

Tactic:
have := Module.finite_of_finite F (M := K)
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this : Finite K
have : ∀ (this : Fintype K), Nonempty (K →ₐ[F] L)
⊢ Nonempty (K →ₐ[F] L)

Tactic:
have := Fintype.ofFinite K
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this : Fintype K
have : ∀ (this : Fintype L), Nonempty (K →ₐ[F] L)
⊢ Nonempty (K →ₐ[F] L)

Tactic:
have := Fintype.ofFinite L
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this_5 : Fintype K
this : Fintype L
⊢ Nonempty (K →ₐ[F] L)

Tactic:
⟨Polynomial.IsSplittingField.lift _ (X ^ Fintype.card K - X) ?_⟩

Premises used: HSub.hSub, Fintype.card, Polynomial.IsSplittingField.lift, Nonempty.intro, HPow.hPow, Polynomial.X
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this_5 : Fintype K
this : Fintype L
refine : Splits (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
⊢ Nonempty (K →ₐ[F] L)

Tactic:
refine ⟨Polynomial.IsSplittingField.lift _ (X ^ Fintype.card K - X) ?_⟩
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this_5 : Fintype K
this : Fintype L
⊢ Splits (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))

Tactic:
(FiniteField.isSplittingField_sub L F).splits.of_dvd ?_ ?_

Premises used: Polynomial.IsSplittingField.splits, Polynomial.Splits.of_dvd
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this_5 : Fintype K
this : Fintype L
refine_1 : Ne (α := L[X]) (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card L) - X)) 0
refine_2 :
  Dvd.dvd (α := L[X]) (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
    (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card L) - X))
⊢ Splits (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))

Tactic:
refine (FiniteField.isSplittingField_sub L F).splits.of_dvd ?_ ?_

Premises used: Polynomial.IsSplittingField.splits, Polynomial.Splits.of_dvd
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this_5 : Fintype K
this : Fintype L
⊢ Ne (α := L[X]) (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card L) - X)) 0

Tactic:
map_ne_zero (FiniteField.X_pow_card_sub_X_ne_zero _ Fintype.one_lt_card)

Premises used: Fintype.one_lt_card, FiniteField.X_pow_card_sub_X_ne_zero, Polynomial.map_ne_zero
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this_5 : Fintype K
this : Fintype L
⊢ Ne (α := L[X]) (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card L) - X)) 0

Tactic:
exact map_ne_zero (FiniteField.X_pow_card_sub_X_ne_zero _ Fintype.one_lt_card)
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this_5 : Fintype K
this : Fintype L
refine_2 :
  Dvd.dvd (α := L[X])
    (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card F ^ Module.finrank F K) - X))
    (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card F ^ Module.finrank F L) - X))
⊢ Dvd.dvd (α := L[X]) (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
    (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card L) - X))

Tactic:
rw [Module.card_eq_pow_finrank (K := F), Module.card_eq_pow_finrank (K := F) (V := L)]

Premises used: Module.card_eq_pow_finrank
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this_5 : Fintype K
this : Fintype L
⊢ Dvd.dvd (α := L[X])
    (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card F ^ Module.finrank F K) - X))
    (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card F ^ Module.finrank F L) - X))

Tactic:
(map_dvd_map' _).mpr (dvd_pow_pow_sub_self_of_dvd h)

Premises used: Iff.mpr, dvd_pow_pow_sub_self_of_dvd, Polynomial.map_dvd_map'
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
this_1 : Finite F
this_2 : Fintype F
this_3 : Module.Finite F K
this_4 : Finite K
this_5 : Fintype K
this : Fintype L
⊢ Dvd.dvd (α := L[X])
    (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card F ^ Module.finrank F K) - X))
    (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card F ^ Module.finrank F L) - X))

Tactic:
exact (map_dvd_map' _).mpr (dvd_pow_pow_sub_self_of_dvd h)

Premises used: Iff.mpr, dvd_pow_pow_sub_self_of_dvd, Polynomial.map_dvd_map'
-- Module: Mathlib.FieldTheory.Finite.GaloisField
Goal:
F : Type u_3
K : Type u_4
L : Type u_5
inst : Field F
inst_1 : Field K
inst_2 : Algebra F K
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Finite L
h : Module.finrank F K ∣ Module.finrank F L
obtain : ∀ (f : K →ₐ[F] L), Nat.card (K →ₐ[F] L) = Module.finrank F K
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K

Tactic:
obtain ⟨f⟩ := nonempty_algHom_of_finrank_dvd h

Premises used: FiniteField.nonempty_algHom_of_finrank_dvd