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 : ℕ
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))
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]
-- 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))
neg₄ :
  (↑m ! : A)⁻¹ʳ * (HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * 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 ^ (m * k) =
  (↑(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))
neg₄ :
  (↑m ! : A)⁻¹ʳ * (HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * 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))
neg₆ :
  (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * x ^ (m * k) =
    (↑(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 * 0 =
  (↑(m.uniformBell k) : A) * HMul.hMul (α := A) (↑(m * k)! : A)⁻¹ʳ 0
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))
neg₄ :
  (↑m ! : A)⁻¹ʳ * (HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * 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))
neg₆ :
  (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * x ^ (m * k) =
    (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
neg₇ :
  (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * 0 =
    (↑(m.uniformBell k) : A) * HMul.hMul (α := A) (↑(m * k)! : A)⁻¹ʳ 0
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have neg₈ : 0 = (↑(m.uniformBell k) : A) * HMul.hMul (α := A) (↑(m * k)! : A)⁻¹ʳ 0
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))
neg₄ :
  (↑m ! : A)⁻¹ʳ * (HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * 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))
neg₆ :
  (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * x ^ (m * k) =
    (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
neg₇ :
  (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * 0 =
    (↑(m.uniformBell k) : A) * HMul.hMul (α := A) (↑(m * k)! : A)⁻¹ʳ 0
neg₈ : 0 = (↑(m.uniformBell k) : A) * HMul.hMul (α := A) (↑(m * k)! : A)⁻¹ʳ 0
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have neg₉ : 0 = HMul.hMul (α := A) (↑(m.uniformBell k) : A) 0
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))
neg₄ :
  (↑m ! : A)⁻¹ʳ * (HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * 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))
