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 : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
simp :
  x ^ k.1 * (y ^ k.2 * (↑(m.choose k.1) : A)) =
    x ^ k.1 * (y ^ k.2 * ((↑m ! : A) * HMul.hMul (α := A) (↑k.1! : A)⁻¹ʳ (↑k.2! : A)⁻¹ʳ))
⊢ x ^ k.1 * y ^ k.2 * (↑(m.choose k.1) : A) = x ^ k.1 * y ^ k.2 * (↑m ! : A) * (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ

Tactic:
simp only [mul_assoc]

Premises used: mul_assoc
-- 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 : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
e_a : (↑(m.choose k.1) : A) = (↑m ! : A) * HMul.hMul (α := A) (↑k.1! : A)⁻¹ʳ (↑k.2! : A)⁻¹ʳ
⊢ x ^ k.1 * (y ^ k.2 * (↑(m.choose k.1) : A)) =
    x ^ k.1 * (y ^ k.2 * ((↑m ! : A) * HMul.hMul (α := A) (↑k.1! : A)⁻¹ʳ (↑k.2! : A)⁻¹ʳ))

Tactic:
congr
-- 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 : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
e_a : (↑(m.choose k.1) : A) = HMul.hMul (α := A) (↑m ! : A) (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ
⊢ (↑(m.choose k.1) : A) = (↑m ! : A) * HMul.hMul (α := A) (↑k.1! : A)⁻¹ʳ (↑k.2! : A)⁻¹ʳ

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- 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 : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
⊢ (↑(m.choose k.1) : A) = HMul.hMul (α := A) (↑m ! : A) (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ

Tactic:
castChoose_eq (hn_fac.natCast_factorial_of_lt hmn) hk

Premises used: IsUnit.natCast_factorial_of_lt, Nat.castChoose_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 : ℕ
hmn : m < n
x y : A
hx : x ∈ I
hy : y ∈ I
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
⊢ (↑(m.choose k.1) : A) = HMul.hMul (α := A) (↑m ! : A) (↑k.1! : A)⁻¹ʳ * (↑k.2! : A)⁻¹ʳ

Tactic:
exact castChoose_eq (hn_fac.natCast_factorial_of_lt hmn) hk

Premises used: IsUnit.natCast_factorial_of_lt, Nat.castChoose_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)
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
pos : ∀ (hmn : m < n), dpow I m (x + y) = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y
neg : ∀ (hmn : n ≤ m), dpow I m (x + y) = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y
⊢ dpow I m (x + y) = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y

Tactic:
by_cases! hmn : m < 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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : m < n
⊢ dpow I m (x + y) = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y

Tactic:
dpow_add_of_lt hn_fac hmn hx hy

Premises used: DividedPowers.OfInvertibleFactorial.dpow_add_of_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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : m < n
⊢ dpow I m (x + y) = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y

Tactic:
exact dpow_add_of_lt hn_fac hmn hx hy

Premises used: DividedPowers.OfInvertibleFactorial.dpow_add_of_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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
⊢ I ^ m ≤ I ^ n

Tactic:
have h_sub : I ^ m ≤ I ^ n := Ideal.pow_le_pow_right hmn
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
neg : (↑m ! : A)⁻¹ʳ * (x + y) ^ m = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y
⊢ dpow I m (x + y) = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y

Tactic:
rw [dpow_eq_of_mem (Ideal.add_mem I hx hy)]

Premises used: Ideal.add_mem, DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
neg :
  (↑m ! : A)⁻¹ʳ * (x + y) ^ m =
    ∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m,
      (if x ∈ I then (↑x_1.1! : A)⁻¹ʳ * x ^ x_1.1 else 0) * if y ∈ I then (↑x_1.2! : A)⁻¹ʳ * y ^ x_1.2 else 0
⊢ (↑m ! : A)⁻¹ʳ * (x + y) ^ m = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y

Tactic:
simp only [dpow]

Premises used: DividedPowers.OfInvertibleFactorial.dpow
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
rw : (x + y) ^ m ∈ I ^ n
⊢ (x + y) ^ m = 0

Tactic:
rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]

Premises used: Ideal.mem_bot, Ideal.zero_eq_bot
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m ∈ I ^ n

Tactic:
Set.mem_of_subset_of_mem h_sub (Ideal.pow_mem_pow (Ideal.add_mem I hx hy) m)

Premises used: Set.mem_of_subset_of_mem, Ideal.add_mem, Ideal.pow_mem_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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m ∈ I ^ n

Tactic:
exact Set.mem_of_subset_of_mem h_sub (Ideal.pow_mem_pow (Ideal.add_mem I hx hy) m)

Premises used: Set.mem_of_subset_of_mem, Ideal.add_mem, Ideal.pow_mem_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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m = 0

Tactic:
have hxy : (x + y) ^ m = 0 := by
      rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
      exact Set.mem_of_subset_of_mem h_sub (Ideal.pow_mem_pow (Ideal.add_mem I hx hy) m)
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
neg :
  Eq.{u_1 + 1} (α := A)
    (∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m,
      (if x ∈ I then (↑x_1.1! : A)⁻¹ʳ * x ^ x_1.1 else 0) * if y ∈ I then (↑x_1.2! : A)⁻¹ʳ * y ^ x_1.2 else 0)
    0
⊢ (↑m ! : A)⁻¹ʳ * (x + y) ^ m =
    ∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m,
      (if x ∈ I then (↑x_1.1! : A)⁻¹ʳ * x ^ x_1.1 else 0) * if y ∈ I then (↑x_1.2! : A)⁻¹ʳ * y ^ x_1.2 else 0

Tactic:
rw [hxy, mul_zero, eq_comm]

Premises used: eq_comm, MulZeroClass.mul_zero
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
neg :
  ∀ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m,
    ((if x ∈ I then (↑x_1.1! : A)⁻¹ʳ * x ^ x_1.1 else 0) * if y ∈ I then (↑x_1.2! : A)⁻¹ʳ * y ^ x_1.2 else 0) = 0
⊢ Eq.{u_1 + 1} (α := A)
    (∑ x_1 ∈ @Finset.antidiagonal _ instAddMonoid _ m,
      (if x ∈ I then (↑x_1.1! : A)⁻¹ʳ * x ^ x_1.1 else 0) * if y ∈ I then (↑x_1.2! : A)⁻¹ʳ * y ^ x_1.2 else 0)
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
neg : HMul.hMul (α := A) (↑k.1! : A)⁻¹ʳ (↑k.2! : A)⁻¹ʳ * (y ^ k.2 * x ^ k.1) = 0
⊢ ((if x ∈ I then (↑k.1! : A)⁻¹ʳ * x ^ k.1 else 0) * if y ∈ I then (↑k.2! : A)⁻¹ʳ * y ^ k.2 else 0) = 0

Tactic:
rw [if_pos hx, if_pos hy, mul_assoc, mul_comm (x ^ k.1), mul_assoc, ← mul_assoc]

Premises used: mul_assoc, if_pos, Prod.fst, HPow.hPow, mul_comm
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
neg : y ^ k.2 * x ^ k.1 = 0
⊢ HMul.hMul (α := A) (↑k.1! : A)⁻¹ʳ (↑k.2! : A)⁻¹ʳ * (y ^ k.2 * x ^ k.1) = 0

Tactic:
apply mul_eq_zero_of_right

Premises used: mul_eq_zero_of_right
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
neg : y ^ k.2 * x ^ k.1 ∈ I ^ n
⊢ y ^ k.2 * x ^ k.1 = 0

Tactic:
rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]

