awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi_1 : IsSuccPrelimit i
hi : ¬Nonempty.{v + 1} (↑(Iio i) : Type v)
top :
  ∀ (hi : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤)
    (hi : ¬Nonempty.{v + 1} (↑(Iio ⊤) : Type v)),
    Eq.{v + 1} (α := IntermediateField F E)
      ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
      (⊥ : IntermediateField F E)
⊢ Eq (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i : IntermediateField F E)
    (⊥ : IntermediateField F E)
have coe : ∀ (a : (Module.rank F E).ord.ToType) (hi : IsSuccPrelimit (↑a : WithTop (Module.rank F E).ord.ToType))
  (hi : ¬Nonempty.{v + 1} (↑(Iio (↑a : WithTop (Module.rank F E).ord.ToType)) : Type v)),
  Eq (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
        (↑a : WithTop (Module.rank F E).ord.ToType) :
      IntermediateField F E)
    (⊥ : IntermediateField F E)
Tactic: cases i
Cleared hypotheses: i, hi_1, hi
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
hi_1 : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
hi : ¬Nonempty.{v + 1} (↑(Iio ⊤) : Type v)
⊢ Eq.{v + 1} (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
    (⊥ : IntermediateField F E)
have this : Nonempty.{v + 1} (Module.rank F E).ord.ToType
Tactic: have := mk_ne_zero_iff.mp (rank_pos.trans_eq (mk_ord_toType <| Module.rank F E).symm).ne'
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
hi_1 : IsSuccPrelimit.{v} (α := WithTop (Module.rank F E).ord.ToType) ⊤
hi : ¬Nonempty.{v + 1} (↑(Iio ⊤) : Type v)
this : Nonempty.{v + 1} (Module.rank F E).ord.ToType
⊢ Eq.{v + 1} (α := IntermediateField F E)
    ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) ⊤ : IntermediateField F E)
    (⊥ : IntermediateField F E)
have hi₁ : ¬Nonempty.{v + 1} (↑(range WithTop.some) : Type v)
Tactic: rw [← range_coe] at hi
Cleared hypotheses: hi, this
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f :
  (↑(limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
              IntermediateField F E) →ₐ[F]
          Ē)
        (embFunctor F E) i) :
    Type v)
h : Nonempty.{v + 1} (↑(Iio i) : Type v)
⊢ LE.le.{v} (α := Subalgebra F E)
    (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i))
    (⨆ (x : (↑(Iio i) : Type v)),
      toSubalgebra
        ((fun (j : (↑(Iio i) : Type v)) ↦
            ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                (↑j : WithTop (Module.rank F E).ord.ToType) :
              IntermediateField F E))
          x))
have rw : LE.le.{v} (α := Subalgebra F E)
  (toSubalgebra
    (⨆ (j : (↑(Iio i) : Type v)),
      (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
        (↑j : WithTop (Module.rank F E).ord.ToType)))
  (⨆ (x : (↑(Iio i) : Type v)),
    toSubalgebra
      ((fun (j : (↑(Iio i) : Type v)) ↦
          ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
              (↑j : WithTop (Module.rank F E).ord.ToType) :
            IntermediateField F E))
        x))
Tactic: rw [← iSup_filtration hi, toSubalgebra_iSup_of_directed directed_filtration]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst_3 : Algebra.IsAlgebraic F E
i : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f :
  (↑(limit (F := fun (j : WithTop (Module.rank F E).ord.ToType) ↦
        ↥((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) j :
              IntermediateField F E) →ₐ[F]
          Ē)
        (embFunctor F E) i) :
    Type v)
h : Nonempty.{v + 1} (↑(Iio i) : Type v)
rw :
  LE.le.{v} (α := Subalgebra F E)
    (toSubalgebra
      (⨆ (j : (↑(Iio i) : Type v)),
        (filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
          (↑j : WithTop (Module.rank F E).ord.ToType)))
    (⨆ (x : (↑(Iio i) : Type v)),
      toSubalgebra
        ((fun (j : (↑(Iio i) : Type v)) ↦
            ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                (↑j : WithTop (Module.rank F E).ord.ToType) :
              IntermediateField F E))
          x))
⊢ LE.le.{v} (α := Subalgebra F E)
    (toSubalgebra ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E) i))
    (⨆ (x : (↑(Iio i) : Type v)),
      toSubalgebra
        ((fun (j : (↑(Iio i) : Type v)) ↦
            ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
                (↑j : WithTop (Module.rank F E).ord.ToType) :
              IntermediateField F E))
          x))
