awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun (x : Kˣ) ↦ (↑x : K) ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
x : Kˣ
⊢ x ^ i = 1 ↔ Eq (α := K) ((φ : (a : Kˣ) → K) x : K) ((1 : (a : Kˣ) → K) x : K)

Tactic:
simp [φ, Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
inst_2 : DecidableEq K
i : ℕ
φ : Kˣ →* K := { toFun := fun (x : Kˣ) ↦ (↑x : K) ^ i, map_one' := ⋯, map_mul' := ⋯ }
this : Decidable (φ = 1)
calc : Eq.{u_1 + 1} (α := K) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K) (if q - 1 ∣ i then -1 else 0)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : Kˣ, (↑x : K) ^ i) (if q - 1 ∣ i then -1 else 0)

Tactic:
calc (∑ x : Kˣ, φ x) = if φ = 1 then Fintype.card Kˣ else 0 := sum_hom_units φ
      _ = if q - 1 ∣ i then -1 else 0 := by
        suffices q - 1 ∣ i ↔ φ = 1 by
          simp only [this]
          split_ifs; swap
          · exact Nat.cast_zero
          · rw [Fintype.card_units, Nat.cast_sub,
              cast_card_eq_zero, Nat.cast_one, zero_sub]
            show 1 ≤ q; exact Fintype.card_pos_iff.mpr ⟨0⟩
        rw [← forall_pow_eq_one_iff, DFunLike.ext_iff]
        apply forall_congr'; intro x; simp [φ, Units.ext_iff]

Premises used: sum_hom_units, Finset.univ, Units, Fintype.card, DFunLike.coe, Finset.sum
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
pos : ∀ (hi : i = 0), Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
neg : ∀ (hi : ¬i = 0), Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0

Tactic:
by_cases hi : i = 0
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : i = 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0

Tactic:
simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero]

Premises used: Finset.card_univ, FiniteField.cast_card_eq_zero, pow_zero, nsmul_one, Finset.sum_const
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
contrapose! : ∀ (h : q - 1 ∣ i), q - 1 ≤ i
⊢ ¬q - 1 ∣ i

Tactic:
contrapose! h
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i

Tactic:
Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h

Premises used: Nat.pos_of_ne_zero, Nat.le_of_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
hi : ¬i = 0
h : q - 1 ∣ i
⊢ q - 1 ≤ i

Tactic:
exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h

Premises used: Nat.pos_of_ne_zero, Nat.le_of_dvd
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ¬q - 1 ∣ i

Tactic:
have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ }
h₁ : ∀ (x : K), x ∈ map φ univ ↔ Membership.mem (γ := Finset K) (univ \ {0}) x
⊢ map φ univ = univ \ {0}

Tactic:
ext x
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ }
x : K
⊢ x ∈ map φ univ ↔ Membership.mem (γ := Finset K) (univ \ {0}) x

Tactic:
simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff,
        mem_singleton, φ] using isUnit_iff_ne_zero

Premises used: Finset.mem_univ, Finset.mem_singleton, isUnit_iff_ne_zero, Finset.mem_sdiff, Function.Embedding.coeFn_mk, Finset.mem_map, true_and
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ }
⊢ map φ univ = univ \ {0}

Tactic:
have : univ.map φ = univ \ {0} := by
      ext x
      simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff,
        mem_singleton, φ] using isUnit_iff_ne_zero
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ }
this : map φ univ = univ \ {0}
rw : HAdd.hAdd (α := K) (∑ x ∈ univ \ {0}, x ^ i) (∑ x ∈ {0}, x ^ i) = ∑ x ∈ univ \ {0}, x ^ i
rw₁ : ∑ x ∈ univ \ {0}, x ^ i + HPow.hPow (α := K) 0 i = ∑ x ∈ univ \ {0}, x ^ i
rw₂ : HAdd.hAdd (α := K) (∑ x ∈ univ \ {0}, x ^ i) 0 = ∑ x ∈ univ \ {0}, x ^ i
rw₃ rw₄ : Eq (α := K) (∑ x ∈ univ \ {0}, x ^ i) (∑ x ∈ univ \ {0}, x ^ i)
⊢ Eq (α := K) (∑ x : K, x ^ i) (∑ x ∈ univ \ {0}, x ^ i)

Tactic:
rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]

Premises used: Finset.sum_singleton, add_zero, Singleton.singleton, OfNat.ofNat, zero_pow, Finset.subset_univ, Finset.sum_sdiff
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ Eq (α := K) (∑ x ∈ univ \ {0}, x ^ i) (∑ x : Kˣ, (↑x : K) ^ i)

Tactic:
simp [φ, ← this, univ.sum_map φ]

Premises used: Finset.univ, Finset.sum_map
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ }
this : map φ univ = univ \ {0}
hnc : ¬q - 1 ∣ i
⊢ Eq.{u_1 + 1} (α := K) (∑ x : Kˣ, (↑x : K) ^ i) 0

Tactic:
rw [sum_pow_units K i, if_neg]

Premises used: FiniteField.sum_pow_units, if_neg
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ¬q - 1 ∣ i

Tactic:
hiq
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ }
this : map φ univ = univ \ {0}
⊢ ¬q - 1 ∣ i

Tactic:
exact hiq
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
hiq : ¬q - 1 ∣ i
φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ }
this : map φ univ = univ \ {0}
x : Eq (α := K) (∑ x : K, x ^ i) (∑ x ∈ univ \ {0}, x ^ i)
x₁ : Eq (α := K) (∑ x ∈ univ \ {0}, x ^ i) (∑ x : Kˣ, (↑x : K) ^ i)
x₂ : Eq.{u_1 + 1} (α := K) (∑ x : Kˣ, (↑x : K) ^ i) 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0

Tactic:
calc
      ∑ x : K, x ^ i = ∑ x ∈ univ \ {(0 : K)}, x ^ i := by
        rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
      _ = ∑ x : Kˣ, (x ^ i : K) := by simp [φ, ← this, univ.sum_map φ]
      _ = 0 := by rw [sum_pow_units K i, if_neg]; exact hiq

Premises used: Finset.univ, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
have : ¬q - 1 ∣ i
neg : ∀ (hiq : ¬q - 1 ∣ i), Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
have₁ : ¬q - 1 ∣ i
neg₁ neg₂ neg₃ : ∀ (hiq : ¬q - 1 ∣ i), Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
neg₄ :
  ∀ (hiq : ¬q - 1 ∣ i),
    let φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := ⋯ };
    ∀ (this : map φ univ = univ \ {0}), Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0

Tactic:
classical
    have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
    let φ : Kˣ ↪ K := ⟨fun x ↦ x, Units.val_injective⟩
    have : univ.map φ = univ \ {0} := by
      ext x
      simpa only [mem_map, mem_univ, Function.Embedding.coeFn_mk, true_and, mem_sdiff,
        mem_singleton, φ] using isUnit_iff_ne_zero
    calc
      ∑ x : K, x ^ i = ∑ x ∈ univ \ {(0 : K)}, x ^ i := by
        rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
      _ = ∑ x : Kˣ, (x ^ i : K) := by simp [φ, ← this, univ.sum_map φ]
      _ = 0 := by rw [sum_pow_units K i, if_neg]; exact hiq

Premises used: Finset.univ, OfNat.ofNat
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
x x_1 : R
obtain :
  ∀ (p : ℕ),
    CharP K p →
      ∀ (w : ℕ+) (hp : Nat.Prime p) (card_eq : q = p ^ (↑w : ℕ)),
        OneHom.toFun (↑(powMonoidHom q) : OneHom R R) (x + x_1) =
          OneHom.toFun (↑(powMonoidHom q) : OneHom R R) x + OneHom.toFun (↑(powMonoidHom q) : OneHom R R) x_1
⊢ OneHom.toFun (↑(powMonoidHom q) : OneHom R R) (x + x_1) =
    OneHom.toFun (↑(powMonoidHom q) : OneHom R R) x + OneHom.toFun (↑(powMonoidHom q) : OneHom R R) x_1

Tactic:
obtain ⟨p, _, _, hp, card_eq⟩ := card' K

Premises used: FiniteField.card'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
x x_1 : R
p : ℕ
left : CharP K p
w : ℕ+
hp : Nat.Prime p
card_eq : q = p ^ (↑w : ℕ)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
x x_1 : R
p : ℕ
left : CharP K p
w : ℕ+
hp : Nat.Prime p
card_eq : q = p ^ (↑w : ℕ)
h : Nontrivial R
⊢ CharP R p

Tactic:
have : CharP R p := charP_of_injective_algebraMap' K p
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
x x_1 : R
p : ℕ
left : CharP K p
w : ℕ+
hp : Nat.Prime p
card_eq : q = p ^ (↑w : ℕ)
h : Nontrivial R
this : CharP R p
⊢ ExpChar R p

Tactic:
have : ExpChar R p := .prime hp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
x x_1 : R
p : ℕ
left : CharP K p
w : ℕ+
hp : Nat.Prime p
card_eq : q = p ^ (↑w : ℕ)
h : Nontrivial R
this_1 : CharP R p
this : ExpChar R p
simp : (x + x_1) ^ p ^ (↑w : ℕ) = x ^ p ^ (↑w : ℕ) + x_1 ^ p ^ (↑w : ℕ)
⊢ OneHom.toFun (↑(powMonoidHom q) : OneHom R R) (x + x_1) =
    OneHom.toFun (↑(powMonoidHom q) : OneHom R R) x + OneHom.toFun (↑(powMonoidHom q) : OneHom R R) x_1

Tactic:
simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, powMonoidHom_apply, card_eq]

Premises used: MonoidHom.toOneHom_coe, powMonoidHom_apply, OneHom.toFun_eq_coe
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
x x_1 : R
p : ℕ
left : CharP K p
w : ℕ+
hp : Nat.Prime p
card_eq : q = p ^ (↑w : ℕ)
h : Nontrivial R
this_1 : CharP R p
this : ExpChar R p
⊢ (x + x_1) ^ p ^ (↑w : ℕ) = x ^ p ^ (↑w : ℕ) + x_1 ^ p ^ (↑w : ℕ)

Tactic:
add_pow_expChar_pow ..

Premises used: add_pow_expChar_pow
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
x x_1 : R
p : ℕ
left : CharP K p
w : ℕ+
hp : Nat.Prime p
card_eq : q = p ^ (↑w : ℕ)
h : Nontrivial R
this_1 : CharP R p
this : ExpChar R p
⊢ (x + x_1) ^ p ^ (↑w : ℕ) = x ^ p ^ (↑w : ℕ) + x_1 ^ p ^ (↑w : ℕ)

Tactic:
exact add_pow_expChar_pow ..

Premises used: add_pow_expChar_pow
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
x : K
⊢ Eq.{u_2 + 1} (α := R) (OneHom.toFun (↑(powMonoidHom q) : OneHom R R) ((algebraMap K R : (a : K) → R) x) : R)
    ((algebraMap K R : (a : K) → R) x : R)

Tactic:
simp [← map_pow, pow_card]