neg₆ :
  (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * x ^ (m * k) =
    (↑(m.uniformBell k) : A) * ((↑(m * k)! : A)⁻¹ʳ * x ^ (m * k))
neg₇ :
  (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m * 0 =
    (↑(m.uniformBell k) : A) * HMul.hMul (α := A) (↑(m * k)! : A)⁻¹ʳ 0
neg₈ : 0 = (↑(m.uniformBell k) : A) * HMul.hMul (α := A) (↑(m * k)! : A)⁻¹ʳ 0
neg₉ : 0 = HMul.hMul (α := A) (↑(m.uniformBell k) : A) 0
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x
have neg₁₀ : Eq.{u_1 + 1} (α := A) 0 0
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
hI2 : HPow.hPow (β := ℕ) I 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
⊢ (dividedPowers hI2).dpow n a = 0
have simp : a ∈ I → (↑n ! : A)⁻¹ʳ * a ^ n = 0
Tactic: simp only [dividedPowers, OfInvertibleFactorial.dpow_apply, ite_eq_right_iff]
-- 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
hI2 : HPow.hPow (β := ℕ) I 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
⊢ (↑n ! : A)⁻¹ʳ * a ^ n = 0
have rw : HMul.hMul (α := A) (↑n ! : A)⁻¹ʳ 0 = 0
Tactic: rw [Ideal.pow_eq_zero_of_mem hI2 hn ha, 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
hI2 : HPow.hPow (β := ℕ) I 2 = 0
n : ℕ
hn : 2 ≤ n
a : A
ha : a ∈ I
rw : HMul.hMul (α := A) (↑n ! : A)⁻¹ʳ 0 = 0
⊢ (↑n ! : A)⁻¹ʳ * a ^ n = 0
have rw₁ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [Ideal.pow_eq_zero_of_mem hI2 hn ha, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommRing A
p : ℕ
inst_1 : Fact (Nat.Prime p)
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
I : Ideal A
inst_2 : DecidablePred fun (x : A) ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
⊢ (dividedPowers hp hIp).dpow n a = 0
have simp : a ∈ I → (↑n ! : A)⁻¹ʳ * a ^ n = 0
Tactic: simp only [dividedPowers, OfInvertibleFactorial.dpow_apply, ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommRing A
p : ℕ
inst_1 : Fact (Nat.Prime p)
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
I : Ideal A
inst_2 : DecidablePred fun (x : A) ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
ha : a ∈ I
⊢ (↑n ! : A)⁻¹ʳ * a ^ n = 0
have rw : HMul.hMul (α := A) (↑n ! : A)⁻¹ʳ 0 = 0
Tactic: rw [Ideal.pow_eq_zero_of_mem hIp hn ha, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommRing A
p : ℕ
inst_1 : Fact (Nat.Prime p)
hp : IsNilpotent.{u_1} (R := A) (↑p : A)
I : Ideal A
inst_2 : DecidablePred fun (x : A) ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
ha : a ∈ I
rw : HMul.hMul (α := A) (↑n ! : A)⁻¹ʳ 0 = 0
⊢ (↑n ! : A)⁻¹ʳ * a ^ n = 0
have rw₁ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [Ideal.pow_eq_zero_of_mem hIp hn ha, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommRing A
p : ℕ
inst_1 : CharP A p
inst_2 : Fact (Nat.Prime p)
I : Ideal A
inst_3 : DecidablePred fun (x : A) ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
⊢ (dividedPowers A p hIp).dpow n a = 0
have simp : a ∈ I → (↑n ! : A)⁻¹ʳ * a ^ n = 0
Tactic: simp only [dividedPowers, IsNilpotent.dividedPowers, OfInvertibleFactorial.dpow_apply,
    ite_eq_right_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommRing A
p : ℕ
inst_1 : CharP A p
inst_2 : Fact (Nat.Prime p)
I : Ideal A
inst_3 : DecidablePred fun (x : A) ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
ha : a ∈ I
⊢ (↑n ! : A)⁻¹ʳ * a ^ n = 0
have rw : HMul.hMul (α := A) (↑n ! : A)⁻¹ʳ 0 = 0
Tactic: rw [Ideal.pow_eq_zero_of_mem hIp hn ha, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
A : Type u_1
inst : CommRing A
p : ℕ
inst_1 : CharP A p
inst_2 : Fact (Nat.Prime p)
I : Ideal A
inst_3 : DecidablePred fun (x : A) ↦ x ∈ I
hIp : I ^ p = 0
n : ℕ
hn : p ≤ n
a : A
ha : a ∈ I
rw : HMul.hMul (α := A) (↑n ! : A)⁻¹ʳ 0 = 0
⊢ (↑n ! : A)⁻¹ʳ * a ^ n = 0
have rw₁ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [Ideal.pow_eq_zero_of_mem hIp hn ha, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : DecidablePred fun (x : R) ↦ x ∈ I
n : ℕ
x : R
hx : x ∈ I
⊢ dpow I n x = (↑n ! : R)⁻¹ʳ * x ^ n
have rw : OfInvertibleFactorial.dpow I n x = (↑n ! : R)⁻¹ʳ * x ^ n
Tactic: rw [dpow, OfInvertibleFactorial.dpow_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : DecidablePred fun (x : R) ↦ x ∈ I
n : ℕ
x : R
hx : x ∈ I
rw : OfInvertibleFactorial.dpow I n x = (↑n ! : R)⁻¹ʳ * x ^ n
⊢ dpow I n x = (↑n ! : R)⁻¹ʳ * x ^ n
have rw₁ : (↑n ! : R)⁻¹ʳ * x ^ n = (↑n ! : R)⁻¹ʳ * x ^ n
Tactic: rw [dpow, OfInvertibleFactorial.dpow_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ʳ (x ^ n)
have rw : hI.dpow n x = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R) • hI.dpow n x
Tactic: rw [inverse_eq_inv', ← factorial_mul_dpow_eq_pow hI hx, ← smul_eq_mul, ← smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R) • hI.dpow n x
have nth_rewrite : HSMul.hSMul (α := R) 1 (hI.dpow n x) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R) • hI.dpow n x
Tactic: nth_rewrite 1 [← one_smul R (hI.dpow n x)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ HSMul.hSMul (α := R) 1 (hI.dpow n x) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R) • hI.dpow n x
have e_a : 1 = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1
have rw : (↑n ! : R) = HSMul.hSMul (β := R) n ! 1
Tactic: rw [cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
rw : (↑n ! : R) = HSMul.hSMul (β := R) n ! 1
⊢ (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1
have rw₁ : (↑n ! : R) = HMul.hMul (α := R) (↑n ! : R) 1
Tactic: rw [cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
rw : (↑n ! : R) = HSMul.hSMul (β := R) n ! 1
rw₁ : (↑n ! : R) = HMul.hMul (α := R) (↑n ! : R) 1
⊢ (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1
have rw₂ : Eq.{u_1 + 1} (α := R) (↑n ! : R) (↑n ! : R)
Tactic: rw [cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ 1 = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R)
have aux : (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1
Tactic: have aux : ((n !) : R) = (n ! : ℚ) • (1 : R) := by
    rw [cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1
⊢ 1 = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R)
have e_a : 1 = HSMul.hSMul (β := R) (HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ)) 1
Tactic: rw [aux, ← mul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1
this : HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ) = 1
⊢ 1 = HSMul.hSMul (β := R) (HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ)) 1
have rw : 1 = HSMul.hSMul (α := ℚ) (β := R) 1 1
Tactic: rw [this, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1
this : HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ) = 1
rw : 1 = HSMul.hSMul (α := ℚ) (β := R) 1 1
⊢ 1 = HSMul.hSMul (β := R) (HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ)) 1
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [this, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1
⊢ 1 = HSMul.hSMul (β := R) (HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ)) 1
have e_a : HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ) = 1
Tactic: suffices (n ! : ℚ)⁻¹ * (n !) = 1 by
    rw [this, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
aux : (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1
⊢ HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ) = 1
have e_a : Ne (α := ℚ) (↑n ! : ℚ) 0
Tactic: apply Rat.inv_mul_cancel
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : DecidablePred fun (x : R) ↦ x ∈ I
inst_2 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (dividedPowers I).dpow n x
have rw : hI.dpow n x = if x ∈ I then (↑n ! : R)⁻¹ʳ * x ^ n else 0
Tactic: rw [dpow_apply, if_pos hx, eq_comm, inverse_mul_eq_iff_eq_mul _ _ _
      (IsUnit.natCast_factorial_of_algebra ℚ n), factorial_mul_dpow_eq_pow _ hx]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : DecidablePred fun (x : R) ↦ x ∈ I
inst_2 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
rw : hI.dpow n x = if x ∈ I then (↑n ! : R)⁻¹ʳ * x ^ n else 0
⊢ hI.dpow n x = (dividedPowers I).dpow n x
have rw₁ : hI.dpow n x = (↑n ! : R)⁻¹ʳ * x ^ n
Tactic: rw [dpow_apply, if_pos hx, eq_comm, inverse_mul_eq_iff_eq_mul _ _ _
      (IsUnit.natCast_factorial_of_algebra ℚ n), factorial_mul_dpow_eq_pow _ hx]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : DecidablePred fun (x : R) ↦ x ∈ I
inst_2 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
rw : hI.dpow n x = if x ∈ I then (↑n ! : R)⁻¹ʳ * x ^ n else 0
rw₁ : hI.dpow n x = (↑n ! : R)⁻¹ʳ * x ^ n
⊢ hI.dpow n x = (dividedPowers I).dpow n x
have rw₂ : (↑n ! : R)⁻¹ʳ * x ^ n = hI.dpow n x
Tactic: rw [dpow_apply, if_pos hx, eq_comm, inverse_mul_eq_iff_eq_mul _ _ _
      (IsUnit.natCast_factorial_of_algebra ℚ n), factorial_mul_dpow_eq_pow _ hx]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : DecidablePred fun (x : R) ↦ x ∈ I
inst_2 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
rw : hI.dpow n x = if x ∈ I then (↑n ! : R)⁻¹ʳ * x ^ n else 0
rw₁ : hI.dpow n x = (↑n ! : R)⁻¹ʳ * x ^ n
rw₂ : (↑n ! : R)⁻¹ʳ * x ^ n = hI.dpow n x
⊢ hI.dpow n x = (dividedPowers I).dpow n x
have rw₃ : x ^ n = (↑n ! : R) * hI.dpow n x
Tactic: rw [dpow_apply, if_pos hx, eq_comm, inverse_mul_eq_iff_eq_mul _ _ _
      (IsUnit.natCast_factorial_of_algebra ℚ n), factorial_mul_dpow_eq_pow _ hx]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.RatAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : DecidablePred fun (x : R) ↦ x ∈ I
inst_2 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
rw : hI.dpow n x = if x ∈ I then (↑n ! : R)⁻¹ʳ * x ^ n else 0
rw₁ : hI.dpow n x = (↑n ! : R)⁻¹ʳ * x ^ n
rw₂ : (↑n ! : R)⁻¹ʳ * x ^ n = hI.dpow n x
rw₃ : x ^ n = (↑n ! : R) * hI.dpow n x
⊢ hI.dpow n x = (dividedPowers I).dpow n x
have rw₄ : x ^ n = x ^ n
Tactic: rw [dpow_apply, if_pos hx, eq_comm, inverse_mul_eq_iff_eq_mul _ _ _
      (IsUnit.natCast_factorial_of_algebra ℚ n), factorial_mul_dpow_eq_pow _ hx]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
⊢ IsNilpotent x ↔ IsNilpotent x.fst
have mp : IsNilpotent x → IsNilpotent x.fst
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
mp : IsNilpotent x → IsNilpotent x.fst
⊢ IsNilpotent x ↔ IsNilpotent x.fst
have mpr : IsNilpotent x.fst → IsNilpotent x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x ^ n = 0
⊢ IsNilpotent x.fst
have mp : x.fst ^ n = 0
Tactic: refine ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x ^ n = 0
⊢ x.fst ^ n = 0
have mp : (x ^ n).fst = 0
Tactic: rw [← fst_pow, hn, fst_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x ^ n = 0
mp : (x ^ n).fst = 0
⊢ x.fst ^ n = 0
have mp₁ : Eq.{u_1 + 1} (α := R) (fst.{u_1, u_2} (M := M) 0) 0
Tactic: rw [← fst_pow, hn, fst_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DualNumber (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.{u_1, u_2} Rᵐᵒᵖ M
inst_4 : SMulCommClass R Rᵐᵒᵖ M
x : TrivSqZeroExt R M
n : ℕ
hn : x ^ n = 0
mp : (x ^ n).fst = 0
mp₁ : Eq.{u_1 + 1} (α := R) (fst.{u_1, u_2} (M := M) 0) 0
⊢ x.fst ^ n = 0
have mp₂ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [← fst_pow, hn, fst_zero]