awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
a :
  ∀ (σ : (_ : L →ₐ[K] E) × E)
    (hσ :
      Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
        (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
          { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
        σ),
    Eq.{v + 1} (α := E) ((aeval (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) : (a : K[X]) → E) (minpoly K pb.gen) : E) (0 : E)
⊢ Eq.{v + 1} (α := E)
    (∏ x ∈ Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ,
      HSub.hSub (α := E) (β := E)
        ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (x.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
              (a : L) → E)
            pb.gen :
          E)
        ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (x.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
              (a : L) → E)
            pb.gen :
          E))
    (∏
      x ∈
        Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
          { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ },
      HSub.hSub (α := E) ((x.fst (β := fun (i : L →ₐ[K] E) ↦ E) : (a : L) → E) pb.gen : E)
        (x.snd (β := fun (i : L →ₐ[K] E) ↦ E)))
have a₁ : ∀ (a : (_ : Fin pb.dim) × Fin pb.dim)
  (ha :
    Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
      (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) a),
  Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
    (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
      { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := sorry })
    ((fun (i : (_ : Fin pb.dim) × Fin pb.dim)
          (x :
            Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
              (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
        (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
            ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
                (a : L) → E)
              pb.gen) :
          (_ : L →ₐ[K] E) × E))
      a ha)
Tactic: refine prod_bij' (fun i _ ↦ ⟨e i.2, e i.1 pb.gen⟩)
    (fun σ hσ ↦ ⟨e.symm (PowerBasis.lift pb σ.2 ?_), e.symm σ.1⟩) ?_ ?_ ?_ ?_ (fun i _ ↦ by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
σ : (_ : L →ₐ[K] E) × E
hσ :
  Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
    (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
      { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
    σ
⊢ Eq.{v + 1} (α := E) ((aeval (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) : (a : K[X]) → E) (minpoly K pb.gen) : E) (0 : E)
have hroots₁ : ∀ (σ : L →ₐ[K] E),
  Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
    Eq (α := E) (eval ((σ : (a : L) → E) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) : E) (0 : E)
Tactic: simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *
Cleared hypotheses: hroots, hσ
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
σ : (_ : L →ₐ[K] E) × E
hσ :
  Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
    (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
      { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
    σ
hroots₁ :
  ∀ (σ : L →ₐ[K] E),
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      Eq (α := E) (eval ((σ : (a : L) → E) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) : E) (0 : E)
⊢ Eq.{v + 1} (α := E) ((aeval (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) : (a : K[X]) → E) (minpoly K pb.gen) : E) (0 : E)
have hσ₁ : σ.snd (β := fun (i : L →ₐ[K] E) ↦ E) ≠ (σ.fst (β := fun (i : L →ₐ[K] E) ↦ E) : (a : L) → E) pb.gen ∧
  Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
    eval (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
Tactic: simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *
Cleared hypotheses: hroots, hσ
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
⊢ ∀ (a : (_ : Fin pb.dim) × Fin pb.dim)
    (ha :
      Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
        (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) a),
    Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
      (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
        { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
      ((fun (i : (_ : Fin pb.dim) × Fin pb.dim)
            (x :
              Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
                (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
          (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
              ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
                  (a : L) → E)
                pb.gen) :
            (_ : L →ₐ[K] E) × E))
        a ha)
have a : ∀
  (hroots :
    ∀ (σ : L →ₐ[K] E),
      Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
        Eq (α := E) (eval ((σ : (a : L) → E) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) : E) (0 : E))
  (a b : Fin pb.dim) (ha : ¬b = a),
  Ne (α := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) a : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
      ((((e : (a : Fin pb.dim) → L →ₐ[K] E) b : L →ₐ[K] E) : (a : L) → E) pb.gen : E) ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      Eq (α := E)
        (eval ((((e : (a : Fin pb.dim) → L →ₐ[K] E) a : L →ₐ[K] E) : (a : L) → E) pb.gen)
            (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) :
          E)
        (0 : E)
Tactic: simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *
Cleared hypotheses: hroots
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
⊢ ∀ (a : (_ : L →ₐ[K] E) × E)
    (ha :
      Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
        (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
          { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
        a),
    Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
      (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ)
      ((fun (σ : (_ : L →ₐ[K] E) × E)
            (hσ :
              Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
                (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
                  { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
                σ) ↦
          (Sigma.mk (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (pb.lift (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) ⋯))
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (σ.fst (β := fun (i : L →ₐ[K] E) ↦ E))) :
            (_ : Fin pb.dim) × Fin pb.dim))
        a ha)
have a : ∀
  (hroots :
    ∀ (σ : L →ₐ[K] E),
      Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
        Eq (α := E) (eval ((σ : (a : L) → E) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) : E) (0 : E))
  (a : L →ₐ[K] E) (b : E)
  (ha :
    b ≠ (a : (a : L) → E) pb.gen ∧
      Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
        eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0),
  ¬a = pb.lift b sorry
Tactic: simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
⊢ ∀ (a : (_ : Fin pb.dim) × Fin pb.dim)
    (ha :
      Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
        (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) a),
    (fun (σ : (_ : L →ₐ[K] E) × E)
            (hσ :
              Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
                (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
                  { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ })
                σ) ↦
          (Sigma.mk (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (pb.lift (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) ⋯))
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (σ.fst (β := fun (i : L →ₐ[K] E) ↦ E))) :
            (_ : Fin pb.dim) × Fin pb.dim))
        ((fun (i : (_ : Fin pb.dim) × Fin pb.dim)
              (x :
                Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
                  (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
            (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
                ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
                ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
                    (a : L) → E)
                  pb.gen) :
              (_ : L →ₐ[K] E) × E))
          a ha)
        ⋯ =
      a
have a : ∀ (a b : Fin pb.dim) (ha : ¬b = a),
  Eq (α := L →ₐ[K] E)
    (pb.lift ((((e : (a : Fin pb.dim) → L →ₐ[K] E) a : L →ₐ[K] E) : (a : L) → E) pb.gen) sorry : L →ₐ[K] E)
    ((e : (a : Fin pb.dim) → L →ₐ[K] E) a : L →ₐ[K] E)
Tactic: simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots_1 : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
hroots :
  ∀ (σ : L →ₐ[K] E),
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      Eq (α := E) (eval ((σ : (a : L) → E) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) : E) (0 : E)
a : L →ₐ[K] E
b : E
hba :
  b ≠ (a : (a : L) → E) pb.gen ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
ha : a = pb.lift b ⋯
⊢ False
have hba₁ : b ≠ b ∧
  Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
    eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
Tactic: rw [ha, PowerBasis.lift_gen] at hba
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
ι : Type w
inst : DecidableEq ι
inst_1 : Fintype ι
K : Type u
L : Type v
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module.Finite K L
R : Type z
inst_6 : CommRing R
inst_7 : Algebra R K
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (discr K b)
have rw : IsIntegral R (traceMatrix K b).det
Tactic: classical
  rw [discr_def]
  exact IsIntegral.det fun i j ↦ isIntegral_trace ((h i).mul (h j))
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen]
    (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) • z)
have hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
Tactic: have hinv : IsUnit (traceMatrix K B.basis).det := by
    simpa [← discr_def] using discr_isUnit_of_basis _ B.basis
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
⊢ HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
have e_a : Eq (α := Fin B.dim → K)
  (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ (B.basis.equivFun : (a : L) → Fin B.dim → K) z)
  fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen]
    (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) • z)
have H : HSMul.hSMul (β := Fin B.dim → K)
    (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
    (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
  HSMul.hSMul (β := (i : Fin B.dim) → K)
    (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
    (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
Tactic: have H :
    (traceMatrix K B.basis).det • (traceMatrix K B.basis) *ᵥ (B.basis.equivFun z) =
      (traceMatrix K B.basis).det • fun i => trace K L (z * B.basis i) := by
    congr; exact traceMatrix_of_basis_mulVec _ _
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen]
    (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) • z)
have cramer : (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
    (cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) : (a : Fin B.dim → K) → Fin B.dim → K)
      fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
  HSMul.hSMul (β := Fin B.dim → K)
    (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
    (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
Tactic: have cramer := mulVec_cramer (traceMatrix K B.basis) fun i => trace K L (z * B.basis i)
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
cramer :
  (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (Matrix.cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) :
          (a : Fin B.dim → K) → Fin B.dim → K)
        fun (i : Fin B.dim) ↦
        (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
this :
  ∀ (i : Fin B.dim),
    Membership.mem (γ := Subalgebra R K) ⊥
      (HSMul.hSMul (β := Fin B.dim → K)
        (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
        ((B.basis.equivFun : (a : L) → Fin B.dim → K) z : Fin B.dim → K) i)
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen]
    (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) • z)
have rw : Membership.mem (γ := Subalgebra R L) R[B.gen]
  (∑ x : Fin B.dim,
    discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) •
      HSMul.hSMul.{u, v, v} (α := K) (β := L)
        ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) x : K)
        ((B.basis : (a : Fin B.dim) → L) x : L))
Tactic: rw [← B.basis.sum_repr z, Finset.smul_sum]