awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
y : B
hy : y ∈ J
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
⊢ dpow hI f n (HAdd.hAdd (α := B) ((f : (a : A) → B) a : B) y) =
    ∑ k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, dpow hI f k.1 ((f : (a : A) → B) a) * dpow hI f k.2 y
have obtain : ∀ (b : A) (hb : b ∈ I) (hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)),
  dpow hI f n (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    ∑ k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      dpow hI f k.1 ((f : (a : A) → B) a) * dpow hI f k.2 ((f : (a : A) → B) b)
Tactic: obtain ⟨b, hb, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hy)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
⊢ dpow hI f n (HAdd.hAdd (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    ∑ k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      dpow hI f k.1 ((f : (a : A) → B) a) * dpow hI f k.2 ((f : (a : A) → B) b)
have rw : ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
  (f : (a : A) → B) (hI.dpow x.1 a * hI.dpow x.2 b) =
    dpow hI f x.1 ((f : (a : A) → B) a) * dpow hI f x.2 ((f : (a : A) → B) b)
Tactic: rw [← map_add, dpow_apply' hI hIf (I.add_mem ha hb), hI.dpow_add ha hb, map_sum,
      Finset.sum_congr rfl]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
k : ℕ × ℕ
h : k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
⊢ (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
    dpow hI f k.1 ((f : (a : A) → B) a) * dpow hI f k.2 ((f : (a : A) → B) b)
have rw : (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
  HMul.hMul (α := B) ((f : (a : A) → B) (hI.dpow k.1 a) : B) (dpow hI f k.2 ((f : (a : A) → B) b))
Tactic: rw [dpow_apply' hI hIf ha, dpow_apply' hI hIf hb, ← _root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
k : ℕ × ℕ
h : k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
rw :
  (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
    HMul.hMul (α := B) ((f : (a : A) → B) (hI.dpow k.1 a) : B) (dpow hI f k.2 ((f : (a : A) → B) b))
⊢ (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
    dpow hI f k.1 ((f : (a : A) → B) a) * dpow hI f k.2 ((f : (a : A) → B) b)
have rw₁ : (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (hI.dpow k.1 a) : B) ((f : (a : A) → B) (hI.dpow k.2 b) : B)
Tactic: rw [dpow_apply' hI hIf ha, dpow_apply' hI hIf hb, ← _root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
k : ℕ × ℕ
h : k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
rw :
  (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
    HMul.hMul (α := B) ((f : (a : A) → B) (hI.dpow k.1 a) : B) (dpow hI f k.2 ((f : (a : A) → B) b))
rw₁ :
  (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (hI.dpow k.1 a) : B) ((f : (a : A) → B) (hI.dpow k.2 b) : B)
⊢ (f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) =
    dpow hI f k.1 ((f : (a : A) → B) a) * dpow hI f k.2 ((f : (a : A) → B) b)
have rw₂ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) : B)
  ((f : (a : A) → B) (hI.dpow k.1 a * hI.dpow k.2 b) : B)
Tactic: rw [dpow_apply' hI hIf ha, dpow_apply' hI hIf hb, ← _root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
x y : B
hy : y ∈ J
⊢ dpow hI f n (x * y) = x ^ n * dpow hI f n y
have obtain : ∀ (a : A),
  dpow hI f n (HMul.hMul (α := B) ((f : (a : A) → B) a : B) y) =
    HPow.hPow (α := B) ((f : (a : A) → B) a : B) n * dpow hI f n y
Tactic: obtain ⟨a, rfl⟩ := hf x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
y : B
hy : y ∈ J
a : A
⊢ dpow hI f n (HMul.hMul (α := B) ((f : (a : A) → B) a : B) y) =
    HPow.hPow (α := B) ((f : (a : A) → B) a : B) n * dpow hI f n y
have obtain : ∀ (b : A) (hb : b ∈ I) (hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)),
  dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HPow.hPow (α := B) ((f : (a : A) → B) a : B) n * dpow hI f n ((f : (a : A) → B) b)
Tactic: obtain ⟨b, hb, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hy)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
⊢ dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HPow.hPow (α := B) ((f : (a : A) → B) a : B) n * dpow hI f n ((f : (a : A) → B) b)
have rw : dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
  HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
Tactic: rw [dpow_apply' hI hIf hb, ← _root_.map_mul, ← map_pow,
      dpow_apply' hI hIf (mul_mem_left I a hb), hI.dpow_mul hb, _root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
rw :
  dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
⊢ dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HPow.hPow (α := B) ((f : (a : A) → B) a : B) n * dpow hI f n ((f : (a : A) → B) b)
have rw₁ : dpow hI f n ((f : (a : A) → B) (a * b)) =
  HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
Tactic: rw [dpow_apply' hI hIf hb, ← _root_.map_mul, ← map_pow,
      dpow_apply' hI hIf (mul_mem_left I a hb), hI.dpow_mul hb, _root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
rw :
  dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₁ :
  dpow hI f n ((f : (a : A) → B) (a * b)) =
    HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
⊢ dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HPow.hPow (α := B) ((f : (a : A) → B) a : B) n * dpow hI f n ((f : (a : A) → B) b)
have rw₂ : dpow hI f n ((f : (a : A) → B) (a * b)) =
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
Tactic: rw [dpow_apply' hI hIf hb, ← _root_.map_mul, ← map_pow,
      dpow_apply' hI hIf (mul_mem_left I a hb), hI.dpow_mul hb, _root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
rw :
  dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₁ :
  dpow hI f n ((f : (a : A) → B) (a * b)) =
    HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₂ :
  dpow hI f n ((f : (a : A) → B) (a * b)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
⊢ dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HPow.hPow (α := B) ((f : (a : A) → B) a : B) n * dpow hI f n ((f : (a : A) → B) b)
have rw₃ : (f : (a : A) → B) (hI.dpow n (a * b)) =
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
Tactic: rw [dpow_apply' hI hIf hb, ← _root_.map_mul, ← map_pow,
      dpow_apply' hI hIf (mul_mem_left I a hb), hI.dpow_mul hb, _root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
rw :
  dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₁ :
  dpow hI f n ((f : (a : A) → B) (a * b)) =
    HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₂ :
  dpow hI f n ((f : (a : A) → B) (a * b)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₃ :
  (f : (a : A) → B) (hI.dpow n (a * b)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
⊢ dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HPow.hPow (α := B) ((f : (a : A) → B) a : B) n * dpow hI f n ((f : (a : A) → B) b)
have rw₄ : (f : (a : A) → B) (a ^ n * hI.dpow n b) =
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
Tactic: rw [dpow_apply' hI hIf hb, ← _root_.map_mul, ← map_pow,
      dpow_apply' hI hIf (mul_mem_left I a hb), hI.dpow_mul hb, _root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a b : A
hb : b ∈ I
hy : Membership.mem (α := B) J ((f : (a : A) → B) b : B)
rw :
  dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₁ :
  dpow hI f n ((f : (a : A) → B) (a * b)) =
    HMul.hMul (β := B) (HPow.hPow (α := B) ((f : (a : A) → B) a : B) n) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₂ :
  dpow hI f n ((f : (a : A) → B) (a * b)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₃ :
  (f : (a : A) → B) (hI.dpow n (a * b)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
rw₄ :
  (f : (a : A) → B) (a ^ n * hI.dpow n b) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
⊢ dpow hI f n (HMul.hMul (α := B) (β := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) b : B)) =
    HPow.hPow (α := B) ((f : (a : A) → B) a : B) n * dpow hI f n ((f : (a : A) → B) b)
have rw₅ : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B) =
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (a ^ n) : B) ((f : (a : A) → B) (hI.dpow n b) : B)
Tactic: rw [dpow_apply' hI hIf hb, ← _root_.map_mul, ← map_pow,
      dpow_apply' hI hIf (mul_mem_left I a hb), hI.dpow_mul hb, _root_.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m n : ℕ
x : B
hx : x ∈ J
⊢ dpow hI f m x * dpow hI f n x = (↑((m + n).choose m) : B) * dpow hI f (m + n) x
have obtain : ∀ (a : A) (ha : a ∈ I) (hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)),
  dpow hI f m ((f : (a : A) → B) a) * dpow hI f n ((f : (a : A) → B) a) =
    (↑((m + n).choose m) : B) * dpow hI f (m + n) ((f : (a : A) → B) a)
Tactic: obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
⊢ dpow hI f m ((f : (a : A) → B) a) * dpow hI f n ((f : (a : A) → B) a) =
    (↑((m + n).choose m) : B) * dpow hI f (m + n) ((f : (a : A) → B) a)
have simp : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (hI.dpow m a) : B) ((f : (a : A) → B) (hI.dpow n a) : B) =
  HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
Tactic: simp only [dpow_apply' hI hIf ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
⊢ HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (hI.dpow m a) : B) ((f : (a : A) → B) (hI.dpow n a) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
have rw : (f : (a : A) → B) (hI.dpow m a * hI.dpow n a) =
  HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
Tactic: rw [← _root_.map_mul, hI.mul_dpow ha, _root_.map_mul, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
rw :
  (f : (a : A) → B) (hI.dpow m a * hI.dpow n a) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
⊢ HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (hI.dpow m a) : B) ((f : (a : A) → B) (hI.dpow n a) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
have rw₁ : (f : (a : A) → B) ((↑((m + n).choose m) : A) * hI.dpow (m + n) a) =
  HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
Tactic: rw [← _root_.map_mul, hI.mul_dpow ha, _root_.map_mul, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
rw :
  (f : (a : A) → B) (hI.dpow m a * hI.dpow n a) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
rw₁ :
  (f : (a : A) → B) ((↑((m + n).choose m) : A) * hI.dpow (m + n) a) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
⊢ HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (hI.dpow m a) : B) ((f : (a : A) → B) (hI.dpow n a) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
have rw₂ : HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (↑((m + n).choose m) : A) : B)
    ((f : (a : A) → B) (hI.dpow (m + n) a) : B) =
  HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
Tactic: rw [← _root_.map_mul, hI.mul_dpow ha, _root_.map_mul, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m n : ℕ
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
rw :
  (f : (a : A) → B) (hI.dpow m a * hI.dpow n a) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
rw₁ :
  (f : (a : A) → B) ((↑((m + n).choose m) : A) * hI.dpow (m + n) a) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
rw₂ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (↑((m + n).choose m) : A) : B)
      ((f : (a : A) → B) (hI.dpow (m + n) a) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
⊢ HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (hI.dpow m a) : B) ((f : (a : A) → B) (hI.dpow n a) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
have rw₃ : HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B) =
  HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B) ((f : (a : A) → B) (hI.dpow (m + n) a) : B)
Tactic: rw [← _root_.map_mul, hI.mul_dpow ha, _root_.map_mul, map_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ dpow hI f m (dpow hI f n x) = (↑(m.uniformBell n) : B) * dpow hI f (m * n) x
have obtain : ∀ (a : A) (ha : a ∈ I) (hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)),
  dpow hI f m (dpow hI f n ((f : (a : A) → B) a)) = (↑(m.uniformBell n) : B) * dpow hI f (m * n) ((f : (a : A) → B) a)
Tactic: obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
⊢ dpow hI f m (dpow hI f n ((f : (a : A) → B) a)) = (↑(m.uniformBell n) : B) * dpow hI f (m * n) ((f : (a : A) → B) a)
have simp : (f : (a : A) → B) (hI.dpow m (hI.dpow n a)) =
  HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
Tactic: simp only [dpow_apply' hI hIf, ha, hI.dpow_mem hn ha]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.SubDPIdeal (goal)
Goal:
A : Type u_1
inst : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst_1 : CommRing B
f : A →+* B
J : Ideal B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
⊢ (f : (a : A) → B) (hI.dpow m (hI.dpow n a)) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
have rw : (f : (a : A) → B) ((↑(m.uniformBell n) : A) * hI.dpow (m * n) a) =
  HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
Tactic: rw [hI.dpow_comp hn ha, _root_.map_mul, map_natCast]