have rw₁ : LE.le.{v} (α := Subalgebra F E)
  (⨆ (i_1 : (↑(Iio i) : Type v)),
    toSubalgebra
      ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
        (↑i_1 : WithTop (Module.rank F E).ord.ToType)))
  (⨆ (i_1 : (↑(Iio i) : Type v)),
    toSubalgebra
      ((filtration : (a : WithTop (Module.rank F E).ord.ToType) → IntermediateField F E)
        (↑i_1 : WithTop (Module.rank F E).ord.ToType)))
Tactic: rw [← iSup_filtration hi, toSubalgebra_iSup_of_directed directed_filtration]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
have this : Fact (ℵ₀ ≤ Module.rank F E)
Tactic: haveI := Fact.mk rank_inf
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
have rw : (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
    #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) =
  HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
Tactic: rw [Emb.Cardinal.embEquivPi.cardinal_eq, mk_pi]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) =
    HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
have a : (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
    #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
  HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
a :
  (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
⊢ (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) =
    HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
have a₁ : HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E) ≤
  Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦ #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
have a : (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
    #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
  ℵ₀ ^ Module.rank F E
Tactic: rw [← power_eq_two_power rank_inf natCast_le_aleph0 rank_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
| ℵ₀ ^ Module.rank F E
have rw : Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ ℵ₀
Tactic: rw [← mk_ord_toType (Module.rank F E), ← prod_const']
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
    ℵ₀ ^ Module.rank F E
have a : (Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
    #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))) ≤
  Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ ℵ₀
Tactic: conv_rhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
| HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
have rw : Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ 2
Tactic: rw [← mk_ord_toType (Module.rank F E), ← prod_const']
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E) ≤
    Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦
      #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))
have a : (Cardinal.prod fun (x : (Module.rank F E).ord.ToType) ↦ 2) ≤
  Cardinal.prod fun (i : (Module.rank F E).ord.ToType) ↦ #(Cardinal.factor (↑i : WithTop (Module.rank F E).ord.ToType))
Tactic: conv_lhs => rw [← mk_ord_toType (Module.rank F E), ← prod_const']
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
⊢ #(Emb F E) = if ℵ₀ ≤ Module.rank F E then HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E) else Module.rank F E
have pos : ∀ (h : ℵ₀ ≤ Module.rank F E), #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
pos : ∀ (h : ℵ₀ ≤ Module.rank F E), #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E)
⊢ #(Emb F E) = if ℵ₀ ≤ Module.rank F E then HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F E) else Module.rank F E
have neg : ∀ (h : ¬ℵ₀ ≤ Module.rank F E), #(Emb F E) = Module.rank F E
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (hypothesis)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : ¬ℵ₀ ≤ Module.rank F E
⊢ #(Emb F E) = Module.rank F E
have h₁ : IsNoetherian F E
Tactic: rw [not_le, ← IsNoetherian.iff_rank_lt_aleph0] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : IsNoetherian F E
⊢ #(Emb F E) = Module.rank F E
have neg : #(Emb F E) = (↑(finrank F E) : Cardinal.{v})
Tactic: rw [← Module.finrank_eq_rank, ← toNat_eq_iff Module.finrank_pos.ne',
    ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : IsNoetherian F E
neg : #(Emb F E) = (↑(finrank F E) : Cardinal.{v})
⊢ #(Emb F E) = Module.rank F E
have neg₁ : (toNat : (a : Cardinal.{v}) → ℕ) #(Emb F E) = finrank F E
Tactic: rw [← Module.finrank_eq_rank, ← toNat_eq_iff Module.finrank_pos.ne',
    ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : IsNoetherian F E
neg : #(Emb F E) = (↑(finrank F E) : Cardinal.{v})
neg₁ : (toNat : (a : Cardinal.{v}) → ℕ) #(Emb F E) = finrank F E
⊢ #(Emb F E) = Module.rank F E
have neg₂ : Nat.card.{v} (Emb F E) = finrank F E
Tactic: rw [← Module.finrank_eq_rank, ← toNat_eq_iff Module.finrank_pos.ne',
    ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : IsNoetherian F E
neg : #(Emb F E) = (↑(finrank F E) : Cardinal.{v})
neg₁ : (toNat : (a : Cardinal.{v}) → ℕ) #(Emb F E) = finrank F E
neg₂ : Nat.card.{v} (Emb F E) = finrank F E
⊢ #(Emb F E) = Module.rank F E
have neg₃ : finSepDegree F E = finrank F E
Tactic: rw [← Module.finrank_eq_rank, ← toNat_eq_iff Module.finrank_pos.ne',
    ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsSeparable F E
h : IsNoetherian F E
neg : #(Emb F E) = (↑(finrank F E) : Cardinal.{v})
neg₁ : (toNat : (a : Cardinal.{v}) → ℕ) #(Emb F E) = finrank F E
neg₂ : Nat.card.{v} (Emb F E) = finrank F E
neg₃ : finSepDegree F E = finrank F E
⊢ #(Emb F E) = Module.rank F E
have neg₄ : finrank F E = finrank F E
Tactic: rw [← Module.finrank_eq_rank, ← toNat_eq_iff Module.finrank_pos.ne',
    ← Nat.card, ← finSepDegree, finSepDegree_eq_finrank_of_isSeparable]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
rank_inf : ℵ₀ ≤ sepDegree F E
⊢ #(Emb F E) = HPow.hPow (α := Cardinal.{v}) 2 (sepDegree F E)
have rw : HPow.hPow (α := Cardinal.{v}) 2 (Module.rank F ↥(separableClosure F E)) =
  HPow.hPow (α := Cardinal.{v}) 2 (sepDegree F E)
Tactic: rw [← cardinal_separableClosure, cardinal_eq_two_pow_rank rank_inf]
-- Lean 4 proof step from Mathlib.FieldTheory.CardinalEmb (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
⊢ #(Emb F E) = (fun (c : Cardinal.{v}) ↦ if ℵ₀ ≤ c then HPow.hPow (α := Cardinal.{v}) 2 c else c) (sepDegree F E)
have rw : Eq.{v + 2} (α := Cardinal.{v})
  ((fun (c : Cardinal.{v}) ↦ if ℵ₀ ≤ c then HPow.hPow (α := Cardinal.{v}) 2 c else c)
    (Module.rank F ↥(separableClosure F E)))
  ((fun (c : Cardinal.{v}) ↦ if ℵ₀ ≤ c then HPow.hPow (α := Cardinal.{v}) 2 c else c) (sepDegree F E))
Tactic: rw [← cardinal_separableClosure, cardinal_eq_of_isSeparable]
-- Lean 4 proof step from Mathlib.FieldTheory.Cardinality (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ Nonempty.{u_1 + 1} (Field α) ↔ IsPrimePow ‖α‖
have refine : IsPrimePow ‖α‖ → Nonempty.{u_1 + 1} (Field α)
Tactic: refine ⟨fun ⟨h⟩ => Fintype.isPrimePow_card_of_field, ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Cardinality (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
⊢ Nonempty.{u_1 + 1} (Field α)
have this : Fact (Nat.Prime p)
Tactic: haveI := Fact.mk hp.nat_prime
-- Lean 4 proof step from Mathlib.FieldTheory.Cardinality (goal)
Goal:
α : Type u_1
inst : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this : Fact (Nat.Prime p)
⊢ Nonempty.{u_1 + 1} (Field α)
have haveI : ∀ (this : Fintype (GaloisField p n)), Nonempty.{u_1 + 1} (Field α)
Tactic: haveI : Fintype (GaloisField p n) := Fintype.ofFinite (GaloisField p n)
-- Lean 4 proof step from Mathlib.FieldTheory.Cardinality (goal)
Goal:
α : Type u
inst : Infinite α
⊢ Nonempty.{u + 1} (Field α)
have suffices : #α = #(FractionRing (MvPolynomial α (ULift.{u, 0} ℚ)))
Tactic: suffices #α = #(FractionRing (MvPolynomial α <| ULift.{u} ℚ)) from
    (Cardinal.eq.1 this).map (·.field)
-- Lean 4 proof step from Mathlib.FieldTheory.Cardinality (goal)
Goal:
α : Type u
⊢ Nonempty.{u + 1} (Field α) ↔ IsPrimePow #α
have rw : Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n
Tactic: rw [Cardinal.isPrimePow_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Cardinality (goal)
Goal:
α : Type u
⊢ Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n
have inl : ∀ (h : Fintype α), Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n
Tactic: obtain h | h := fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.FieldTheory.Cardinality (goal)
Goal:
α : Type u
inl : ∀ (h : Fintype α), Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n
⊢ Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n
have inr : ∀ (h : Infinite α), Nonempty.{u + 1} (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ (n : ℕ), #α = (↑n : Cardinal.{u}) ∧ IsPrimePow n
Tactic: obtain h | h := fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) f) 0
have haveI : ∀ (this : DecidableEq K), Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) f) 0
Tactic: haveI : DecidableEq K := Classical.decEq K
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, (eval x : (a : MvPolynomial σ K) → K) f) 0
have eval : ∀ x ∈ f.support,
  Eq.{u_1 + 1} (α := K) (∑ x_1 : σ → K, coeff x f * ∏ i : σ, HPow.hPow (β := ℕ) (x_1 i) ((x : (a : σ) → ℕ) i : ℕ)) 0
Tactic: calc
    ∑ x, eval x f = ∑ x : σ → K, ∑ d ∈ f.support, f.coeff d * ∏ i, x i ^ d i := by
      simp only [eval_eq']
    _ = ∑ d ∈ f.support, ∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i := sum_comm
    _ = 0 := sum_eq_zero ?_
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0
have obtain : ∀ (i : σ) (hi : (d : (a : σ) → ℕ) i < q - 1),
  Eq.{u_1 + 1} (α := K) (∑ x : σ → K, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0
Tactic: obtain ⟨i, hi⟩ : ∃ i, d i < q - 1 := f.exists_degree_lt (q - 1) h hd
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, coeff d f * ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0
have x : Eq.{u_1 + 1} (α := K) (∑ x : σ → K, ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0
Tactic: calc
    (∑ x : σ → K, f.coeff d * ∏ i, x i ^ d i) = f.coeff d * ∑ x : σ → K, ∏ i, x i ^ d i :=
      (mul_sum ..).symm
    _ = 0 := (mul_eq_zero.mpr ∘ Or.inr) ?_
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
⊢ Eq.{u_1 + 1} (α := K) (∑ x : σ → K, ∏ i : σ, HPow.hPow (β := ℕ) (x i) ((d : (a : σ) → ℕ) i : ℕ)) 0
have x : ∀ (a : { j : σ // j ≠ i } → K),
  Eq.{u_1 + 1} (α := K)
    (∑ x : { x : σ → K // x ∘ Subtype.val = a }, ∏ j : σ, HPow.hPow (β := ℕ) ((↑x : σ → K) j) ((d : (a : σ) → ℕ) j : ℕ))
    0
Tactic: calc
    (∑ x : σ → K, ∏ i, x i ^ d i) =
        ∑ x₀ : { j // j ≠ i } → K, ∑ x : { x : σ → K // x ∘ (↑) = x₀ }, ∏ j, (x : σ → K) j ^ d j :=
      (Fintype.sum_fiberwise _ _).symm
    _ = 0 := Fintype.sum_eq_zero _ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x₀ : { j : σ // j ≠ i } → K
e : K ≃ { x : σ → K // x ∘ Subtype.val (p := fun (j : σ) ↦ j ≠ i) = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ ∑ a : K,
      (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
        HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ) =
    HMul.hMul (α := K) (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ))
      (∑ a : K, HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ))
have rw : Eq.{u_1 + 1} (α := K)
  (∑ a : K,
    (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
      HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ))
  (∑ i_1 : K,
    (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) *
      HPow.hPow (β := ℕ) i_1 ((d : (a : σ) → ℕ) i : ℕ))
Tactic: rw [mul_sum]
-- Lean 4 proof step from Mathlib.FieldTheory.ChevalleyWarning (goal)
Goal:
K : Type u_1
σ : Type u_2
inst : Fintype K
inst_1 : Field K
inst_2 : Fintype σ
inst_3 : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : (d : (a : σ) → ℕ) i < q - 1
x₀ : { j : σ // j ≠ i } → K
e : K ≃ { x : σ → K // x ∘ Subtype.val (p := fun (j : σ) ↦ j ≠ i) = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
⊢ HMul.hMul (α := K) (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ))
      (∑ a : K, HPow.hPow (β := ℕ) a ((d : (a : σ) → ℕ) i : ℕ)) =
    0
have rw : HMul.hMul (α := K) (∏ j : { j : σ // j ≠ i }, HPow.hPow (β := ℕ) (x₀ j) ((d : (a : σ) → ℕ) (↑j : σ) : ℕ)) 0 = 0
Tactic: rw [sum_pow_lt_card_sub_one K _ hi, mul_zero]