Premises used: Ideal.mem_bot, Ideal.zero_eq_bot
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
neg : y ^ k.2 * x ^ k.1 ∈ (↑(I ^ m) : Set A)
⊢ y ^ k.2 * x ^ k.1 ∈ I ^ n

Tactic:
apply Set.mem_of_subset_of_mem h_sub

Premises used: Set.mem_of_subset_of_mem
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
neg : y ^ k.2 * x ^ k.1 ∈ (↑(I ^ k.2 * I ^ k.1) : Set A)
⊢ y ^ k.2 * x ^ k.1 ∈ (↑(I ^ m) : Set A)

Tactic:
rw [← Finset.mem_antidiagonal.mp hk, add_comm, pow_add]

Premises used: pow_add, add_comm, Finset.HasAntidiagonal.mem_antidiagonal, Iff.mp
-- 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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
⊢ y ^ k.2 * x ^ k.1 ∈ (↑(I ^ k.2 * I ^ k.1) : Set A)

Tactic:
Ideal.mul_mem_mul (Ideal.pow_mem_pow hy _) (Ideal.pow_mem_pow hx _)

Premises used: Set.Mem, Ideal.mul_mem_mul, Ideal.pow_mem_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
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 0
k : ℕ × ℕ
hk : k ∈ @Finset.antidiagonal _ instAddMonoid _ m
⊢ y ^ k.2 * x ^ k.1 ∈ (↑(I ^ k.2 * I ^ k.1) : Set A)

Tactic:
exact Ideal.mul_mem_mul (Ideal.pow_mem_pow hy _) (Ideal.pow_mem_pow hx _)

Premises used: Ideal.mul_mem_mul, Ideal.pow_mem_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
m : ℕ
a x : A
hx : x ∈ I
rw : (↑m ! : A)⁻¹ʳ * (a * x) ^ m = a ^ m * dpow I m x
rw₁ : (↑m ! : A)⁻¹ʳ * (a * x) ^ m = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
rw₂ : (↑m ! : A)⁻¹ʳ * (a ^ m * x ^ m) = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
rw₃ : (↑m ! : A)⁻¹ʳ * a ^ m * x ^ m = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
rw₄ : a ^ m * (↑m ! : A)⁻¹ʳ * x ^ m = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
rw₅ rw₆ : a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m) = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
⊢ dpow I m (a * x) = a ^ m * dpow I m x

