awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
⊢ HMul.hMul (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ m = 0 then 1 else 0)
      (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) =
    HMul.hMul (α := A) (↑((m + n).choose m) : A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ m + n = 0 then 1 else 0)
have simp : Eq.{u_1 + 1} (α := A) (if n = 0 then if m = 0 then 1 else 0 else 0)
  (if m = 0 ∧ n = 0 then (↑((m + n).choose m) : A) else 0)
Tactic: simp only [true_and, mul_ite, mul_one, mul_zero, add_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
⊢ Eq.{u_1 + 1} (α := A) (if n = 0 then if m = 0 then 1 else 0 else 0)
    (if m = 0 ∧ n = 0 then (↑((m + n).choose m) : A) else 0)
have pos : ∀ (hn : n = 0),
  Eq.{u_1 + 1} (α := A) (if n = 0 then if m = 0 then 1 else 0 else 0)
    (if m = 0 ∧ n = 0 then (↑((m + n).choose m) : A) else 0)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
pos :
  ∀ (hn : n = 0),
    Eq.{u_1 + 1} (α := A) (if n = 0 then if m = 0 then 1 else 0 else 0)
      (if m = 0 ∧ n = 0 then (↑((m + n).choose m) : A) else 0)
⊢ Eq.{u_1 + 1} (α := A) (if n = 0 then if m = 0 then 1 else 0 else 0)
    (if m = 0 ∧ n = 0 then (↑((m + n).choose m) : A) else 0)
have neg : ∀ (hn : ¬n = 0),
  Eq.{u_1 + 1} (α := A) (if n = 0 then if m = 0 then 1 else 0 else 0)
    (if m = 0 ∧ n = 0 then (↑((m + n).choose m) : A) else 0)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
hn : ¬n = 0
⊢ Eq.{u_1 + 1} (α := A) (if n = 0 then if m = 0 then 1 else 0 else 0)
    (if m = 0 ∧ n = 0 then (↑((m + n).choose m) : A) else 0)
have neg : ¬(m = 0 ∧ n = 0)
Tactic: rw [if_neg hn, if_neg]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : Membership.mem (γ := Ideal A) ⊥ a
⊢ (if Eq.{u_1 + 1} (α := A) (if a = 0 ∧ n = 0 then 1 else 0) 0 ∧ m = 0 then 1 else 0) =
    HMul.hMul (α := A) (↑(m.uniformBell n) : A) (if a = 0 ∧ m * n = 0 then 1 else 0)
have rw : (if Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) 0 ∧ m = 0 then 1 else 0) =
  HMul.hMul (α := A) (↑(m.uniformBell n) : A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ m * n = 0 then 1 else 0)
Tactic: rw [mem_bot.mp ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : Membership.mem (γ := Ideal A) ⊥ a
⊢ (if Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) 0 ∧ m = 0 then 1 else 0) =
    HMul.hMul (α := A) (↑(m.uniformBell n) : A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ m * n = 0 then 1 else 0)
have simp : Eq.{u_1 + 1} (α := A)
  (if Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) 0 ∧ m = 0 then 1 else 0)
  (if m = 0 ∨ n = 0 then (↑(m.uniformBell n) : A) else 0)
Tactic: simp only [true_and, ite_eq_right_iff, _root_.mul_eq_zero, mul_ite, mul_one, mul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : Membership.mem (γ := Ideal A) ⊥ a
⊢ Eq.{u_1 + 1} (α := A)
    (if Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) 0 ∧ m = 0 then 1 else 0)
    (if m = 0 ∨ n = 0 then (↑(m.uniformBell n) : A) else 0)
have pos : ∀ (hm : m = 0),
  Eq.{u_1 + 1} (α := A)
    (if Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) 0 ∧ m = 0 then 1 else 0)
    (if m = 0 ∨ n = 0 then (↑(m.uniformBell n) : A) else 0)
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : Membership.mem (γ := Ideal A) ⊥ a
pos :
  ∀ (hm : m = 0),
    Eq.{u_1 + 1} (α := A)
      (if Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) 0 ∧ m = 0 then 1 else 0)
      (if m = 0 ∨ n = 0 then (↑(m.uniformBell n) : A) else 0)
⊢ Eq.{u_1 + 1} (α := A)
    (if Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) 0 ∧ m = 0 then 1 else 0)
    (if m = 0 ∨ n = 0 then (↑(m.uniformBell n) : A) else 0)
