awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
⊢ Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)

Tactic:
have : algebraMap B L (aeval x (derivative (minpoly A x))) ≠ 0 := by
    rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
      aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this_1 : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
this :
  Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)
a :
  (∀ (z : B),
      Membership.mem (γ := Subalgebra A L) A[((algebraMap B L : (a : B) → L) x : L)]
        (HMul.hMul (β := L) y ((algebraMap B L : (a : B) → L) z : L))) ↔
    ∀ (a : L),
      Membership.mem (γ := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 a →
        Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
          ((((traceForm K L : (a : L) → L →ₗ[K] K)
                    (HMul.hMul (α := L)
                      (((algebraMap B L : (a : B) → L)
                            ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) :
                              B))⁻¹ :
                        L)
                      y) :
                  L →ₗ[K] K) :
                (a : L) → K)
              a :
            K)
a₁ : Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0
⊢ Membership.mem (γ := Submodule B L) (coeSubmodule L (conductor A x)) y ↔
    y ∈
      HSMul.hSMul (α := L) (β := Submodule B L)
        ((algebraMap B L : (a : B) → L)
            ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
          L)
        (↑(FractionalIdeal.dual A K 1) : Submodule B L)

Tactic:
rw [Submodule.mem_smul_iff_inv_mul_mem this, FractionalIdeal.mem_coe, FractionalIdeal.mem_dual,
    mem_coeSubmodule_conductor]

Premises used: Submodule.mem_smul_iff_inv_mul_mem, FractionalIdeal.mem_dual, mem_coeSubmodule_conductor, FractionalIdeal.mem_coe
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this_1 : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
this :
  Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this_1 : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
this :
  Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)
⊢ Ne.{u + 1} (α := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this_1 : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
this :
  Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)
rwa :
  ¬Eq.{u + 1} (α := L)
      ((((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
            ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
              K[X]))⁻¹ :
        L)
      (0 : L)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ¬Eq.{u + 1} (α := L)
      (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
          ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
            K[X]) :
        L)
      (0 : L)
⊢ Ne.{u + 1} (α := L)
    ((((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
          ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
            K[X]))⁻¹ :
      L)
    (0 : L)

Tactic:
rwa [ne_eq, inv_eq_zero]

Premises used: inv_eq_zero, ne_eq
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this_1 : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
this :
  Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)
⊢ Ne.{u + 1} (α := L)
    ((((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
          ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
            K[X]))⁻¹ :
      L)
    (0 : L)

Tactic:
have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0 := by
    rwa [ne_eq, inv_eq_zero]
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this_1 : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
this :
  Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)
hne₂ :
  Ne.{u + 1} (α := L)
    ((((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
          ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
            K[X]))⁻¹ :
      L)
    (0 : L)
⊢ IsIntegral.{u_1, u} A (A := L) ((algebraMap B L : (a : B) → L) x : L)

Tactic:
have : IsIntegral A (algebraMap B L x) := IsIntegral.map (IsScalarTower.toAlgHom A B L) hAx
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this_1 : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
this_2 :
  Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)
hne₂ :
  Ne.{u + 1} (α := L)
    ((((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
          ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
            K[X]))⁻¹ :
      L)
    (0 : L)
this : IsIntegral.{u_1, u} A (A := L) ((algebraMap B L : (a : B) → L) x : L)
⊢ (∀ (z a : B),
      Membership.mem (γ := Subalgebra A B) A[x] a →
        Membership.mem (α := K) (γ := Submodule A K) (LinearMap.range (Algebra.linearMap A K))
          ((Algebra.trace K L : (a : L) → K)
              (HMul.hMul (α := L)
                (((algebraMap B L : (a : B) → L)
                      ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B))⁻¹ :
                  L)
                (HMul.hMul (β := L) y ((algebraMap B L : (a : B) → L) (z * a) : L))) :
            K)) ↔
    ∀ (a : B),
      Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (α := L)
              (((algebraMap B L : (a : B) → L)
                    ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B))⁻¹ :
                L)
              (HMul.hMul (β := L) y ((algebraMap B L : (a : B) → L) a : L))) :
          K)