Tactic:
rw [dpow_eq_of_mem (Ideal.mul_mem_left I _ hx), dpow_eq_of_mem hx,
    mul_pow, ← mul_assoc, mul_comm _ (a ^ m), mul_assoc]

Premises used: mul_assoc, HPow.hPow, DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem, mul_comm, Ideal.mul_mem_left, 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
⊢ m < n

Tactic:
have hm : m < n := lt_of_le_of_lt le_self_add 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
⊢ k < n

Tactic:
have hk : k < n := lt_of_le_of_lt le_add_self 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
rw :
  HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ (↑k ! : A)⁻¹ʳ * x ^ (m + k) =
    HMul.hMul (α := A) (↑((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

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, ← mul_assoc, ← mul_assoc]

Premises used: mul_assoc, pow_add, HPow.hPow, DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem, mul_comm
-- 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
apply : HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ (↑k ! : A)⁻¹ʳ = HMul.hMul (α := A) (↑((m + k).choose m) : A) (↑(m + k)! : A)⁻¹ʳ
⊢ HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ (↑k ! : A)⁻¹ʳ * x ^ (m + k) =
    HMul.hMul (α := A) (↑((m + k).choose m) : 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
rw : (↑(m + k)! : A) = (↑k ! : A) * HMul.hMul (α := A) (↑m ! : A) (↑((m + k).choose m) : A)
⊢ HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ (↑k ! : A)⁻¹ʳ = HMul.hMul (α := A) (↑((m + k).choose m) : 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 hm),
      inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hk)]

Premises used: Ring.inverse_mul_eq_iff_eq_mul, mul_assoc, IsUnit.natCast_factorial_of_lt, 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
norm_cast : Eq.{u_1 + 1} (α := A) (↑(m + k)! : A) (↑(k ! * (m ! * (m + k).choose m)) : A)
⊢ (↑(m + k)! : A) = (↑k ! : A) * HMul.hMul (α := A) (↑m ! : A) (↑((m + k).choose m) : A)

Tactic:
norm_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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
h : (m + k)! = k ! * (m ! * (m + k).choose m)
⊢ Eq.{u_1 + 1} (α := A) (↑(m + k)! : A) (↑(k ! * (m ! * (m + k).choose m)) : A)

Tactic:
apply congr_arg

Premises used: 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
h : (m + k).choose k * m ! * k ! = k ! * (m ! * (m + k).choose m)
h₁ : k ! * ((m + k).choose k * m !) = k ! * (m ! * (m + k).choose m)
h₂ : k ! * (m ! * (m + k).choose k) = k ! * (m ! * (m + k).choose m)
h₃ h₄ : k ! * (m ! * (m + k).choose k) = k ! * (m ! * (m + k).choose k)
⊢ (m + k)! = k ! * (m ! * (m + k).choose m)

Tactic:
rw [← Nat.add_choose_mul_factorial_mul_factorial, mul_comm, mul_comm _ (m !), Nat.choose_symm_add]

Premises used: Nat.choose_symm_add, Nat.factorial, mul_comm, Nat.add_choose_mul_factorial_mul_factorial
-- 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 : ℕ
x : A
hx : x ∈ I
pos : ∀ (hkm : m + k < n), dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
neg : ∀ (hkm : n ≤ m + k), dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x

Tactic:
by_cases! hkm : 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 : ℕ
x : A
hx : x ∈ I
hkm : m + k < n
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x

Tactic:
dpow_mul_of_add_lt hn_fac hkm hx

Premises used: DividedPowers.OfInvertibleFactorial.dpow_mul_of_add_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 : ℕ
x : A
hx : x ∈ I
hkm : m + k < n
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x

Tactic:
exact dpow_mul_of_add_lt hn_fac hkm hx

Premises used: DividedPowers.OfInvertibleFactorial.dpow_mul_of_add_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 : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
⊢ x ^ (m + k) = 0

Tactic:
have hxmk : x ^ (m + k) = 0 := Ideal.pow_eq_zero_of_mem hnI hkm 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 : ℕ
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
neg₁₂ neg₁₃ : Eq.{u_1 + 1} (α := A) 0 0
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x

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]

Premises used: mul_assoc, pow_add, MulZeroClass.mul_zero, HPow.hPow, DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem, mul_comm
-- 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
⊢ 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
-- 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
rw : (↑m ! : A)⁻¹ʳ * dpow I k x ^ 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

Tactic:
rw [dpow_eq_of_mem (m := m * k) hx, dpow_eq_of_mem (dpow_mem hk hx)]

Premises used: DividedPowers.OfInvertibleFactorial.dpow_mem, DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem