awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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))
neg : ∀ (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))

Tactic:
by_cases hm0 : m = 0
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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))

Tactic:
simp only [hm0, zero_mul, _root_.pow_zero, mul_one, uniformBell_zero_left, cast_one, one_mul]

Premises used: MulZeroClass.zero_mul, pow_zero, mul_one, Nat.uniformBell_zero_left, Nat.cast_one, one_mul
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
⊢ 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
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
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)
⊢ (↑m ! : A)⁻¹ʳ * dpow I k x ^ m = (↑(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]

Premises used: mul_assoc, pow_mul, DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem, mul_comm, mul_pow
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
apply :
  (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m = HMul.hMul (α := A) (↑(m.uniformBell k) : A) (↑(m * k)! : A)⁻¹ʳ
⊢ (↑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:
apply congr_arg₂ _ _ rfl

Premises used: rfl, congr_arg₂
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
rw :
  (↑(m.uniformBell k * k ! ^ m * m !) : A) =
    HPow.hPow (α := A) (↑k ! : A) m * HMul.hMul (α := A) (↑m ! : A) (↑(m.uniformBell k) : A)
⊢ (↑m ! : A)⁻¹ʳ * HPow.hPow (α := A) (↑k ! : A)⁻¹ʳ m = HMul.hMul (α := A) (↑(m.uniformBell k) : A) (↑(m * 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]

Premises used: Ring.inverse_mul_eq_iff_eq_mul, Nat.uniformBell_mul_eq, mul_assoc, IsUnit.natCast_factorial_of_lt, Ring.inverse_pow_mul_eq_iff_eq_mul, Ring.eq_mul_inverse_iff_mul_eq
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
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)
⊢ (↑(m.uniformBell k * k ! ^ m * m !) : A) =
    HPow.hPow (α := A) (↑k ! : A) m * HMul.hMul (α := A) (↑m ! : A) (↑(m.uniformBell k) : A)

Tactic:
push_cast
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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) : 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:
ring_nf
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
neg : ∀ (hmk : n ≤ m * k), 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

Tactic:
by_cases! hmk : m * k < n
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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 : m * k < n
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x

Tactic:
dpow_comp_of_mul_lt hn_fac hk hmk hx

Premises used: DividedPowers.OfInvertibleFactorial.dpow_comp_of_mul_lt
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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 : m * k < n
⊢ dpow I m (dpow I k x) = (↑(m.uniformBell k) : A) * dpow I (m * k) x

Tactic:
exact dpow_comp_of_mul_lt hn_fac hk hmk hx

Premises used: DividedPowers.OfInvertibleFactorial.dpow_comp_of_mul_lt
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
⊢ x ^ (m * k) = 0

Tactic:
have hxmk : x ^ (m * k) = 0 := Ideal.pow_eq_zero_of_mem hnI hmk hx
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
neg₁₀ neg₁₁ : Eq.{u_1 + 1} (α := A) 0 0
⊢ dpow I m (dpow I k x) = (↑(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]

Premises used: DividedPowers.OfInvertibleFactorial.dpow_mem, mul_assoc, pow_mul, MulZeroClass.mul_zero, DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem, mul_comm, mul_pow
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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 : ℕ
x : A
⊢ (dividedPowers hn_fac hnI).dpow m x = if x ∈ I then (↑m ! : A)⁻¹ʳ * x ^ m else 0

Tactic:
rfl

Premises used: DividedPowers.OfInvertibleFactorial.dpow, rfl, ite
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
⊢ IsUnit.{u_1} (M := A) (↑(HSub.hSub (α := ℕ) 2 1)! : A)

Tactic:
norm_num
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
simp : a ∈ I → (↑n ! : A)⁻¹ʳ * a ^ n = 0
⊢ (dividedPowers hI2).dpow n a = 0

Tactic:
simp only [dividedPowers, OfInvertibleFactorial.dpow_apply, ite_eq_right_iff]

Premises used: DividedPowers.OfSquareZero.dividedPowers, DividedPowers.OfInvertibleFactorial.dpow_apply, ite_eq_right_iff
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := A) 0 0
⊢ (↑n ! : A)⁻¹ʳ * a ^ n = 0

Tactic:
rw [Ideal.pow_eq_zero_of_mem hI2 hn ha, mul_zero]

Premises used: Ideal.pow_eq_zero_of_mem, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
simp : a ∈ I → (↑n ! : A)⁻¹ʳ * a ^ n = 0
⊢ (dividedPowers hp hIp).dpow n a = 0

Tactic:
simp only [dividedPowers, OfInvertibleFactorial.dpow_apply, ite_eq_right_iff]

Premises used: DividedPowers.OfInvertibleFactorial.dpow_apply, DividedPowers.IsNilpotent.dividedPowers, ite_eq_right_iff
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := A) 0 0
⊢ (↑n ! : A)⁻¹ʳ * a ^ n = 0

Tactic:
rw [Ideal.pow_eq_zero_of_mem hIp hn ha, mul_zero]

Premises used: Ideal.pow_eq_zero_of_mem, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
simp : a ∈ I → (↑n ! : A)⁻¹ʳ * a ^ n = 0
⊢ (dividedPowers A p hIp).dpow n a = 0

Tactic:
simp only [dividedPowers, IsNilpotent.dividedPowers, OfInvertibleFactorial.dpow_apply,
    ite_eq_right_iff]

Premises used: DividedPowers.OfInvertibleFactorial.dpow_apply, DividedPowers.IsNilpotent.dividedPowers, DividedPowers.CharP.dividedPowers, ite_eq_right_iff
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := A) 0 0
⊢ (↑n ! : A)⁻¹ʳ * a ^ n = 0

