awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₂ : (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
  Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
Tactic: simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₃ : Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₄ : Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₅ : Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
    Finset.card (α := E →ₐ[F] A) Finset.univ ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₅ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₆ : Finset.card.{u_5} (α := A) (Finset.image (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) Finset.univ) =
    Finset.card (α := E →ₐ[F] A) Finset.univ ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₅ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₆ :
  Finset.card.{u_5} (α := A) (Finset.image (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) Finset.univ) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₇ : InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) (↑Finset.univ : Set (E →ₐ[F] A)) ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₅ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₆ :
  Finset.card.{u_5} (α := A) (Finset.image (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) Finset.univ) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₇ :
  InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) (↑Finset.univ : Set (E →ₐ[F] A)) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₈ : InjOn (β := A) (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) univ ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
Tactic: classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₁ : Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
  Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
Tactic: classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₂ : (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
  Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
Tactic: classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₃ : Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₄ : Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₅ : Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
    Finset.card (α := E →ₐ[F] A) Finset.univ ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
inst_4 : Algebra.IsSeparable F E
A : Type u_5
inst_5 : Field A
inst_6 : Algebra F A
hA : ∀ (x : E), Splits (Polynomial.map (algebraMap F A) (minpoly F x))
α : E
simp_rw : natDegree (minpoly F α) = finrank F E ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₁ :
  Fintype.card.{u_5} (↑(rootSet (minpoly F α) A) : Type u_5) = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₂ :
  (rootSet (minpoly F α) A).toFinset.card = finrank F E ↔
    Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
simp_rw₃ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = finrank F E ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₄ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) = Fintype.card (E →ₐ[F] A) ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
simp_rw₅ :
  Finset.card.{u_5} (α := A) (toFinset (range fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α)) =
      Finset.card (α := E →ₐ[F] A) Finset.univ ↔
    Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
⊢ Eq (α := IntermediateField F E) F⟮α⟯ ⊤ ↔ Function.Injective (β := A) fun (φ : E →ₐ[F] A) ↦ (φ : (a : E) → A) α
have simp_rw₆ : Finset.card.{u_5} (α := A) (Finset.image (fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α) Finset.univ) =
    Finset.card (α := E →ₐ[F] A) Finset.univ ↔
  Function.Injective (β := A) fun (ψ : E →ₐ[F] A) ↦ (ψ : (a : E) → A) α
Tactic: classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, injOn_univ]