Tactic:
⟨fun H b ↦ (mul_one b) ▸ H b 1 (one_mem _), fun H _ _ _ ↦ H _⟩

Premises used: HMul.hMul, Algebra.adjoin, Eq.rec, Iff.intro, OneMemClass.one_mem, mul_one, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this_1 : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
this_2 :
  Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)
hne₂ :
  Ne.{u + 1} (α := L)
    ((((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
          ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) :
            K[X]))⁻¹ :
      L)
    (0 : L)
this : IsIntegral.{u_1, u} A (A := L) ((algebraMap B L : (a : B) → L) x : L)
⊢ (∀ (z a : B),
      Membership.mem (γ := Subalgebra A B) A[x] a →
        Membership.mem (α := K) (γ := Submodule A K) (LinearMap.range (Algebra.linearMap A K))
          ((Algebra.trace K L : (a : L) → K)
              (HMul.hMul (α := L)
                (((algebraMap B L : (a : B) → L)
                      ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B))⁻¹ :
                  L)
                (HMul.hMul (β := L) y ((algebraMap B L : (a : B) → L) (z * a) : L))) :
            K)) ↔
    ∀ (a : B),
      Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (α := L)
              (((algebraMap B L : (a : B) → L)
                    ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B))⁻¹ :
                L)
              (HMul.hMul (β := L) y ((algebraMap B L : (a : B) → L) a : L))) :
          K)

Tactic:
exact ⟨fun H b ↦ (mul_one b) ▸ H b 1 (one_mem _), fun H _ _ _ ↦ H _⟩
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
⊢ Membership.mem (α := B) (γ := Ideal B) (differentIdeal A B)
    ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B)

Tactic:
SetLike.le_def.mp ?_ (Ideal.mem_span_singleton_self _)

Premises used: SetLike.le_def, Iff.mp, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
refine :
  LE.le (α := Ideal B)
    (Ideal.span
      (singleton (α := B) ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B)))
    (differentIdeal A B)
⊢ Membership.mem (α := B) (γ := Ideal B) (differentIdeal A B)
    ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B)

Tactic:
refine SetLike.le_def.mp ?_ (Ideal.mem_span_singleton_self _)

Premises used: SetLike.le_def, Iff.mp, Ideal.mem_span_singleton_self
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
rw : HMul.hMul (α := Ideal B) (conductor A x) (differentIdeal A B) ≤ differentIdeal A B
⊢ LE.le (α := Ideal B)
    (Ideal.span
      (singleton (α := B) ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B)))
    (differentIdeal A B)

Tactic:
rw [← conductor_mul_differentIdeal A K L x hx]

Premises used: conductor_mul_differentIdeal
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
⊢ HMul.hMul (α := Ideal B) (conductor A x) (differentIdeal A B) ≤ differentIdeal A B

Tactic:
Ideal.mul_le_left

Premises used: Set.Mem, Ideal.mul_le_left
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
⊢ HMul.hMul (α := Ideal B) (conductor A x) (differentIdeal A B) ≤ differentIdeal A B

Tactic:
exact Ideal.mul_le_left

Premises used: Ideal.mul_le_left
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
obtain :
  ∀ (a : Ideal B) (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a), P ^ (e - 1) ∣ differentIdeal A B
⊢ P ^ (e - 1) ∣ differentIdeal A B

Tactic:
obtain ⟨a, ha⟩ := (pow_dvd_pow _ (Nat.sub_le e 1)).trans hP

Premises used: pow_dvd_pow, Nat.sub_le, OfNat.ofNat, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsFractionRing B L
inst_17 : IsDedekindDomain A
inst_18 : IsDedekindDomain B
inst_19 : IsTorsionFree A B
inst_20 : Module.Finite A B
p : Ideal A
inst_21 : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
⊢ ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥

Tactic:
have hp' := (Ideal.map_eq_bot_iff_of_injective
    (FaithfulSMul.algebraMap_injective A B)).not.mpr hp