awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
⊢ 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)
have 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)
Tactic: rwa [ne_eq, inv_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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)
⊢ (∀ (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)
have 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)
Tactic: have hne₂ : (aeval (algebraMap B L x) (derivative (minpoly K (algebraMap B L x))))⁻¹ ≠ 0 := by
    rwa [ne_eq, inv_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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)
⊢ (∀ (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)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)
have 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)
Tactic: refine SetLike.le_def.mp ?_ (Ideal.mem_span_singleton_self _)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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)] ⊤
⊢ 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)
have rw : HMul.hMul (α := Ideal B) (conductor A x) (differentIdeal A B) ≤ differentIdeal A B
Tactic: rw [← conductor_mul_differentIdeal A K L x hx]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
⊢ P ^ (e - 1) ∣ differentIdeal A B
have obtain : ∀ (a : Ideal B) (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a), P ^ (e - 1) ∣ differentIdeal A B
Tactic: obtain ⟨a, ha⟩ := (pow_dvd_pow _ (Nat.sub_le e 1)).trans hP
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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
⊢ P ^ (e - 1) ∣ differentIdeal A B
have hp' : ¬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
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
have habot : a ≠ ⊥
Tactic: have habot : a ≠ ⊥ := fun ha' ↦ hp' (by simpa [ha'] using ha)
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hP : HPow.hPow (α := Ideal B) ⊥ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a
⊢ False
have apply : Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
Tactic: apply hp'
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hP : HPow.hPow (α := Ideal B) ⊥ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a
⊢ Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
have rwa : ∀ (hP : HPow.hPow (α := Ideal B) 0 e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p)
  (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
  Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
Tactic: rwa [← Ideal.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP
Cleared hypotheses: hP, ha
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hP : HPow.hPow (α := Ideal B) ⊥ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a
rwa :
  ∀ (hP : HPow.hPow (α := Ideal B) 0 e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p)
    (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
    Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
⊢ Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
have rwa₁ : ∀ (hP : Dvd.dvd.{u_3} (α := Ideal B) 0 (Ideal.map (F := A →+* B) (algebraMap A B) p))
  (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
  Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
Tactic: rwa [← Ideal.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP
Cleared hypotheses: hP, ha
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hP : HPow.hPow (α := Ideal B) ⊥ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a
rwa :
  ∀ (hP : HPow.hPow (α := Ideal B) 0 e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p)
    (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
    Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
rwa₁ :
  ∀ (hP : Dvd.dvd.{u_3} (α := Ideal B) 0 (Ideal.map (F := A →+* B) (algebraMap A B) p))
    (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
    Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
⊢ Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
have rwa₂ : ∀ (hP : Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) 0)
  (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
  Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
Tactic: rwa [← Ideal.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP
Cleared hypotheses: hP, ha
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hP : HPow.hPow (α := Ideal B) ⊥ e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a
rwa :
  ∀ (hP : HPow.hPow (α := Ideal B) 0 e ∣ Ideal.map (F := A →+* B) (algebraMap A B) p)
    (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
    Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
rwa₁ :
  ∀ (hP : Dvd.dvd.{u_3} (α := Ideal B) 0 (Ideal.map (F := A →+* B) (algebraMap A B) p))
    (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
    Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
rwa₂ :
  ∀ (hP : Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) 0)
    (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
    Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
⊢ Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
have rwa₃ : ∀ (hP : Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥)
  (ha : Ideal.map (F := A →+* B) (algebraMap A B) p = HPow.hPow (α := Ideal B) ⊥ (e - 1) * a),
  Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
Tactic: rwa [← Ideal.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP
Cleared hypotheses: hP, ha
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
⊢ P ^ (e - 1) ∣ differentIdeal A B
have hPbot : P ≠ ⊥
Tactic: have hPbot : P ≠ ⊥ := by
    rintro rfl; apply hp'
    rwa [← Ideal.zero_eq_bot, zero_pow he, zero_dvd_iff, Ideal.zero_eq_bot] at hP
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
have obtain : ∀ (b : Ideal B) (hb : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ e * b),
  Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
Tactic: obtain ⟨b, hb⟩ := hP
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (hypothesis)
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 ≠ ⊥
a : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
hb : Ideal.map (F := A →+* B) (algebraMap A B) p = P ^ e * b
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e
have ha₁ : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = (P ^ (e - 1) * a) ^ e
Tactic: apply_fun (· ^ e : Ideal B → _) at ha
Cleared hypotheses: ha