Premises used: map_pow, FiniteField.pow_card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
⊢ Eq (α := (a : R) → R) (⇑(frobeniusAlgHom K R) : (a : R) → R) fun (x : R) ↦ x ^ q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
p : ℕ
inst_4 : ExpChar R p
inst_5 : PerfectRing R p
obtain :
  ∀ (p' : ℕ),
    CharP K p' →
      ∀ (n : ℕ+) (hp : Nat.Prime p') (card_eq : q = p' ^ (↑n : ℕ)),
        Function.Bijective (α := R) (β := R) (⇑(frobeniusAlgHom K R) : (a : R) → R)
⊢ Function.Bijective (α := R) (β := R) (⇑(frobeniusAlgHom K R) : (a : R) → R)

Tactic:
obtain ⟨p', _, n, hp, card_eq⟩ := card' K

Premises used: FiniteField.card'
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
p : ℕ
inst_4 : ExpChar R p
inst_5 : PerfectRing R p
p' : ℕ
left : CharP K p'
n : ℕ+
hp : Nat.Prime p'
card_eq : q = p' ^ (↑n : ℕ)
rw : Function.Bijective (β := R) fun (x : R) ↦ x ^ p' ^ (↑n : ℕ)
⊢ Function.Bijective (α := R) (β := R) (⇑(frobeniusAlgHom K R) : (a : R) → R)

Tactic:
rw [coe_frobeniusAlgHom, card_eq]

Premises used: FiniteField.coe_frobeniusAlgHom
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
p : ℕ
inst_4 : ExpChar R p
inst_5 : PerfectRing R p
p' : ℕ
left : CharP K p'
n : ℕ+
hp : Nat.Prime p'
card_eq : q = p' ^ (↑n : ℕ)
⊢ ExpChar K p'

Tactic:
have : ExpChar K p' := ExpChar.prime hp
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
p : ℕ
inst_4 : ExpChar R p
inst_5 : PerfectRing R p
p' : ℕ
left : CharP K p'
n : ℕ+
hp : Nat.Prime p'
card_eq : q = p' ^ (↑n : ℕ)
this : ExpChar K p'
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
p : ℕ
inst_4 : ExpChar R p
inst_5 : PerfectRing R p
p' : ℕ
left : CharP K p'
n : ℕ+
hp : Nat.Prime p'
card_eq : q = p' ^ (↑n : ℕ)
this : ExpChar K p'
h : Nontrivial R
⊢ p = p'

Tactic:
have := ExpChar.eq ‹_› (expChar_of_injective_algebraMap (algebraMap K R).injective p')
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
p : ℕ
inst_4 : ExpChar R p
inst_5 : PerfectRing R p
p' : ℕ
left : CharP K p'
n : ℕ+
hp : Nat.Prime p'
card_eq : q = p' ^ (↑n : ℕ)
this_1 : ExpChar K p'
h : Nontrivial R
this : p = p'
subst :
  CharP K p →
    ∀ (hp : Nat.Prime p) (card_eq : q = p ^ (↑n : ℕ)) (this : ExpChar K p),
      Function.Bijective (β := R) fun (x : R) ↦ x ^ p ^ (↑n : ℕ)
⊢ Function.Bijective (β := R) fun (x : R) ↦ x ^ p' ^ (↑n : ℕ)

Tactic:
subst this
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
R : Type u_2
inst : Field K
inst_1 : Fintype K
inst_2 : CommRing R
inst_3 : Algebra K R
p : ℕ
inst_4 : ExpChar R p
inst_5 : PerfectRing R p
n : ℕ+
h : Nontrivial R
left : CharP K p
hp : Nat.Prime p
card_eq : q = p ^ (↑n : ℕ)
this : ExpChar K p
⊢ Function.Bijective (β := R) fun (x : R) ↦ x ^ p ^ (↑n : ℕ)

Tactic:
apply bijective_iterateFrobenius

Premises used: bijective_iterateFrobenius
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsAlgebraic K L
⊢ Eq (α := (a : L) → L) (⇑(frobeniusAlgEquivOfAlgebraic K L) : (a : L) → L) fun (x : L) ↦ x ^ q

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra.IsAlgebraic K L
n : ℕ
⊢ Eq (α := L → L) (⇑(frobeniusAlgEquivOfAlgebraic K L) : (a : L) → L)^[n] fun (x : L) ↦ x ^ q ^ n

Tactic:
pow_iterate (Fintype.card K) n

Premises used: pow_iterate, Fintype.card
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
have :
  ∀ (this : Fintype L),
    HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) (Module.finrank K L) = 1 ∧
      ∀ m < Module.finrank K L, 0 < m → HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m ≠ 1
⊢ HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) (Module.finrank K L) = 1 ∧
    ∀ m < Module.finrank K L, 0 < m → HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m ≠ 1

Tactic:
have := Fintype.ofFinite L
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this : Fintype L
⊢ HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) (Module.finrank K L) = 1 ∧
    ∀ m < Module.finrank K L, 0 < m → HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m ≠ 1

Tactic:
⟨DFunLike.ext _ _ fun x ↦ ?_, fun m lt pos eq ↦ ?_⟩

Premises used: DFunLike.ext, And.intro
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this : Fintype L
refine_1 :
  ∀ (x : L),
    Eq (α := L) ((HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) (Module.finrank K L) : (a : L) → L) x : L)
      ((1 : (a : L) → L) x : L)
refine_2 :
  ∀ (m : ℕ) (lt : m < Module.finrank K L) (pos : 0 < m) (eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1),
    False
⊢ HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) (Module.finrank K L) = 1 ∧
    ∀ m < Module.finrank K L, 0 < m → HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m ≠ 1

Tactic:
refine ⟨DFunLike.ext _ _ fun x ↦ ?_, fun m lt pos eq ↦ ?_⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this : Fintype L
x : L
refine_1 : (⇑(frobeniusAlgHom K L) : (a : L) → L)^[Module.finrank K L] x = (1 : (a : L) → L) x
refine_1₁ : (fun (x : L) ↦ x ^ q)^[Module.finrank K L] x = (1 : (a : L) → L) x
refine_1₂ : x ^ q ^ Module.finrank K L = (1 : (a : L) → L) x
refine_1₃ : x ^ q ^ Module.finrank K L = x
refine_1₄ : x ^ Fintype.card L = x
⊢ Eq (α := L) ((HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) (Module.finrank K L) : (a : L) → L) x : L)
    ((1 : (a : L) → L) x : L)

Tactic:
simp_rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply,
        ← Module.card_eq_pow_finrank, pow_card]