have neg : ∀ (hm : ¬m = 0),
  Eq.{u_1 + 1} (α := A)
    (if Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0) 0 ∧ m = 0 then 1 else 0)
    (if m = 0 ∨ n = 0 then (↑(m.uniformBell n) : A) else 0)
Tactic: by_cases hm : m = 0
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
⊢ hI = hI'
have obtain : ∀ (hI : ℕ → A → A) (h₀ : ∀ {n : ℕ} {x : A}, x ∉ I → hI n x = 0) (dpow_zero : ∀ {x : A}, x ∈ I → hI 0 x = 1)
  (dpow_one : ∀ {x : A}, x ∈ I → hI 1 x = x) (dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI n x ∈ I)
  (dpow_add :
    ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → hI n (x + y) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI k.1 x * hI k.2 y)
  (dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → hI n (a * x) = a ^ n * hI n x)
  (mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → hI m x * hI n x = (↑((m + n).choose m) : A) * hI (m + n) x)
  (dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI m (hI n x) = (↑(m.uniformBell n) : A) * hI (m * n) x)
  (h_eq :
    ∀ (n : ℕ) {x : A},
      x ∈ I →
        { dpow := hI, dpow_null := @h₀, dpow_zero := @dpow_zero, dpow_one := @dpow_one, dpow_mem := @dpow_mem,
                dpow_add := @dpow_add, dpow_mul := @dpow_mul, mul_dpow := @mul_dpow, dpow_comp := @dpow_comp :
                DividedPowers I }.dpow
            n x =
          hI'.dpow n x),
  { dpow := hI, dpow_null := @h₀, dpow_zero := @dpow_zero, dpow_one := @dpow_one, dpow_mem := @dpow_mem,
      dpow_add := @dpow_add, dpow_mul := @dpow_mul, mul_dpow := @mul_dpow, dpow_comp := @dpow_comp : DividedPowers I } =
    hI'
Tactic: obtain ⟨hI, h₀, _⟩ := hI
Cleared hypotheses: hI, h_eq
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI' : DividedPowers I
hI : ℕ → A → A
h₀ : ∀ {n : ℕ} {x : A}, x ∉ I → hI n x = 0
dpow_zero : ∀ {x : A}, x ∈ I → hI 0 x = 1
dpow_one : ∀ {x : A}, x ∈ I → hI 1 x = x
dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI n x ∈ I
dpow_add :
  ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → hI n (x + y) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI k.1 x * hI k.2 y
dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → hI n (a * x) = a ^ n * hI n x
mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → hI m x * hI n x = (↑((m + n).choose m) : A) * hI (m + n) x
dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI m (hI n x) = (↑(m.uniformBell n) : A) * hI (m * n) x
h_eq :
  ∀ (n : ℕ) {x : A},
    x ∈ I →
      { dpow := hI, dpow_null := @h₀, dpow_zero := @dpow_zero, dpow_one := @dpow_one, dpow_mem := @dpow_mem,
              dpow_add := @dpow_add, dpow_mul := @dpow_mul, mul_dpow := @mul_dpow, dpow_comp := @dpow_comp :
              DividedPowers I }.dpow
          n x =
        hI'.dpow n x
⊢ { dpow := hI, dpow_null := @h₀, dpow_zero := @dpow_zero, dpow_one := @dpow_one, dpow_mem := @dpow_mem,
      dpow_add := @dpow_add, dpow_mul := @dpow_mul, mul_dpow := @mul_dpow, dpow_comp := @dpow_comp : DividedPowers I } =
    hI'
have obtain : ∀ (hI' : ℕ → A → A) (h₀' : ∀ {n : ℕ} {x : A}, x ∉ I → hI' n x = 0) (dpow_zero_1 : ∀ {x : A}, x ∈ I → hI' 0 x = 1)
  (dpow_one_1 : ∀ {x : A}, x ∈ I → hI' 1 x = x) (dpow_mem_1 : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI' n x ∈ I)
  (dpow_add_1 :
    ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → hI' n (x + y) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI' k.1 x * hI' k.2 y)
  (dpow_mul_1 : ∀ {n : ℕ} {a x : A}, x ∈ I → hI' n (a * x) = a ^ n * hI' n x)
  (mul_dpow_1 : ∀ {m n : ℕ} {x : A}, x ∈ I → hI' m x * hI' n x = (↑((m + n).choose m) : A) * hI' (m + n) x)
  (dpow_comp_1 : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI' m (hI' n x) = (↑(m.uniformBell n) : A) * hI' (m * n) x)
  (h_eq :
    ∀ (n : ℕ) {x : A},
      x ∈ I →
        { dpow := hI, dpow_null := @h₀, dpow_zero := @dpow_zero, dpow_one := @dpow_one, dpow_mem := @dpow_mem,
                dpow_add := @dpow_add, dpow_mul := @dpow_mul, mul_dpow := @mul_dpow, dpow_comp := @dpow_comp :
                DividedPowers I }.dpow
            n x =
          { dpow := hI', dpow_null := @h₀', dpow_zero := @dpow_zero_1, dpow_one := @dpow_one_1, dpow_mem := @dpow_mem_1,
                dpow_add := @dpow_add_1, dpow_mul := @dpow_mul_1, mul_dpow := @mul_dpow_1, dpow_comp := @dpow_comp_1 :
                DividedPowers I }.dpow
            n x),
  { dpow := hI, dpow_null := @h₀, dpow_zero := @dpow_zero, dpow_one := @dpow_one, dpow_mem := @dpow_mem,
      dpow_add := @dpow_add, dpow_mul := @dpow_mul, mul_dpow := @mul_dpow, dpow_comp := @dpow_comp : DividedPowers I } =
    { dpow := hI', dpow_null := @h₀', dpow_zero := @dpow_zero_1, dpow_one := @dpow_one_1, dpow_mem := @dpow_mem_1,
      dpow_add := @dpow_add_1, dpow_mul := @dpow_mul_1, mul_dpow := @mul_dpow_1, dpow_comp := @dpow_comp_1 }
Tactic: obtain ⟨hI', h₀', _⟩ := hI'
Cleared hypotheses: hI', h_eq
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : ℕ → A → A
h₀ : ∀ {n : ℕ} {x : A}, x ∉ I → hI n x = 0
dpow_zero : ∀ {x : A}, x ∈ I → hI 0 x = 1
dpow_one : ∀ {x : A}, x ∈ I → hI 1 x = x
dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI n x ∈ I
dpow_add :
  ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → hI n (x + y) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI k.1 x * hI k.2 y
dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → hI n (a * x) = a ^ n * hI n x
mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → hI m x * hI n x = (↑((m + n).choose m) : A) * hI (m + n) x
dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI m (hI n x) = (↑(m.uniformBell n) : A) * hI (m * n) x
hI' : ℕ → A → A
h₀' : ∀ {n : ℕ} {x : A}, x ∉ I → hI' n x = 0
dpow_zero_1 : ∀ {x : A}, x ∈ I → hI' 0 x = 1
dpow_one_1 : ∀ {x : A}, x ∈ I → hI' 1 x = x
dpow_mem_1 : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI' n x ∈ I
dpow_add_1 :
  ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → hI' n (x + y) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI' k.1 x * hI' k.2 y
dpow_mul_1 : ∀ {n : ℕ} {a x : A}, x ∈ I → hI' n (a * x) = a ^ n * hI' n x
mul_dpow_1 : ∀ {m n : ℕ} {x : A}, x ∈ I → hI' m x * hI' n x = (↑((m + n).choose m) : A) * hI' (m + n) x
dpow_comp_1 : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI' m (hI' n x) = (↑(m.uniformBell n) : A) * hI' (m * n) x
h_eq :
  ∀ (n : ℕ) {x : A},
    x ∈ I →
      { dpow := hI, dpow_null := @h₀, dpow_zero := @dpow_zero, dpow_one := @dpow_one, dpow_mem := @dpow_mem,
              dpow_add := @dpow_add, dpow_mul := @dpow_mul, mul_dpow := @mul_dpow, dpow_comp := @dpow_comp :
              DividedPowers I }.dpow
          n x =
        { dpow := hI', dpow_null := @h₀', dpow_zero := @dpow_zero_1, dpow_one := @dpow_one_1, dpow_mem := @dpow_mem_1,
              dpow_add := @dpow_add_1, dpow_mul := @dpow_mul_1, mul_dpow := @mul_dpow_1, dpow_comp := @dpow_comp_1 :
              DividedPowers I }.dpow
          n x
⊢ { dpow := hI, dpow_null := @h₀, dpow_zero := @dpow_zero, dpow_one := @dpow_one, dpow_mem := @dpow_mem,
      dpow_add := @dpow_add, dpow_mul := @dpow_mul, mul_dpow := @mul_dpow, dpow_comp := @dpow_comp : DividedPowers I } =
    { dpow := hI', dpow_null := @h₀', dpow_zero := @dpow_zero_1, dpow_one := @dpow_one_1, dpow_mem := @dpow_mem_1,
      dpow_add := @dpow_add_1, dpow_mul := @dpow_mul_1, mul_dpow := @mul_dpow_1, dpow_comp := @dpow_comp_1 }
have simp : hI = hI'
Tactic: simp only [mk.injEq]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h : Eq.{u_1 + 1} (α := ℕ → A → A) ((fun (h : DividedPowers I) ↦ h.dpow) hI) ((fun (h : DividedPowers I) ↦ h.dpow) hI')
⊢ hI = hI'
have h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
Tactic: ext n x
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
hb : b ∈ I
⊢ hI.dpow n (a + b) = ∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b
have rw : Eq.{u_1 + 1} (α := A) (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI.dpow k.1 a * hI.dpow k.2 b)
  (∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b)
Tactic: rw [hI.dpow_add ha hb, sum_antidiagonal_eq_sum_range_succ_mk]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
hb : b ∈ I
rw :
  Eq.{u_1 + 1} (α := A) (∑ k ∈ @antidiagonal _ instAddMonoid _ n, hI.dpow k.1 a * hI.dpow k.2 b)
    (∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b)
⊢ hI.dpow n (a + b) = ∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b
have rw₁ : Eq.{u_1 + 1} (α := A) (∑ k ∈ range n.succ, hI.dpow (k, n - k).1 a * hI.dpow (k, n - k).2 b)
  (∑ k ∈ range (n + 1), hI.dpow k a * hI.dpow (n - k) b)
Tactic: rw [hI.dpow_add ha hb, sum_antidiagonal_eq_sum_range_succ_mk]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
a b : A
dp : ℕ → A → A
dp_add : ∀ (n : ℕ), dp n (a + b) = ∑ k ∈ @antidiagonal _ instAddMonoid _ n, dp k.1 a * dp k.2 b
⊢ (PowerSeries.mk fun (n : ℕ) ↦ dp n (a + b)) =
    HMul.hMul (α := PowerSeries A) (PowerSeries.mk fun (n : ℕ) ↦ dp n a) (PowerSeries.mk fun (n : ℕ) ↦ dp n b)
have h : ∀ (n : ℕ),
  Eq (α := A) ((PowerSeries.coeff n : (a : PowerSeries A) → A) (PowerSeries.mk fun (n : ℕ) ↦ dp n (a + b)) : A)
    ((PowerSeries.coeff n : (a : PowerSeries A) → A)
        (HMul.hMul (α := PowerSeries A) (PowerSeries.mk fun (n : ℕ) ↦ dp n a) (PowerSeries.mk fun (n : ℕ) ↦ dp n b)) :
      A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (a * b) = hI.dpow n a * b ^ n
have rw : hI.dpow n (b * a) = hI.dpow n a * b ^ n
Tactic: rw [mul_comm, hI.dpow_mul ha, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
rw : hI.dpow n (b * a) = hI.dpow n a * b ^ n
⊢ hI.dpow n (a * b) = hI.dpow n a * b ^ n
have rw₁ : b ^ n * hI.dpow n a = hI.dpow n a * b ^ n
Tactic: rw [mul_comm, hI.dpow_mul ha, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
rw : hI.dpow n (b * a) = hI.dpow n a * b ^ n
rw₁ : b ^ n * hI.dpow n a = hI.dpow n a * b ^ n
⊢ hI.dpow n (a * b) = hI.dpow n a * b ^ n
have rw₂ : hI.dpow n a * b ^ n = hI.dpow n a * b ^ n
Tactic: rw [mul_comm, hI.dpow_mul ha, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (a • b) = hI.dpow n a • b ^ n
have rw : hI.dpow n (a * b) = hI.dpow n a • b ^ n
Tactic: rw [smul_eq_mul, hI.dpow_mul_right ha, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
rw : hI.dpow n (a * b) = hI.dpow n a • b ^ n
⊢ hI.dpow n (a • b) = hI.dpow n a • b ^ n
have rw₁ : hI.dpow n a * b ^ n = hI.dpow n a • b ^ n
Tactic: rw [smul_eq_mul, hI.dpow_mul_right ha, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
rw : hI.dpow n (a * b) = hI.dpow n a • b ^ n
rw₁ : hI.dpow n a * b ^ n = hI.dpow n a • b ^ n
⊢ hI.dpow n (a • b) = hI.dpow n a • b ^ n
have rw₂ : hI.dpow n a * b ^ n = hI.dpow n a * b ^ n
Tactic: rw [smul_eq_mul, hI.dpow_mul_right ha, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
⊢ (↑0! : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
have zero : (↑1 : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
Tactic: rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
zero : (↑1 : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
⊢ (↑0! : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
have zero₁ : 1 * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
Tactic: rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
zero : (↑1 : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
zero₁ : 1 * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
⊢ (↑0! : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
have zero₂ : hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
Tactic: rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
zero : (↑1 : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
zero₁ : 1 * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
zero₂ : hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
⊢ (↑0! : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
have zero₃ : hI.dpow 0 a = 1
Tactic: rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
zero : (↑1 : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
zero₁ : 1 * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
zero₂ : hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
zero₃ : hI.dpow 0 a = 1
⊢ (↑0! : A) * hI.dpow 0 a = HPow.hPow (β := ℕ) a 0
have zero₄ : Eq.{u_1 + 1} (α := A) 1 1
Tactic: rw [factorial_zero, cast_one, one_mul, pow_zero, hI.dpow_zero ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
⊢ (↑(n + 1)! : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ : (↑(n ! * (n + 1)) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
Tactic: rw [factorial_succ, mul_comm (n + 1)]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
⊢ (↑(n ! * (n + 1)) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ : (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
Tactic: nth_rewrite 1 [← (n + 1).choose_one_right]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
Tactic: rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ₁ : HMul.hMul (α := A) (↑n ! : A) (↑((n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
Tactic: rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₁ : HMul.hMul (α := A) (↑n ! : A) (↑((n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ₂ : (↑n ! : A) * ((↑((n + 1).choose n) : A) * hI.dpow (n + 1) a) = a ^ (n + 1)
Tactic: rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₁ : HMul.hMul (α := A) (↑n ! : A) (↑((n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₂ : (↑n ! : A) * ((↑((n + 1).choose n) : A) * hI.dpow (n + 1) a) = a ^ (n + 1)
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ₃ : (↑n ! : A) * (hI.dpow n a * hI.dpow 1 a) = a ^ (n + 1)
Tactic: rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₁ : HMul.hMul (α := A) (↑n ! : A) (↑((n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₂ : (↑n ! : A) * ((↑((n + 1).choose n) : A) * hI.dpow (n + 1) a) = a ^ (n + 1)
succ₃ : (↑n ! : A) * (hI.dpow n a * hI.dpow 1 a) = a ^ (n + 1)
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ₄ : (↑n ! : A) * hI.dpow n a * hI.dpow 1 a = a ^ (n + 1)
Tactic: rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₁ : HMul.hMul (α := A) (↑n ! : A) (↑((n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₂ : (↑n ! : A) * ((↑((n + 1).choose n) : A) * hI.dpow (n + 1) a) = a ^ (n + 1)
succ₃ : (↑n ! : A) * (hI.dpow n a * hI.dpow 1 a) = a ^ (n + 1)
succ₄ : (↑n ! : A) * hI.dpow n a * hI.dpow 1 a = a ^ (n + 1)
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ₅ : a ^ n * hI.dpow 1 a = a ^ (n + 1)
Tactic: rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
a : A
hI : DividedPowers I
ha : a ∈ I
n : ℕ
ih : (↑n ! : A) * hI.dpow n a = a ^ n
succ : (↑(n ! * (n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₁ : HMul.hMul (α := A) (↑n ! : A) (↑((n + 1).choose n) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
succ₂ : (↑n ! : A) * ((↑((n + 1).choose n) : A) * hI.dpow (n + 1) a) = a ^ (n + 1)
succ₃ : (↑n ! : A) * (hI.dpow n a * hI.dpow 1 a) = a ^ (n + 1)
succ₄ : (↑n ! : A) * hI.dpow n a * hI.dpow 1 a = a ^ (n + 1)
succ₅ : a ^ n * hI.dpow 1 a = a ^ (n + 1)
⊢ (↑(n ! * (n + 1).choose 1) : A) * hI.dpow (n + 1) a = a ^ (n + 1)
have succ₆ : a ^ n * a = a ^ (n + 1)
Tactic: rw [← choose_symm_add, cast_mul, mul_assoc,
      ← hI.mul_dpow ha, ← mul_assoc, ih, hI.dpow_one ha, pow_succ, mul_comm]