awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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' : ℕ)
⊢ K ≃ₐ[ZMod p] K'
have have : (hGalK : K ≃ₐ[ZMod p] GaloisField p (↑n : ℕ)) → K ≃ₐ[ZMod p] K'
Tactic: have hGalK := GaloisField.algEquivGaloisFieldOfFintype p n hK
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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 : ℕ)
⊢ K ≃ₐ[ZMod p] K'
have have : (hK'Gal : GaloisField p (↑n' : ℕ) ≃ₐ[ZMod p] K') → K ≃ₐ[ZMod p] K'
Tactic: have hK'Gal := (GaloisField.algEquivGaloisFieldOfFintype p n' hK').symm
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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'
have 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'
Tactic: rw [Nat.pow_right_injective h_prime.out.one_lt hKK'] at *
Cleared hypotheses: hKK', a', hK', hGalK, hK'Gal
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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'
⊢ K ≃+* K'
have choose : (p : ℕ) → (_char_p_K : CharP K p) → K ≃+* K'
Tactic: choose p _char_p_K using CharP.exists K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ K ≃+* K'
have choose : (p' : ℕ) → (_char_p'_K' : CharP K' p') → K ≃+* K'
Tactic: choose p' _char_p'_K' using CharP.exists K'
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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'
⊢ K ≃+* K'
have choose : (n : ℕ+) → (hp : Nat.Prime p) → (hK : Fintype.card K = p ^ (↑n : ℕ)) → K ≃+* K'
Tactic: choose n hp hK using FiniteField.card K p
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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 : ℕ)
⊢ K ≃+* K'
have choose : (n' : ℕ+) → (hp' : Nat.Prime p') → (hK' : Fintype.card K' = p' ^ (↑n' : ℕ)) → K ≃+* K'
Tactic: choose n' hp' hK' using FiniteField.card K' p'
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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'
have by_contra : ∀ (hne : ¬p = p'), False
Tactic: by_contra hne
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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' : ℕ)
⊢ K ≃+* K'
have hpp' : 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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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'
⊢ K ≃+* K'
have 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'
Tactic: rw [← hpp'] at _char_p'_K'
Cleared hypotheses: _char_p'_K', n, hp, hK, n', hp', hK', hpp'
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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'
⊢ K ≃+* K'
have this : Fact (Nat.Prime p)
Tactic: haveI := fact_iff.2 hp
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ p ^ Module.finrank (ZMod p) k = Nat.card k
have rw : p ^ Module.finrank (ZMod p) k = Nat.card (ZMod p) ^ Module.finrank (ZMod p) k
Tactic: rw [Module.natCard_eq_pow_finrank (K := ZMod p), Nat.card_zmod]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ p ^ Module.finrank (ZMod p) k = Nat.card k
have rw₁ : p ^ Module.finrank (ZMod p) k = p ^ Module.finrank (ZMod p) k
Tactic: rw [Module.natCard_eq_pow_finrank (K := ZMod p), Nat.card_zmod]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ p ^ Module.finrank (ZMod p) k = Fintype.card k
have rw : Nat.card k = Fintype.card k
Tactic: rw [pow_finrank_eq_natCard, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ p ^ Module.finrank (ZMod p) k = Fintype.card k
have rw₁ : Nat.card k = Nat.card k
Tactic: rw [pow_finrank_eq_natCard, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ Nonempty (K →ₐ[F] L)
have this : Finite F
Tactic: have := Finite.of_injective _ (algebraMap F L).injective
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Nonempty (K →ₐ[F] L)
have have : ∀ (this : Fintype F), Nonempty (K →ₐ[F] L)
Tactic: have := Fintype.ofFinite F
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ Nonempty (K →ₐ[F] L)
have this₁ : Module.Finite F K
Tactic: have := Module.finite_of_finrank_pos (Nat.pos_of_dvd_of_pos h Module.finrank_pos)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ Nonempty (K →ₐ[F] L)
have this₁ : Finite K
Tactic: have := Module.finite_of_finite F (M := K)
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Nonempty (K →ₐ[F] L)
have have : ∀ (this : Fintype K), Nonempty (K →ₐ[F] L)
Tactic: have := Fintype.ofFinite K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Nonempty (K →ₐ[F] L)
have have : ∀ (this : Fintype L), Nonempty (K →ₐ[F] L)
Tactic: have := Fintype.ofFinite L
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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)
have refine : Splits (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
Tactic: refine ⟨Polynomial.IsSplittingField.lift _ (X ^ Fintype.card K - X) ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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))
have refine_1 : Ne (α := L[X]) (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card L) - X)) 0
Tactic: refine (FiniteField.isSplittingField_sub L F).splits.of_dvd ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Splits (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card K) - X))
have 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))
Tactic: refine (FiniteField.isSplittingField_sub L F).splits.of_dvd ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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 K) - X))
    (Polynomial.map (algebraMap F L) (HPow.hPow (α := F[X]) X (Fintype.card L) - X))
