awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
neg : (↑m ! : A)⁻¹ʳ * x ^ m * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₁ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₂ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₃ :
  (↑m ! : A)⁻¹ʳ * (x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₄ : (↑m ! : A)⁻¹ʳ * (x ^ m * (↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₅ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ m * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₆ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * (x ^ m * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
Tactic: rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
neg : (↑m ! : A)⁻¹ʳ * x ^ m * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₁ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₂ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₃ :
  (↑m ! : A)⁻¹ʳ * (x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₄ : (↑m ! : A)⁻¹ʳ * (x ^ m * (↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₅ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ m * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₆ :
  (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * (x ^ m * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₇ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ (m + k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
Tactic: rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
neg : (↑m ! : A)⁻¹ʳ * x ^ m * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₁ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₂ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₃ :
  (↑m ! : A)⁻¹ʳ * (x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₄ : (↑m ! : A)⁻¹ʳ * (x ^ m * (↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₅ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ m * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₆ :
  (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * (x ^ m * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₇ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ (m + k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₈ : (↑m ! : A)⁻¹ʳ * HMul.hMul (α := A) (↑k ! : A)⁻¹ʳ 0 = (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
Tactic: rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
neg : (↑m ! : A)⁻¹ʳ * x ^ m * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₁ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₂ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₃ :
  (↑m ! : A)⁻¹ʳ * (x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₄ : (↑m ! : A)⁻¹ʳ * (x ^ m * (↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₅ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ m * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₆ :
  (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * (x ^ m * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₇ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ (m + k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₈ :
  (↑m ! : A)⁻¹ʳ * HMul.hMul (α := A) (↑k ! : A)⁻¹ʳ 0 =
    (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₉ : HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ 0 = (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
Tactic: rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
neg : (↑m ! : A)⁻¹ʳ * x ^ m * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₁ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₂ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₃ :
  (↑m ! : A)⁻¹ʳ * (x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₄ : (↑m ! : A)⁻¹ʳ * (x ^ m * (↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₅ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ m * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₆ :
  (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * (x ^ m * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₇ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ (m + k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₈ :
  (↑m ! : A)⁻¹ʳ * HMul.hMul (α := A) (↑k ! : A)⁻¹ʳ 0 =
    (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
neg₉ : HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ 0 = (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₁₀ : 0 = (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
Tactic: rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
neg : (↑m ! : A)⁻¹ʳ * x ^ m * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₁ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₂ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₃ :
  (↑m ! : A)⁻¹ʳ * (x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₄ : (↑m ! : A)⁻¹ʳ * (x ^ m * (↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₅ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ m * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₆ :
  (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * (x ^ m * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₇ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ (m + k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₈ :
  (↑m ! : A)⁻¹ʳ * HMul.hMul (α := A) (↑k ! : A)⁻¹ʳ 0 =
    (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
neg₉ : HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ 0 = (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
neg₁₀ : 0 = (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₁₁ : 0 = HMul.hMul (α := A) (↑((m + k).choose m) : A) 0
Tactic: rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
neg : (↑m ! : A)⁻¹ʳ * x ^ m * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₁ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg₂ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₃ :
  (↑m ! : A)⁻¹ʳ * (x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₄ : (↑m ! : A)⁻¹ʳ * (x ^ m * (↑k ! : A)⁻¹ʳ * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₅ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ m * x ^ k) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₆ :
  (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * (x ^ m * x ^ k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₇ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ (m + k)) = (↑((m + k).choose m) : A) * ((↑(m + k)! : A)⁻¹ʳ * x ^ (m + k))
neg₈ :
  (↑m ! : A)⁻¹ʳ * HMul.hMul (α := A) (↑k ! : A)⁻¹ʳ 0 =
    (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
neg₉ : HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ 0 = (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
neg₁₀ : 0 = (↑((m + k).choose m) : A) * HMul.hMul (α := A) (↑(m + k)! : A)⁻¹ʳ 0
neg₁₁ : 0 = HMul.hMul (α := A) (↑((m + k).choose m) : A) 0
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₁₂ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [dpow_eq_of_mem hx, dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_assoc, ← mul_assoc (x ^ m), mul_comm (x ^ m), mul_assoc _ (x ^ m), ← pow_add, hxmk,
      mul_zero, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (hypothesis)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have hmn : m < n
Tactic: have hmn : m < n := lt_of_le_of_lt (Nat.le_mul_of_pos_right _ (Nat.pos_of_ne_zero hk)) hkm
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have rw : (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
Tactic: rw [dpow_eq_of_mem (m := m * k) hx, dpow_eq_of_mem (dpow_mem hk hx)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
⊢ (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
have pos : ∀ (hm0 : m = 0), (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
Tactic: by_cases hm0 : m = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
pos : ∀ (hm0 : m = 0), (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
⊢ (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
have neg : ∀ (hm0 : ¬m = 0), (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
Tactic: by_cases hm0 : m = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (hypothesis)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
⊢ (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
have hkn : k < n
Tactic: have hkn : k < n := lt_of_le_of_lt (Nat.le_mul_of_pos_left _ (Nat.pos_of_ne_zero hm0)) hkm
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
have neg : (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * x ^ (m * k) =
  HMul.hMul (α := A) (↑(m.uniformBell k) : A) (↑(m * k)! : A)⁻¹ʳ * x ^ (m * k)
Tactic: rw [dpow_eq_of_mem hx, mul_pow, ← pow_mul, mul_comm k, ← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * x ^ (m * k) =
    HMul.hMul (α := A) (↑(m.uniformBell k) : A) (↑(m * k)! : A)⁻¹ʳ * x ^ (m * k)
have apply : (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m = HMul.hMul (α := A) (↑(m.uniformBell k) : A) (↑(m * k)! : A)⁻¹ʳ
Tactic: apply congr_arg₂ _ _ rfl
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m = HMul.hMul (α := A) (↑(m.uniformBell k) : A) (↑(m * k)! : A)⁻¹ʳ
have rw : (↑(m.uniformBell k * k ! ^ m * m !) : A) =
  HPow.hPow (α := A) (↑k ! : A) m * HMul.hMul (α := A) (↑m ! : A) (↑(m.uniformBell k) : A)
Tactic: rw [eq_mul_inverse_iff_mul_eq _ _ _ (hn_fac.natCast_factorial_of_lt hkm),
      mul_assoc, inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hmn),
      inverse_pow_mul_eq_iff_eq_mul _ _ (hn_fac.natCast_factorial_of_lt hkn),
      ← uniformBell_mul_eq _ hk]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
hm0 : ¬m = 0
hkn : k < n
⊢ (↑(m.uniformBell k * k ! ^ m * m !) : A) =
    HPow.hPow (α := A) (↑k ! : A) m * HMul.hMul (α := A) (↑m ! : A) (↑(m.uniformBell k) : A)
have push_cast : (↑(m.uniformBell k) : A) * HPow.hPow (α := A) (↑k ! : A) m * (↑m ! : A) =
  HPow.hPow (α := A) (↑k ! : A) m * HMul.hMul (α := A) (↑m ! : A) (↑(m.uniformBell k) : A)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have pos : ∀ (hmk : m * k < n), dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
Tactic: by_cases! hmk : m * k < n
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
pos : ∀ (hmk : m * k < n), dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have neg : ∀ (hmk : n ≤ m * k), dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
Tactic: by_cases! hmk : m * k < n
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (hypothesis)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have hxmk : x ^ (m * k) = 0
Tactic: have hxmk : x ^ (m * k) = 0 := Ideal.pow_eq_zero_of_mem hnI hmk hx
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have neg : (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * dpow I (m * k) x
Tactic: rw [dpow_eq_of_mem (dpow_mem hk hx), dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_pow, ← pow_mul, ← mul_assoc, mul_comm k, hxmk, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
neg : (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * dpow I (m * k) x
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have neg₁ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ k) ^ m = (↑(m.uniformBell k) : A) * dpow I (m * k) x
Tactic: rw [dpow_eq_of_mem (dpow_mem hk hx), dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_pow, ← pow_mul, ← mul_assoc, mul_comm k, hxmk, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
neg : (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * dpow I (m * k) x
neg₁ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ k) ^ m = (↑(m.uniformBell k) : A) * dpow I (m * k) x
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have neg₂ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ k) ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
Tactic: rw [dpow_eq_of_mem (dpow_mem hk hx), dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_pow, ← pow_mul, ← mul_assoc, mul_comm k, hxmk, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
neg : (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * dpow I (m * k) x
neg₁ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ k) ^ m = (↑(m.uniformBell k) : A) * dpow I (m * k) x
neg₂ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ k) ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have neg₃ : (↑m ! : A)⁻¹ʳ * (HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * (x ^ k) ^ m) =
  (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
Tactic: rw [dpow_eq_of_mem (dpow_mem hk hx), dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_pow, ← pow_mul, ← mul_assoc, mul_comm k, hxmk, mul_zero, mul_zero, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
inst_1 : DecidablePred fun (x : A) ↦ x ∈ I
n : ℕ
hn_fac : IsUnit.{u_1} (M := A) (↑(n - 1)! : A)
hnI : I ^ n = 0
m k : ℕ
hk : k ≠ 0
x : A
hx : x ∈ I
hmk : n ≤ m * k
hxmk : x ^ (m * k) = 0
neg : (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(m.uniformBell k) : A) * dpow I (m * k) x
neg₁ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ k) ^ m = (↑(m.uniformBell k) : A) * dpow I (m * k) x
neg₂ : (↑m ! : A)⁻¹ʳ * ((↑k ! : A)⁻¹ʳ * x ^ k) ^ m = (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
neg₃ :
  (↑m ! : A)⁻¹ʳ * (HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * (x ^ k) ^ m) =
    (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have neg₄ : (↑m ! : A)⁻¹ʳ * (HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * x ^ (k * m)) =
  (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
Tactic: rw [dpow_eq_of_mem (dpow_mem hk hx), dpow_eq_of_mem hx, dpow_eq_of_mem hx,
      mul_pow, ← pow_mul, ← mul_assoc, mul_comm k, hxmk, mul_zero, mul_zero, mul_zero]