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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ dpow I m (x + y) = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y
have neg : (↑m ! : A)⁻¹ʳ * (x + y) ^ m = ∑ 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)]
-- 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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ (↑m ! : A)⁻¹ʳ * (x + y) ^ m = ∑ k ∈ @Finset.antidiagonal _ instAddMonoid _ m, dpow I k.1 x * dpow I k.2 y
have 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
Tactic: simp only [dpow]
-- 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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ (x + y) ^ m = 0
have rw : (x + y) ^ m ∈ I ^ n
Tactic: rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
-- 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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
⊢ (↑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
have hxy : (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)
-- 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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 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
have 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
Tactic: rw [hxy, mul_zero, eq_comm]
-- 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 : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
h_sub : I ^ m ≤ I ^ n
hxy : (x + y) ^ m = 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
have 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
Tactic: apply Finset.sum_eq_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 : ℕ
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
⊢ ((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
have neg : HMul.hMul (α := A) (↑k.1! : A)⁻¹ʳ (↑k.2! : A)⁻¹ʳ * (y ^ k.2 * x ^ k.1) = 0
Tactic: rw [if_pos hx, if_pos hy, mul_assoc, mul_comm (x ^ k.1), 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)
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
⊢ HMul.hMul (α := A) (↑k.1! : A)⁻¹ʳ (↑k.2! : A)⁻¹ʳ * (y ^ k.2 * x ^ k.1) = 0
have neg : y ^ k.2 * x ^ k.1 = 0
Tactic: apply mul_eq_zero_of_right
-- 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 : ℕ
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 = 0
have neg : y ^ k.2 * x ^ k.1 ∈ I ^ n
Tactic: rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
-- 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 : ℕ
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 ^ n
have neg : y ^ k.2 * x ^ k.1 ∈ (↑(I ^ m) : Set A)
Tactic: apply Set.mem_of_subset_of_mem h_sub
-- 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 : ℕ
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 ^ m) : Set A)
have neg : y ^ k.2 * x ^ k.1 ∈ (↑(I ^ k.2 * I ^ k.1) : Set A)
Tactic: rw [← Finset.mem_antidiagonal.mp hk, add_comm, pow_add]
-- 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
m : ℕ
a x : A
hx : x ∈ I
⊢ dpow I m (a * x) = a ^ m * dpow I m x
have rw : (↑m ! : A)⁻¹ʳ * (a * x) ^ m = 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]
-- 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
m : ℕ
a x : A
hx : x ∈ I
rw : (↑m ! : A)⁻¹ʳ * (a * x) ^ m = a ^ m * dpow I m x
⊢ dpow I m (a * x) = a ^ m * dpow I m x
have rw₁ : (↑m ! : A)⁻¹ʳ * (a * x) ^ m = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
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]
-- 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
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)
⊢ dpow I m (a * x) = a ^ m * dpow I m x
have rw₂ : (↑m ! : A)⁻¹ʳ * (a ^ m * x ^ m) = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
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]
-- 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
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)
⊢ dpow I m (a * x) = a ^ m * dpow I m x
have rw₃ : (↑m ! : A)⁻¹ʳ * a ^ m * x ^ m = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
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]
-- 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
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)
⊢ dpow I m (a * x) = a ^ m * dpow I m x
have rw₄ : a ^ m * (↑m ! : A)⁻¹ʳ * x ^ m = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
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]
-- 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
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)
⊢ dpow I m (a * x) = a ^ m * dpow I m x
have rw₅ : a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m) = a ^ m * ((↑m ! : A)⁻¹ʳ * x ^ m)
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]
-- 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have hm : m < n
Tactic: have hm : m < n := lt_of_le_of_lt le_self_add hkm
-- 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have hk : k < n
Tactic: have hk : k < n := lt_of_le_of_lt le_add_self 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have 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)
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]
-- 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ (↑k ! : A)⁻¹ʳ * x ^ (m + k) =
    HMul.hMul (α := A) (↑((m + k).choose m) : A) (↑(m + k)! : A)⁻¹ʳ * x ^ (m + k)
have apply : HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ (↑k ! : A)⁻¹ʳ = HMul.hMul (α := A) (↑((m + k).choose m) : 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ HMul.hMul (α := A) (↑m ! : A)⁻¹ʳ (↑k ! : A)⁻¹ʳ = HMul.hMul (α := A) (↑((m + k).choose m) : A) (↑(m + k)! : A)⁻¹ʳ
have rw : (↑(m + k)! : A) = (↑k ! : A) * HMul.hMul (α := A) (↑m ! : A) (↑((m + k).choose m) : 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)]
-- 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (↑(m + k)! : A) = (↑k ! : A) * HMul.hMul (α := A) (↑m ! : A) (↑((m + k).choose m) : A)
have norm_cast : Eq.{u_1 + 1} (α := A) (↑(m + k)! : A) (↑(k ! * (m ! * (m + k).choose m)) : A)
Tactic: norm_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)
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ Eq.{u_1 + 1} (α := A) (↑(m + k)! : A) (↑(k ! * (m ! * (m + k).choose m)) : A)
have h : (m + k)! = k ! * (m ! * (m + k).choose m)
Tactic: apply congr_arg
-- 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 : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ (m + k)! = k ! * (m ! * (m + k).choose m)
have h : (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]
-- 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 : ℕ
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)
⊢ (m + k)! = k ! * (m ! * (m + k).choose m)
have h₁ : k ! * ((m + k).choose k * m !) = k ! * (m ! * (m + k).choose m)
Tactic: rw [← Nat.add_choose_mul_factorial_mul_factorial, mul_comm, mul_comm _ (m !), Nat.choose_symm_add]
-- 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 : ℕ
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)
⊢ (m + k)! = k ! * (m ! * (m + k).choose m)
have h₂ : k ! * (m ! * (m + k).choose 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]
-- 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 : ℕ
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)
⊢ (m + k)! = k ! * (m ! * (m + k).choose m)
have h₃ : k ! * (m ! * (m + k).choose k) = k ! * (m ! * (m + k).choose k)
Tactic: rw [← Nat.add_choose_mul_factorial_mul_factorial, mul_comm, mul_comm _ (m !), Nat.choose_symm_add]
-- 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
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have pos : ∀ (hkm : m + k < n), 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
-- 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
pos : ∀ (hkm : m + k < n), 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
have neg : ∀ (hkm : n ≤ m + k), 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
-- 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 : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : 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 hkm 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 : ℕ
x : A
hx : x ∈ I
hkm : n ≤ m + k
hxmk : x ^ (m + k) = 0
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg : (↑m ! : A)⁻¹ʳ * x ^ m * 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]
-- 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
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₁ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * x ^ k) = (↑((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]
-- 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
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₂ : (↑m ! : A)⁻¹ʳ * x ^ m * ((↑k ! : A)⁻¹ʳ * 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))
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₃ : (↑m ! : A)⁻¹ʳ * (x ^ m * ((↑k ! : A)⁻¹ʳ * 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))
⊢ dpow I m x * dpow I k x = (↑((m + k).choose m) : A) * dpow I (m + k) x
have neg₄ : (↑m ! : A)⁻¹ʳ * (x ^ m * (↑k ! : A)⁻¹ʳ * 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))
⊢ 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]