have 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))
Tactic: rw [Module.card_eq_pow_finrank (K := F), Module.card_eq_pow_finrank (K := F) (V := L)]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K
have obtain : ∀ (f : K →ₐ[F] L), Nat.card (K →ₐ[F] L) = Module.finrank F K
Tactic: obtain ⟨f⟩ := nonempty_algHom_of_finrank_dvd h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
f : K →ₐ[F] L
algInst : Algebra K L := f.toAlgebra
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K
have this : Finite K
Tactic: have := Finite.of_injective _ (algebraMap K L).injective
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
f : K →ₐ[F] L
algInst : Algebra K L := f.toAlgebra
this : Finite K
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K
have rw : Nat.card.{u_4} Gal(K/F) = Module.finrank F K
Tactic: rw [Nat.card_congr (Normal.algHomEquivAut F L K), IsGalois.card_aut_eq_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
f : K →ₐ[F] L
algInst : Algebra K L := f.toAlgebra
this : Finite K
rw : Nat.card.{u_4} Gal(K/F) = Module.finrank F K
⊢ Nat.card (K →ₐ[F] L) = Module.finrank F K
have rw₁ : Module.finrank F K = Module.finrank F K
Tactic: rw [Nat.card_congr (Normal.algHomEquivAut F L K), IsGalois.card_aut_eq_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
inst_6 : Finite K
h : Module.finrank F K ∣ Module.finrank F L
⊢ Fintype.card (K →ₐ[F] L) = Module.finrank F K
have rw : Nat.card (K →ₐ[F] L) = Module.finrank F K
Tactic: rw [Fintype.card_eq_nat_card, natCard_algHom_of_finrank_dvd h]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
inst_6 : Finite K
h : Module.finrank F K ∣ Module.finrank F L
rw : Nat.card (K →ₐ[F] L) = Module.finrank F K
⊢ Fintype.card (K →ₐ[F] L) = Module.finrank F K
have rw₁ : Module.finrank F K = Module.finrank F K
Tactic: rw [Fintype.card_eq_nat_card, natCard_algHom_of_finrank_dvd h]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ Nonempty (K →ₐ[F] L) ↔ Module.finrank F K ∣ Module.finrank F L
have refine : Nonempty (K →ₐ[F] L) → ∀ (f : K →ₐ[F] L), Module.finrank F K ∣ Module.finrank F L
Tactic: refine ⟨fun ⟨f⟩ ↦ ?_, nonempty_algHom_of_finrank_dvd⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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 : Nonempty (K →ₐ[F] L)
f : K →ₐ[F] L
algInst : Algebra K L := f.toAlgebra
⊢ Module.finrank F K ∣ Module.finrank F L
have rw : Module.finrank F K ∣ Module.finrank F K * Module.finrank K L
Tactic: rw [← Module.finrank_mul_finrank F K L]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) f :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) f : MvPolynomial σ (ZMod p))
have C : ∀ (a : ZMod p),
  Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
Tactic: apply induction_on f
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
C :
  ∀ (a : ZMod p),
    Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
          ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
        MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
          ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
        MvPolynomial σ (ZMod p))
⊢ Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) f :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) f : MvPolynomial σ (ZMod p))
have add : ∀ (p_1 q : MvPolynomial σ (ZMod p)),
  Eq (α := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
        MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p)) →
    Eq (α := MvPolynomial σ (ZMod p))
        ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
          MvPolynomial σ (ZMod p))
        ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p)) →
      Eq (α := MvPolynomial σ (ZMod p))
        ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 + q) :
          MvPolynomial σ (ZMod p))
        ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 + q) : MvPolynomial σ (ZMod p))
Tactic: apply induction_on f
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
C :
  ∀ (a : ZMod p),
    Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
          ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
        MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
          ((MvPolynomial.C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
        MvPolynomial σ (ZMod p))
add :
  ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    Eq (α := MvPolynomial σ (ZMod p))
        ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
          MvPolynomial σ (ZMod p))
        ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p)) →
      Eq (α := MvPolynomial σ (ZMod p))
          ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q :
            MvPolynomial σ (ZMod p))
          ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) q : MvPolynomial σ (ZMod p)) →
        Eq (α := MvPolynomial σ (ZMod p))
          ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 + q) :
            MvPolynomial σ (ZMod p))
          ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 + q) : MvPolynomial σ (ZMod p))
⊢ Eq (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) f :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) f : MvPolynomial σ (ZMod p))
have mul_X : ∀ (p_1 : MvPolynomial σ (ZMod p)) (n : σ),
  Eq (α := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 :
        MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) p_1 : MvPolynomial σ (ZMod p)) →
    Eq (α := MvPolynomial σ (ZMod p))
      ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 * X n) :
        MvPolynomial σ (ZMod p))
      ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p)) (p_1 * X n) : MvPolynomial σ (ZMod p))
Tactic: apply induction_on f
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Polynomial (goal)
Goal:
σ : Type u_1
p : ℕ
inst : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
a : ZMod p
⊢ Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
    ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
    ((expand p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
        ((C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
      MvPolynomial σ (ZMod p))
have C : Eq.{u_1 + 1} (α := MvPolynomial σ (ZMod p))
  ((frobenius (MvPolynomial σ (ZMod p)) p : (a : MvPolynomial σ (ZMod p)) → MvPolynomial σ (ZMod p))
      ((C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p)) :
    MvPolynomial σ (ZMod p))
  ((C : (a : ZMod p) → MvPolynomial σ (ZMod p)) a : MvPolynomial σ (ZMod p))
Tactic: rw [expand_C, frobenius_def, ← C_pow, ZMod.pow_card]