Premises used: pow_iterate, Module.card_eq_pow_finrank, AlgHom.one_apply, FiniteField.pow_card, FiniteField.coe_frobeniusAlgHom, AlgHom.coe_pow
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
x : L
h : Membership.mem (γ := Multiset L) (val univ) x
simp_rw : HPow.hPow (α := L[X]) X (q ^ m) - X ≠ 0 ∧ x ^ q ^ m - x = 0
⊢ x ∈ (HPow.hPow (α := L[X]) X (q ^ m) - X).roots

Tactic:
simp_rw [mem_roots', IsRoot, eval_sub, eval_pow, eval_X]

Premises used: Polynomial.eval_X, Polynomial.eval_pow, Polynomial.IsRoot, Polynomial.mem_roots', Polynomial.eval_sub
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
x : L
h : Membership.mem (γ := Multiset L) (val univ) x
⊢ Eq (α := L) ((HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m : (a : L) → L) x : L) ((1 : (a : L) → L) x : L)

Tactic:
have := DFunLike.congr_fun eq x
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this_1 : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
x : L
h : Membership.mem (γ := Multiset L) (val univ) x
this : Eq (α := L) ((HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m : (a : L) → L) x : L) ((1 : (a : L) → L) x : L)
⊢ (fun (x : L) ↦ x ^ q ^ m) x - x = 0

Tactic:
rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply, ← sub_eq_zero] at this

Premises used: pow_iterate, sub_eq_zero, AlgHom.one_apply, FiniteField.coe_frobeniusAlgHom, AlgHom.coe_pow
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this_1 : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
x : L
h : Membership.mem (γ := Multiset L) (val univ) x
this : (fun (x : L) ↦ x ^ q ^ m) x - x = 0
⊢ HPow.hPow (α := L[X]) X (q ^ m) - X ≠ 0 ∧ x ^ q ^ m - x = 0

Tactic:
⟨fun h ↦ ?_, this⟩

Premises used: And.intro
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this_1 : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
x : L
h : Membership.mem (γ := Multiset L) (val univ) x
this : (fun (x : L) ↦ x ^ q ^ m) x - x = 0
refine : ∀ (h : HPow.hPow (α := L[X]) X (q ^ m) - X = 0), False
⊢ HPow.hPow (α := L[X]) X (q ^ m) - X ≠ 0 ∧ x ^ q ^ m - x = 0

Tactic:
refine ⟨fun h ↦ ?_, this⟩
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this_1 : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
x : L
h_1 : Membership.mem (γ := Multiset L) (val univ) x
this : (fun (x : L) ↦ x ^ q ^ m) x - x = 0
h : HPow.hPow (α := L[X]) X (q ^ m) - X = 0
⊢ False

Tactic:
simpa [Fintype.one_lt_card.ne, pos.ne, eqComm] using congr_arg (coeff · 1) h

Premises used: Fintype.one_lt_card, Polynomial.coeff, congr_arg, OfNat.ofNat, LT.lt.ne, eqComm
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
⊢ Finset.card.{u_3} (α := L) univ ≤ (HPow.hPow (α := L[X]) X (q ^ m) - X).natDegree

Tactic:
have := card_le_degree_of_subset_roots (R := L) (p := X ^ q ^ m - X) (Z := univ) fun x _ ↦ by
      simp_rw [mem_roots', IsRoot, eval_sub, eval_pow, eval_X]
      have := DFunLike.congr_fun eq x
      rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply, ← sub_eq_zero] at this
      refine ⟨fun h ↦ ?_, this⟩
      simpa [Fintype.one_lt_card.ne, pos.ne, eqComm] using congr_arg (coeff · 1) h
-- Module: Mathlib.FieldTheory.Finite.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
L : Type u_3
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Finite L
this_1 : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1
this : Finset.card.{u_3} (α := L) univ ≤ (HPow.hPow (α := L[X]) X (q ^ m) - X).natDegree
⊢ False

Tactic:
this.not_gt (((natDegree_sub_le ..).trans_eq ?_).trans_lt <|
      (Nat.pow_lt_pow_right Fintype.one_lt_card lt).trans_eq Module.card_eq_pow_finrank.symm)

Premises used: Fintype.one_lt_card, LE.le.trans_eq, Module.card_eq_pow_finrank, LT.lt.trans_eq, LE.le.not_gt, Eq.symm, LE.le.trans_lt, Polynomial.natDegree_sub_le, Nat.pow_lt_pow_right