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 : 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) ⊥
ha' : a = ⊥
⊢ Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥

Tactic:
simpa [ha'] using ha
-- 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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
⊢ a ≠ ⊥

Tactic:
have habot : a ≠ ⊥ := fun ha' ↦ hp' (by simpa [ha'] using ha)
-- 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
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
apply : Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
⊢ False

Tactic:
apply hp'
-- 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
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) ⊥
rwa₃ rwa₄ rwa₅ 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) ⊥
⊢ 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

Premises used: zero_dvd_iff, Ideal.zero_eq_bot, zero_pow
-- 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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
⊢ 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
-- 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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
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
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e

Tactic:
obtain ⟨b, hb⟩ := hP
-- 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 ≠ ⊥
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
⊢ 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

Premises used: HPow.hPow
-- 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 ≠ ⊥
a : Ideal B
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
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = (P ^ (e - 1) * a) ^ e
⊢ HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = (P ^ e * b) ^ (e - 1)

Tactic:
apply_fun (· ^ (e - 1) : Ideal B → _) at hb

Premises used: HSub.hSub, HPow.hPow, 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 : 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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = (P ^ (e - 1) * a) ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = (P ^ e * b) ^ (e - 1)
⊢ HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = P ^ ((e - 1) * e) * a ^ e

Tactic:
simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb

Premises used: pow_mul, mul_comm, mul_pow
-- 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 ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = (P ^ (e - 1) * a) ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = (P ^ e * b) ^ (e - 1)
ha₁ : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = P ^ ((e - 1) * e) * a ^ e
⊢ HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)

Tactic:
simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb

Premises used: pow_mul, mul_comm, mul_pow
-- 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 ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = P ^ ((e - 1) * e) * a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
rw : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1 + 1)
| HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e

Tactic:
rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]

Premises used: Iff.mpr, Nat.sub_add_cancel, Nat.one_le_iff_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 : 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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = P ^ ((e - 1) * e) * a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1 + 1) = P ^ ((e - 1) * e) * a ^ e

Tactic:
conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]

Premises used: Iff.mpr, Nat.sub_add_cancel, Nat.one_le_iff_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 : 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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) e = P ^ ((e - 1) * e) * a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
ha₁ : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1 + 1) = P ^ ((e - 1) * e) * a ^ e
⊢ HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)

Tactic:
conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]

Premises used: Iff.mpr, Nat.sub_add_cancel, Nat.one_le_iff_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 : 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
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1 + 1) = P ^ ((e - 1) * e) * a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p * b ^ (e - 1) = a ^ e

Tactic:
rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha

Premises used: mul_assoc, pow_add, pow_ne_zero, pow_one, mul_comm, mul_right_inj'
-- 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 ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1 + 1) = P ^ ((e - 1) * e) * a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
ha₁ : Ideal.map (F := A →+* B) (algebraMap A B) p * b ^ (e - 1) = a ^ e
⊢ HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)

Tactic:
rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha

Premises used: mul_assoc, pow_add, pow_ne_zero, pow_one, mul_comm, mul_right_inj'
-- 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 ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p * b ^ (e - 1) = a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e

Tactic:
⟨_, ha.symm⟩

Premises used: Exists.intro, Eq.symm
-- 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 ≠ ⊥
a : Ideal B
hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
b : Ideal B
ha : Ideal.map (F := A →+* B) (algebraMap A B) p * b ^ (e - 1) = a ^ e
hb : HPow.hPow (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) p) (e - 1) = P ^ ((e - 1) * e) * b ^ (e - 1)
⊢ Ideal.map (F := A →+* B) (algebraMap A B) p ∣ a ^ e

Tactic:
exact ⟨_, ha.symm⟩
-- 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
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

Tactic:
have : p.map (algebraMap A B) ∣ a ^ e := by
    obtain ⟨b, hb⟩ := hP
    apply_fun (· ^ e : Ideal B → _) at ha
    apply_fun (· ^ (e - 1) : Ideal B → _) at hb
    simp only [mul_pow, ← pow_mul, mul_comm e] at ha hb
    conv_lhs at ha => rw [← Nat.sub_add_cancel (Nat.one_le_iff_ne_zero.mpr he)]
    rw [pow_add, hb, mul_assoc, mul_right_inj' (pow_ne_zero _ hPbot), pow_one, mul_comm] at ha
    exact ⟨_, ha.symm⟩