Tactic:
rw [Ideal.pow_eq_zero_of_mem hIp hn ha, mul_zero]

Premises used: Ideal.pow_eq_zero_of_mem, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
rw₁ rw₂ : (↑n ! : R)⁻¹ʳ * x ^ n = (↑n ! : R)⁻¹ʳ * x ^ n
⊢ dpow I n x = (↑n ! : R)⁻¹ʳ * x ^ n

Tactic:
rw [dpow, OfInvertibleFactorial.dpow_eq_of_mem hx]

Premises used: DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem, DividedPowers.RatAlgebra.dpow
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : DecidablePred fun (x : R) ↦ x ∈ I
inst_2 : Algebra ℚ R
n : ℕ
x : R
⊢ (dividedPowers I).dpow n x = if x ∈ I then (↑n ! : R)⁻¹ʳ * x ^ n else 0

Tactic:
rfl

Premises used: DividedPowers.OfInvertibleFactorial.dpow, DividedPowers.RatAlgebra.dpow, rfl, ite
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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 : hI.dpow n x = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R) • hI.dpow n x
⊢ hI.dpow n x = HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ʳ (x ^ n)

Tactic:
rw [inverse_eq_inv', ← factorial_mul_dpow_eq_pow hI hx, ← smul_eq_mul, ← smul_assoc]

Premises used: DividedPowers.factorial_mul_dpow_eq_pow, Ring.inverse_eq_inv', smul_assoc, smul_eq_mul
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
nth_rewrite : HSMul.hSMul (α := R) 1 (hI.dpow n x) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R) • hI.dpow n x
⊢ 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)]

Premises used: one_smul, DividedPowers.dpow
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
inst_1 : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
e_a : 1 = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R)
⊢ HSMul.hSMul (α := R) 1 (hI.dpow n x) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R) • hI.dpow n x

Tactic:
congr
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) (↑n ! : R) (↑n ! : R)
⊢ (↑n ! : R) = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ) 1

Tactic:
rw [cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]

Premises used: Nat.cast_smul_eq_nsmul, nsmul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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

Tactic:
have aux : ((n !) : R) = (n ! : ℚ) • (1 : R) := by
    rw [cast_smul_eq_nsmul, nsmul_eq_mul, mul_one]
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
e_a : 1 = HSMul.hSMul (β := R) (HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ)) 1
⊢ 1 = HSMul.hSMul (α := ℚ) (β := R) (↑n ! : ℚ)⁻¹ (↑n ! : R)

Tactic:
rw [aux, ← mul_smul]

Premises used: SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ 1 = HSMul.hSMul (β := R) (HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ)) 1

Tactic:
rw [this, one_smul]

Premises used: one_smul
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
e_a : HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ) = 1
⊢ 1 = HSMul.hSMul (β := R) (HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ)) 1

Tactic:
suffices (n ! : ℚ)⁻¹ * (n !) = 1 by
    rw [this, one_smul]
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
e_a : Ne (α := ℚ) (↑n ! : ℚ) 0
⊢ HMul.hMul (α := ℚ) (↑n ! : ℚ)⁻¹ (↑n ! : ℚ) = 1

Tactic:
apply Rat.inv_mul_cancel

Premises used: Rat.inv_mul_cancel
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
⊢ ¬Eq (α := ℚ) (↑n ! : ℚ) (↑0 : ℚ)

Tactic:
simp [factorial_ne_zero]

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.RingTheory.DividedPowers.RatAlgebra
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
rw₄ rw₅ : x ^ n = x ^ n
⊢ hI.dpow n x = (dividedPowers I).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]

Premises used: DividedPowers.factorial_mul_dpow_eq_pow, Ring.inverse_mul_eq_iff_eq_mul, DividedPowers.RatAlgebra.dpow_apply, if_pos, eq_comm
-- Module: Mathlib.RingTheory.DualNumber
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
mpr : IsNilpotent x.fst → IsNilpotent x
⊢ IsNilpotent x ↔ IsNilpotent x.fst

Tactic:
constructor
-- Module: Mathlib.RingTheory.DualNumber
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

Tactic:
⟨n, ?_⟩

Premises used: Exists.intro, IsNilpotent
-- Module: Mathlib.RingTheory.DualNumber
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.fst ^ n = 0
⊢ IsNilpotent x.fst

