awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
⊢ differentIdeal A C =
    HMul.hMul (α := Ideal C) (differentIdeal B C) (Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B))
have this₁ : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)
Tactic: haveI : FiniteDimensional (FractionRing A) (FractionRing C) := .of_isLocalization A C A⁰
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
this : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)
⊢ differentIdeal A C =
    HMul.hMul (α := Ideal C) (differentIdeal B C) (Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B))
have this₁ : FiniteDimensional.{u_4, u_3} (FractionRing B) (FractionRing C)
Tactic: haveI : FiniteDimensional (FractionRing B) (FractionRing C) := .of_isLocalization B C B⁰
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)
this : FiniteDimensional.{u_4, u_3} (FractionRing B) (FractionRing C)
⊢ differentIdeal A C =
    HMul.hMul (α := Ideal C) (differentIdeal B C) (Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B))
have rw : (dual A (FractionRing A) 1)⁻¹ =
  HMul.hMul (α := FractionalIdeal (R := C) C⁰ (FractionRing C)) (dual B (FractionRing B) 1)⁻¹
    (↑(Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B)) : FractionalIdeal C⁰ (FractionRing C))
Tactic: rw [← coeIdeal_inj (K := FractionRing C), coeIdeal_mul, coeIdeal_differentIdeal A
    (FractionRing A), coeIdeal_differentIdeal B (FractionRing B)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
C : Type u_3
inst_7 : IsDomain B
inst_8 : CommRing C
inst_9 : Algebra B C
inst_10 : Algebra A C
inst_11 : IsDedekindDomain C
inst_12 : Module.Finite A B
inst_13 : Module.Finite A C
inst_14 : Module.Finite B C
inst_15 : IsTorsionFree A C
inst_16 : IsTorsionFree B C
inst_17 : IsScalarTower A B C
inst_18 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing C)
this_1 : Algebra.IsSeparable.{u_4, u_3} (FractionRing B) (FractionRing C)
this_2 : Algebra.IsSeparable.{u_1, u_4} (FractionRing A) (FractionRing B)
this_3 : FiniteDimensional.{u_1, u_4} (FractionRing A) (FractionRing B)
this_4 : FiniteDimensional.{u_1, u_3} (FractionRing A) (FractionRing C)
this : FiniteDimensional.{u_4, u_3} (FractionRing B) (FractionRing C)
⊢ (dual A (FractionRing A) 1)⁻¹ =
    HMul.hMul (α := FractionalIdeal (R := C) C⁰ (FractionRing C)) (dual B (FractionRing B) 1)⁻¹
      (↑(Ideal.map (F := B →+* C) (algebraMap B C) (differentIdeal A B)) : FractionalIdeal C⁰ (FractionRing C))
have rw : dual A (FractionRing A) 1 =
  HMul.hMul (α := FractionalIdeal (R := C) C⁰ (FractionRing C)) (β := FractionalIdeal (R := C) C⁰ (FractionRing C))
    (dual B (FractionRing B) 1)
    ((extendedHom (FractionRing C) C : (a : FractionalIdeal B⁰ (FractionRing B)) → FractionalIdeal C⁰ (FractionRing C))
        (dual A (FractionRing A) 1) :
      FractionalIdeal (R := C) C⁰ (FractionRing C))
Tactic: rw [← extendedHom_coeIdeal_eq_map (K := FractionRing B), coeIdeal_differentIdeal A
    (FractionRing A), map_inv₀, ← mul_inv, ← inv_eq_iff_eq_inv, inv_inv]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
⊢ LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x]) =
    HSMul.hSMul (α := L) (β := Submodule A L)
      (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
have hKx : IsIntegral K x
Tactic: have hKx : IsIntegral K x := Algebra.IsIntegral.isIntegral x
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
⊢ LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x]) =
    HSMul.hSMul (α := L) (β := Submodule A L)
      (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
have pbgen : pb.gen = x
Tactic: have pbgen : pb.gen = x := by simp [pb]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
⊢ LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x]) =
    HSMul.hSMul (α := L) (β := Submodule A L)
      (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
have hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
Tactic: have hnondeg : (traceForm K L).Nondegenerate := traceForm_nondegenerate K L
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
⊢ LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x]) =
    HSMul.hSMul (α := L) (β := Submodule A L)
      (((aeval x : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K x) : K[X]))⁻¹ : L)
      ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
