awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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_1 : Decidable (φ = 1)
this : q - 1 ∣ i ↔ φ = 1
h : φ = 1
⊢ Eq.{u_1 + 1} (α := K) (↑(Fintype.card.{u_1} Kˣ) : K) (-1)
have pos : 1 ≤ q
Tactic: rw [Fintype.card_units, Nat.cast_sub,
              cast_card_eq_zero, Nat.cast_one, zero_sub]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := K) (↑(if φ = 1 then Fintype.card.{u_1} Kˣ else 0) : K) (if q - 1 ∣ i then -1 else 0)
have suffices : q - 1 ∣ i ↔ φ = 1
Tactic: 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⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ q - 1 ∣ i ↔ φ = 1
have rw : (∀ (x : Kˣ), x ^ i = 1) ↔ ∀ (x : Kˣ), Eq (α := K) ((φ : (a : Kˣ) → K) x : K) ((1 : (a : Kˣ) → K) x : K)
Tactic: rw [← forall_pow_eq_one_iff, DFunLike.ext_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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) ↔ ∀ (x : Kˣ), Eq (α := K) ((φ : (a : Kˣ) → K) x : K) ((1 : (a : Kˣ) → K) x : K)
have h : ∀ (a : Kˣ), a ^ i = 1 ↔ Eq (α := K) ((φ : (a : Kˣ) → K) a : K) ((1 : (a : Kˣ) → K) a : K)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : Kˣ, (↑x : K) ^ i) (if q - 1 ∣ i then -1 else 0)
have 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)
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]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
have pos : ∀ (hi : i = 0), Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
Tactic: by_cases hi : i = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
have neg : ∀ (hi : ¬i = 0), Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
Tactic: by_cases hi : i = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
⊢ ¬q - 1 ∣ i
have contrapose! : ∀ (h : q - 1 ∣ i), q - 1 ≤ i
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
have hiq : ¬q - 1 ∣ i
Tactic: have hiq : ¬q - 1 ∣ i := by contrapose! h; exact Nat.le_of_dvd (Nat.pos_of_ne_zero hi) h
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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}
have h₁ : ∀ (x : K), x ∈ map φ univ ↔ Membership.mem (γ := Finset K) (univ \ {0}) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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' := ⋯ }
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
have this : 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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : K, x ^ i) (∑ x ∈ univ \ {0}, x ^ i)
have rw : HAdd.hAdd (α := K) (∑ x ∈ univ \ {0}, x ^ i) (∑ x ∈ {0}, x ^ i) = ∑ x ∈ univ \ {0}, x ^ i
Tactic: rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq (α := K) (∑ x : K, x ^ i) (∑ x ∈ univ \ {0}, x ^ i)
have rw₁ : ∑ x ∈ univ \ {0}, x ^ i + HPow.hPow (α := K) 0 i = ∑ x ∈ univ \ {0}, x ^ i
Tactic: rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq (α := K) (∑ x : K, x ^ i) (∑ x ∈ univ \ {0}, x ^ i)
have rw₂ : HAdd.hAdd (α := K) (∑ x ∈ univ \ {0}, x ^ i) 0 = ∑ x ∈ univ \ {0}, x ^ i
Tactic: rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq (α := K) (∑ x : K, x ^ i) (∑ x ∈ univ \ {0}, x ^ i)
have rw₃ : Eq (α := K) (∑ x ∈ univ \ {0}, x ^ i) (∑ x ∈ univ \ {0}, x ^ i)
Tactic: rw [← sum_sdiff ({0} : Finset K).subset_univ, sum_singleton, zero_pow hi, add_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
have x : Eq (α := K) (∑ x : K, x ^ i) (∑ x ∈ univ \ {0}, x ^ i)
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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
have x₁ : Eq (α := K) (∑ x ∈ univ \ {0}, x ^ i) (∑ x : Kˣ, (↑x : K) ^ i)
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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
have x₂ : Eq.{u_1 + 1} (α := K) (∑ x : Kˣ, (↑x : K) ^ 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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
have have : ¬q - 1 ∣ i
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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
i : ℕ
h : i < q - 1
hi : ¬i = 0
have : ¬q - 1 ∣ i
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
have neg : ∀ (hiq : ¬q - 1 ∣ i), 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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := K) (∑ x : K, x ^ i) 0
have neg₄ : ∀ (hiq : ¬q - 1 ∣ i),
  let φ : Kˣ ↪ K := { toFun := fun (x : Kˣ) ↦ (↑x : K), inj' := sorry };
  ∀ (this : map φ univ = univ \ {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
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨p, _, _, hp, card_eq⟩ := card' K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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 : ℕ)
⊢ 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
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
⊢ 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
have this : CharP R p
Tactic: have : CharP R p := charP_of_injective_algebraMap' K p
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
⊢ 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
have this₁ : ExpChar R p
Tactic: have : ExpChar R p := .prime hp
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 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
have simp : (x + x_1) ^ p ^ (↑w : ℕ) = x ^ p ^ (↑w : ℕ) + x_1 ^ p ^ (↑w : ℕ)
Tactic: simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, powMonoidHom_apply, card_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ Function.Bijective (α := R) (β := R) (⇑(frobeniusAlgHom K R) : (a : R) → R)
have 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)
Tactic: obtain ⟨p', _, n, hp, card_eq⟩ := card' K
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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 : ℕ)
⊢ Function.Bijective (α := R) (β := R) (⇑(frobeniusAlgHom K R) : (a : R) → R)
have rw : Function.Bijective (β := R) fun (x : R) ↦ x ^ p' ^ (↑n : ℕ)
Tactic: rw [coe_frobeniusAlgHom, card_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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 : ℕ)
⊢ Function.Bijective (β := R) fun (x : R) ↦ x ^ p' ^ (↑n : ℕ)
have this : ExpChar K p'
Tactic: have : ExpChar K p' := ExpChar.prime hp
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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'
⊢ Function.Bijective (β := R) fun (x : R) ↦ x ^ p' ^ (↑n : ℕ)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (hypothesis)
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
⊢ Function.Bijective (β := R) fun (x : R) ↦ x ^ p' ^ (↑n : ℕ)
have this₁ : p = p'
Tactic: have := ExpChar.eq ‹_› (expChar_of_injective_algebraMap (algebraMap K R).injective p')
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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'
⊢ Function.Bijective (β := R) fun (x : R) ↦ x ^ p' ^ (↑n : ℕ)
have 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 : ℕ)
Tactic: subst this
Cleared hypotheses: p', left, hp, card_eq, this_1, this
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 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
have 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
Tactic: have := Fintype.ofFinite L
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
have 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)
Tactic: refine ⟨DFunLike.ext _ _ fun x ↦ ?_, fun m lt pos eq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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)
⊢ 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
have refine_2 : ∀ (m : ℕ) (lt : m < Module.finrank K L) (pos : 0 < m) (eq : HPow.hPow (α := L →ₐ[K] L) (frobeniusAlgHom K L) m = 1),
  False
Tactic: refine ⟨DFunLike.ext _ _ fun x ↦ ?_, fun m lt pos eq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 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)
have refine_1 : (⇑(frobeniusAlgHom K L) : (a : L) → L)^[Module.finrank K L] x = (1 : (a : L) → L) x
Tactic: simp_rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply,
        ← Module.card_eq_pow_finrank, pow_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 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)
have refine_1₁ : (fun (x : L) ↦ x ^ q)^[Module.finrank K L] x = (1 : (a : L) → L) x
Tactic: simp_rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply,
        ← Module.card_eq_pow_finrank, pow_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 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)
have refine_1₂ : x ^ q ^ Module.finrank K L = (1 : (a : L) → L) x
Tactic: simp_rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply,
        ← Module.card_eq_pow_finrank, pow_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 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)
have refine_1₃ : x ^ q ^ Module.finrank K L = x
Tactic: simp_rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply,
        ← Module.card_eq_pow_finrank, pow_card]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.Basic (goal)
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
⊢ 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)
have refine_1₄ : x ^ Fintype.card L = x
Tactic: simp_rw [AlgHom.coe_pow, coe_frobeniusAlgHom, pow_iterate, AlgHom.one_apply,
        ← Module.card_eq_pow_finrank, pow_card]