Tactic:
refine ⟨n, ?_⟩
-- Module: Mathlib.RingTheory.DualNumber
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
mp₂ mp₃ : Eq.{u_1 + 1} (α := R) 0 0
⊢ x.fst ^ n = 0

Tactic:
rw [← fst_pow, hn, fst_zero]

Premises used: TrivSqZeroExt.fst_pow, TrivSqZeroExt.fst_zero
-- Module: Mathlib.RingTheory.DualNumber
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.fst ^ n = 0
⊢ IsNilpotent x

Tactic:
⟨n * 2, ?_⟩

Premises used: HMul.hMul, Exists.intro, OfNat.ofNat, IsNilpotent
-- Module: Mathlib.RingTheory.DualNumber
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.fst ^ n = 0
mpr : x ^ (n * 2) = 0
⊢ IsNilpotent x

Tactic:
refine ⟨n * 2, ?_⟩
-- Module: Mathlib.RingTheory.DualNumber
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.fst ^ n = 0
mpr : HPow.hPow (β := ℕ) (x ^ n) 2 = 0
⊢ x ^ (n * 2) = 0

Tactic:
rw [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.RingTheory.DualNumber
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.fst ^ n = 0
mpr : (HPow.hPow (β := ℕ) (x ^ n) 2).fst = fst.{u_1, u_2} (M := M) 0
mpr₁ : (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0
⊢ HPow.hPow (β := ℕ) (x ^ n) 2 = 0

Tactic:
ext
-- Module: Mathlib.RingTheory.DualNumber
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.fst ^ n = 0
mpr : HPow.hPow (β := ℕ) (x ^ n).fst 2 = fst.{u_1, u_2} (M := M) 0
mpr₁ : HPow.hPow (β := ℕ) (x.fst ^ n) 2 = fst.{u_1, u_2} (M := M) 0
mpr₂ : HPow.hPow (α := R) (β := ℕ) 0 2 = fst.{u_1, u_2} (M := M) 0
mpr₃ : Eq.{u_1 + 1} (α := R) 0 (fst.{u_1, u_2} (M := M) 0)
mpr₄ mpr₅ : Eq.{u_1 + 1} (α := R) 0 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).fst = fst.{u_1, u_2} (M := M) 0

Tactic:
rw [fst_pow, fst_pow, hn, zero_pow two_ne_zero, fst_zero]

Premises used: two_ne_zero, TrivSqZeroExt.fst_pow, zero_pow, TrivSqZeroExt.fst_zero
-- Module: Mathlib.RingTheory.DualNumber
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.fst ^ n = 0
mpr : (x ^ n * x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₁ : (x ^ n).fst • (x ^ n).snd + MulOpposite.op (x ^ n).fst • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₂ : x.fst ^ n • (x ^ n).snd + MulOpposite.op (x.fst ^ n) • (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₃ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd +
      HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) (MulOpposite.op 0) (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
mpr₄ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (x ^ n).snd + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd =
    snd.{u_1, u_2} (R := R) 0
mpr₅ : 0 + HSMul.hSMul.{u_1, u_2, u_2} (α := Rᵐᵒᵖ) 0 (x ^ n).snd = snd.{u_1, u_2} (R := R) 0
mpr₆ : HAdd.hAdd (α := M) 0 0 = snd.{u_1, u_2} (R := R) 0
mpr₇ : Eq.{u_2 + 1} (α := M) 0 (snd.{u_1, u_2} (R := R) 0)
mpr₈ mpr₉ : Eq.{u_2 + 1} (α := M) 0 0
⊢ (HPow.hPow (β := ℕ) (x ^ n) 2).snd = snd.{u_1, u_2} (R := R) 0

Tactic:
rw [pow_two, snd_mul, fst_pow, hn, MulOpposite.op_zero, zero_smul, zero_smul, zero_add,
        snd_zero]

Premises used: pow_two, MulOpposite.op_zero, zero_add, zero_smul, TrivSqZeroExt.snd_mul, TrivSqZeroExt.fst_pow, TrivSqZeroExt.snd_zero
-- Module: Mathlib.RingTheory.DualNumber
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
r : R
rw : IsNilpotent (fst.{u_1, u_2} (M := M) (inl r)) ↔ IsNilpotent r
rw₁ rw₂ : IsNilpotent r ↔ IsNilpotent r
⊢ IsNilpotent (R := TrivSqZeroExt R M) (inl r) ↔ IsNilpotent r

Tactic:
rw [isNilpotent_iff_isNilpotent_fst, fst_inl]

Premises used: TrivSqZeroExt.isNilpotent_iff_isNilpotent_fst, TrivSqZeroExt.fst_inl
-- Module: Mathlib.RingTheory.DualNumber
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 : M
⊢ HPow.hPow (α := TrivSqZeroExt R M) (β := ℕ) (inr x) 2 = 0

Tactic:
simp [pow_two]

Premises used: pow_two