have hpb : Eq.{u + 1} (α := (a : Fin pb.dim) → L)
  (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
        Basis (Fin pb.dim) K L) :
    (a : Fin pb.dim) → L)
  fun (x : Fin pb.dim) ↦
  HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
    ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
Tactic: have hpb : ⇑(LinearMap.BilinForm.dualBasis (traceForm K L) hnondeg pb.basis) = _ :=
    _root_.funext (Basis.traceDual_powerBasis_eq pb)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
⊢ Eq (α := Submodule A L) ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L) A[x] : Submodule A L)
    (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) : Submodule A L)
have rw : Eq (α := Submodule A L)
  (span A (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L))
  (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)))
Tactic: rw [← span_range_natDegree_eq_adjoin (minpoly.monic hAx) (minpoly.aeval _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
⊢ Eq (α := Submodule A L)
    (span A (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L))
    (span A (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)))
have e_s : (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L) =
  Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
⊢ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L) =
    Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)
have e_s : ∀ (y : L),
  y ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L) ↔
    Membership.mem (γ := Set L) (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
⊢ natDegree (minpoly A x) = natDegree (minpoly K x)
have rw : natDegree (minpoly A x) = natDegree (Polynomial.map (algebraMap A K) (minpoly A x))
Tactic: rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
rw : natDegree (minpoly A x) = natDegree (Polynomial.map (algebraMap A K) (minpoly A x))
⊢ natDegree (minpoly A x) = natDegree (minpoly K x)
have rw₁ : natDegree (minpoly A x) = natDegree (minpoly A x)
Tactic: rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
⊢ y ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L) ↔
    Membership.mem (γ := Set L) (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) y
have this : natDegree (minpoly A x) = natDegree (minpoly K x)
Tactic: have : natDegree (minpoly A x) = natDegree (minpoly K x) := by
      rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
this : natDegree (minpoly A x) = natDegree (minpoly K x)
⊢ y ∈ (↑(Finset.image (fun (x_1 : ℕ) ↦ x ^ x_1) (Finset.range (natDegree (minpoly A x)))) : Set L) ↔
    Membership.mem (γ := Set L) (Set.range (ι := Fin pb.dim) (⇑pb.basis : (a : Fin pb.dim) → L)) y
have e_s : (∃ x_1 < natDegree (minpoly A x), x ^ x_1 = y) ↔ ∃ (y_1 : Fin pb.dim), x ^ (↑y_1 : ℕ) = y
Tactic: simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio, Set.mem_range,
      pb.basis_eq_pow, pbgen]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u
inst : CommRing A
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : Algebra K L
inst_5 : Algebra A L
inst_6 : IsScalarTower A K L
inst_7 : IsDomain A
inst_8 : IsFractionRing A K
inst_9 : FiniteDimensional K L
inst_10 : Algebra.IsSeparable K L
inst_11 : IsIntegrallyClosed A
x : L
hx : Eq (α := Subalgebra K L) K[x] ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map ((Subalgebra.equivOfEq K[x] ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hnondeg : LinearMap.BilinForm.Nondegenerate (traceForm K L)
hpb :
  Eq.{u + 1} (α := (a : Fin pb.dim) → L)
    (⇑(LinearMap.BilinForm.dualBasis.{u, u_2, 0} (V := L) (K := K) (ι := Fin pb.dim) (traceForm K L) hnondeg pb.basis :
          Basis (Fin pb.dim) K L) :
      (a : Fin pb.dim) → L)
    fun (x : Fin pb.dim) ↦
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑x : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
y : L
this : natDegree (minpoly A x) = natDegree (minpoly K x)
⊢ (∃ x_1 < natDegree (minpoly A x), x ^ x_1 = y) ↔ ∃ (y_1 : Fin pb.dim), x ^ (↑y_1 : ℕ) = y
have e_s : (∃ x_1 < natDegree (minpoly K x), x ^ x_1 = y) ↔ ∃ (y_1 : Fin pb.dim), x ^ (↑y_1 : ℕ) = y
Tactic: simp only [this]