awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
simp_rw :
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₁ : ∏ σ : Gal(K'/K), (σ : (a : K') → K') x = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₂ :
  ∏ i : Fin (Module.finrank K K'),
      (HPow.hPow (α := Gal(K'/K)) (frobeniusAlgEquivOfAlgebraic K K') (↑i : ℕ) : (a : K') → K') x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₃ :
  ∏ x_1 : Fin (Module.finrank K K'), (⇑(frobeniusAlgEquivOfAlgebraic K K') : (a : K') → K')^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have simp_rw₄ : ∏ x_1 : Fin (Module.finrank K K'), (fun (x : K') ↦ x ^ Fintype.card K)^[(↑x_1 : ℕ)] x =
  x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Tactic: simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
simp_rw :
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₁ : ∏ σ : Gal(K'/K), (σ : (a : K') → K') x = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₂ :
  ∏ i : Fin (Module.finrank K K'),
      (HPow.hPow (α := Gal(K'/K)) (frobeniusAlgEquivOfAlgebraic K K') (↑i : ℕ) : (a : K') → K') x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₃ :
  ∏ x_1 : Fin (Module.finrank K K'), (⇑(frobeniusAlgEquivOfAlgebraic K K') : (a : K') → K')^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₄ :
  ∏ x_1 : Fin (Module.finrank K K'), (fun (x : K') ↦ x ^ Fintype.card K)^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have simp_rw₅ : ∏ x_1 : Fin (Module.finrank K K'), x ^ Fintype.card K ^ (↑x_1 : ℕ) = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Tactic: simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
simp_rw :
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₁ : ∏ σ : Gal(K'/K), (σ : (a : K') → K') x = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₂ :
  ∏ i : Fin (Module.finrank K K'),
      (HPow.hPow (α := Gal(K'/K)) (frobeniusAlgEquivOfAlgebraic K K') (↑i : ℕ) : (a : K') → K') x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₃ :
  ∏ x_1 : Fin (Module.finrank K K'), (⇑(frobeniusAlgEquivOfAlgebraic K K') : (a : K') → K')^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₄ :
  ∏ x_1 : Fin (Module.finrank K K'), (fun (x : K') ↦ x ^ Fintype.card K)^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₅ :
  ∏ x_1 : Fin (Module.finrank K K'), x ^ Fintype.card K ^ (↑x_1 : ℕ) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have simp_rw₆ : HPow.hPow (β := ℕ) x (∑ i : Fin (Module.finrank K K'), Fintype.card K ^ (↑i : ℕ)) =
  x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Tactic: simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
simp_rw :
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₁ : ∏ σ : Gal(K'/K), (σ : (a : K') → K') x = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₂ :
  ∏ i : Fin (Module.finrank K K'),
      (HPow.hPow (α := Gal(K'/K)) (frobeniusAlgEquivOfAlgebraic K K') (↑i : ℕ) : (a : K') → K') x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₃ :
  ∏ x_1 : Fin (Module.finrank K K'), (⇑(frobeniusAlgEquivOfAlgebraic K K') : (a : K') → K')^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₄ :
  ∏ x_1 : Fin (Module.finrank K K'), (fun (x : K') ↦ x ^ Fintype.card K)^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₅ :
  ∏ x_1 : Fin (Module.finrank K K'), x ^ Fintype.card K ^ (↑x_1 : ℕ) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₆ :
  HPow.hPow (β := ℕ) x (∑ i : Fin (Module.finrank K K'), Fintype.card K ^ (↑i : ℕ)) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have simp_rw₇ : HPow.hPow (β := ℕ) x (∑ i ∈ range (Module.finrank K K'), Fintype.card K ^ i) =
  x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Tactic: simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
x : K'
this_1 : Finite K
this_2 : Fintype K
this : Fintype K'
simp_rw :
  (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₁ : ∏ σ : Gal(K'/K), (σ : (a : K') → K') x = x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₂ :
  ∏ i : Fin (Module.finrank K K'),
      (HPow.hPow (α := Gal(K'/K)) (frobeniusAlgEquivOfAlgebraic K K') (↑i : ℕ) : (a : K') → K') x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₃ :
  ∏ x_1 : Fin (Module.finrank K K'), (⇑(frobeniusAlgEquivOfAlgebraic K K') : (a : K') → K')^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₄ :
  ∏ x_1 : Fin (Module.finrank K K'), (fun (x : K') ↦ x ^ Fintype.card K)^[(↑x_1 : ℕ)] x =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₅ :
  ∏ x_1 : Fin (Module.finrank K K'), x ^ Fintype.card K ^ (↑x_1 : ℕ) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₆ :
  HPow.hPow (β := ℕ) x (∑ i : Fin (Module.finrank K K'), Fintype.card K ^ (↑i : ℕ)) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
simp_rw₇ :
  HPow.hPow (β := ℕ) x (∑ i ∈ range (Module.finrank K K'), Fintype.card K ^ i) =
    x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
⊢ (algebraMap K K' : (a : K) → K') ((Algebra.norm K : (a : K') → K) x : K) = x ^ ((Nat.card K' - 1) / (Nat.card K - 1))
have simp_rw₈ : x ^ ((Fintype.card K ^ Module.finrank K K' - 1) / (Fintype.card K - 1)) =
  x ^ ((Fintype.card K' - 1) / (Fintype.card K - 1))
Tactic: simp_rw [← Fintype.card_eq_nat_card, Algebra.norm_eq_prod_automorphisms,
    ← (bijective_frobeniusAlgEquivOfAlgebraic_pow K K').prod_comp, AlgEquiv.coe_pow,
    coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, Finset.prod_pow_eq_pow_sum,
    Fin.sum_univ_eq_sum_range, Nat.geomSum_eq Fintype.one_lt_card, ← Module.card_eq_pow_finrank]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ Nat.card.{u_2} K'ˣ / Nat.card.{u_1} Kˣ
have simp_rw : Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
Tactic: simp_rw [Nat.card_units]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
have have : ∀ (this : Fintype K'ˣ),
  Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
Tactic: have := Fintype.ofFinite K'ˣ
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
have h : Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) =
  Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}
Tactic: convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) =
    Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}
have h : (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ).ncard =
  (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ).ncard
Tactic: rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
⊢ (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ).ncard =
    (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ).ncard
have h : (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) =
  (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this_1 : Finite K
this : Fintype K'ˣ
⊢ (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) =
    (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
have h : ∀ (x : K'ˣ),
  x ∈ (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) ↔
    x ∈ (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
have have : ∀ (this : Fintype K'ˣ),
  Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
Tactic: classical
    have := Fintype.ofFinite K'ˣ
    convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card
    rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]; congr 1; ext
    simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
have have₁ have₂ :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
have h : ∀ (this : Fintype K'ˣ),
  Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) =
    Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}
Tactic: classical
    have := Fintype.ofFinite K'ˣ
    convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card
    rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]; congr 1; ext
    simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
have have₁ have₂ :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
h :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) =
      Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
have h₁ : ∀ (this : Fintype K'ˣ),
  (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ).ncard =
    (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ).ncard
Tactic: classical
    have := Fintype.ofFinite K'ˣ
    convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card
    rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]; congr 1; ext
    simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
have have₁ have₂ :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
h :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) =
      Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}
h₁ h₂ :
  ∀ (this : Fintype K'ˣ),
    (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ).ncard =
      (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ).ncard
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
have h₃ : ∀ (this : Fintype K'ˣ),
  (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) =
    (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
Tactic: classical
    have := Fintype.ofFinite K'ˣ
    convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card
    rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]; congr 1; ext
    simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
this : Finite K
have have₁ have₂ :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
h :
  ∀ (this : Fintype K'ˣ),
    Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) =
      Finset.card.{u_2} (α := K'ˣ) {a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1}
h₁ h₂ :
  ∀ (this : Fintype K'ˣ),
    (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ).ncard =
      (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ).ncard
h₃ h₄ :
  ∀ (this : Fintype K'ˣ),
    (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) =
      (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
⊢ Nat.card.{u_2} ↥(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) ≤ (Nat.card K' - 1) / (Nat.card K - 1)
have h₅ : ∀ (this : Fintype K'ˣ) (x : K'ˣ),
  x ∈ (↑(MonoidHom.ker (M := Kˣ) (Units.map (Algebra.norm K))) : Set K'ˣ) ↔
    x ∈ (↑{a : K'ˣ | a ^ ((Nat.card K' - 1) / (Nat.card K - 1)) = 1} : Set K'ˣ)
Tactic: classical
    have := Fintype.ofFinite K'ˣ
    convert!
      IsCyclic.card_pow_eq_one_le (α := K'ˣ) <|
        Nat.div_pos
            (Nat.sub_le_sub_right (Nat.card_le_card_of_injective _ (algebraMap K K').injective)
              _) <|
          Nat.sub_pos_of_lt Finite.one_lt_card
    rw [← Set.ncard_coe_finset, ← SetLike.coe_sort_coe, Nat.card_coe_set_eq]; congr 1; ext
    simp [Units.ext_iff, ← (algebraMap K K').injective.eq_iff, algebraMap_norm_eq_pow]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k
have inl : ∃ (a : K'), Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : K') → K) a : K) (0 : K)
Tactic: obtain rfl | ne := eq_or_ne k 0
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
Goal:
K : Type u_1
K' : Type u_2
inst : Field K
inst_1 : Field K'
inst_2 : Algebra K K'
inst_3 : Finite K'
k : K
inl : ∃ (a : K'), Eq.{u_1 + 1} (α := K) ((Algebra.norm K : (a : K') → K) a : K) (0 : K)
⊢ ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k
have inr : ∀ (ne : k ≠ 0), ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k
Tactic: obtain rfl | ne := eq_or_ne k 0
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (goal)
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
⊢ ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k
have inr : ∀ (x : K'ˣ) (eq : Eq.{u_1 + 1} (α := Kˣ) ((Units.map (Algebra.norm K) : (a : K'ˣ) → Kˣ) x : Kˣ) (Units.mk0 k ne : Kˣ)),
  ∃ (a : K'), (Algebra.norm K : (a : K') → K) a = k
Tactic: have ⟨x, eq⟩ := unitsMap_norm_surjective K K' (Units.mk0 k ne)
-- 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'
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
have rw : CharP (ZMod p) p
Tactic: rw [← Algebra.charP_iff (ZMod p) K p]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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'
⊢ K ≃ₐ[ZMod p] K'
have this : CharP K p
Tactic: have : CharP K p := by rw [← Algebra.charP_iff (ZMod p) K p]; exact ZMod.charP p
-- 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'
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
have rw : CharP (ZMod p) p
Tactic: rw [← Algebra.charP_iff (ZMod p) K' p]
-- Lean 4 proof step from Mathlib.FieldTheory.Finite.GaloisField (hypothesis)
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
⊢ K ≃ₐ[ZMod p] K'
have this₁ : CharP K' p
Tactic: have : CharP K' p := by rw [← Algebra.charP_iff (ZMod p) K' p]; exact ZMod.charP p
-- 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'
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
⊢ K ≃ₐ[ZMod p] K'
have choose : (n : ℕ+) → (a : Nat.Prime p) → (hK : Fintype.card K = p ^ (↑n : ℕ)) → K ≃ₐ[ZMod p] K'
Tactic: choose n a 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'
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 : ℕ)
⊢ K ≃ₐ[ZMod p] K'
have choose : (n' : ℕ+) → (a' : Nat.Prime p) → (hK' : Fintype.card K' = p ^ (↑n' : ℕ)) → K ≃ₐ[ZMod p] K'
Tactic: choose n' a' 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'
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' : ℕ)
⊢ K ≃ₐ[ZMod p] K'
have 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'
Tactic: rw [hK, hK'] at hKK'
Cleared hypotheses: hKK', a, hK, n', a', hK'