awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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 : B
hx' : x ∉ J
rw :
  Eq (α := B)
    (Function.extend (fun (a : ↥I) ↦ (f : (a : A) → B) (↑a : A)) (fun (a : ↥I) ↦ (f : (a : A) → B) (hI.dpow n (↑a : A)))
      0 x)
    0
rw₁ :
  Eq.{u_2 + 1} (α := B)
    (if h : ∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x then
      (f : (a : A) → B) (hI.dpow n (↑(Classical.choose (p := fun (x_1 : ↥I) ↦ (f : (a : A) → B) (↑x_1 : A) = x) h) : A))
    else 0 x)
    0
rw₂ : Eq.{u_2 + 1} (α := B) (0 x) 0
hnc : ¬∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x
rw₃ : Eq.{u_2 + 1} (α := B) 0 0
hnc₁ : ¬∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x
rw₄ : Eq.{u_2 + 1} (α := B) 0 0
hnc₂ hnc₃ : ¬∃ (a : ↥I), (f : (a : A) → B) (↑a : A) = x
hnc₄ :
  ∀ (a : A) (ha : a ∈ I) (hx' : ((f : (a : A) → B) (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ I) a ha) : A) : B) ∉ J), False
⊢ dpow hI f n x = 0

Tactic:
classical
    rw [dpow, Function.extend_def, dif_neg, Pi.zero_apply]
    rintro ⟨⟨a, ha⟩, rfl⟩
    exact (hIJ ▸ hx') (apply_coe_mem_map f I ⟨a, ha⟩)

Premises used: Function.extend_def, Pi.zero_apply, dif_neg, DividedPowers.Quotient.OfSurjective.dpow, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
x : B
hx : x ∈ J
obtain :
  ∀ (a : A) (ha : a ∈ I) (hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)),
    dpow hI f 0 ((f : (a : A) → B) a) = 1
⊢ dpow hI f 0 x = 1

Tactic:
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
a : A
ha : a ∈ I
hx : Membership.mem (α := B) J ((f : (a : A) → B) a : B)
rw : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow 0 a) : B) (1 : B)
rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
rw₂ rw₃ : Eq.{u_2 + 1} (α := B) 1 1
⊢ dpow hI f 0 ((f : (a : A) → B) a) = 1

Tactic:
rw [dpow_apply' hI hIf ha, hI.dpow_zero ha, map_one]

Premises used: DividedPowers.Quotient.OfSurjective.dpow_apply', DividedPowers.dpow_zero, map_one
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
x : B
hx : x ∈ J
obtain : ∀ (a : A) (ha : a ∈ I) (hax : (f : (a : A) → B) a = x), dpow hI f 1 x = x
⊢ dpow hI f 1 x = x

Tactic:
obtain ⟨a, ha, hax⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
x : B
hx : x ∈ J
a : A
ha : a ∈ I
hax : (f : (a : A) → B) a = x
rw : dpow hI f 1 ((f : (a : A) → B) a) = (f : (a : A) → B) a
rw₁ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow 1 a) : B) ((f : (a : A) → B) a : B)
rw₂ rw₃ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) a : B) ((f : (a : A) → B) a : B)
⊢ dpow hI f 1 x = x

Tactic:
rw [← hax, dpow_apply' hI hIf ha, hI.dpow_one ha]

Premises used: DividedPowers.Quotient.OfSurjective.dpow_apply', DividedPowers.dpow_one
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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 : B
hn : n ≠ 0
hx : x ∈ J
rw :
  ∀ (hx : Membership.mem (γ := Ideal B) (Ideal.map f I) x),
    Membership.mem (γ := Ideal B) (Ideal.map f I) (dpow hI f n x)
⊢ dpow hI f n x ∈ J

Tactic:
rw [hIJ] at hx ⊢
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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 : B
hn : n ≠ 0
hx : Membership.mem (γ := Ideal B) (Ideal.map f I) x
obtain :
  ∀ (a : A) (ha : a ∈ I)
    (hx : Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) a : B)),
    Membership.mem (γ := Ideal B) (Ideal.map f I) (dpow hI f n ((f : (a : A) → B) a))
⊢ Membership.mem (γ := Ideal B) (Ideal.map f I) (dpow hI f n x)

Tactic:
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp hx

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
hx : Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) a : B)
rw : Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) (hI.dpow n a) : B)
⊢ Membership.mem (γ := Ideal B) (Ideal.map f I) (dpow hI f n ((f : (a : A) → B) a))

Tactic:
rw [dpow_apply' hI hIf ha]

Premises used: DividedPowers.Quotient.OfSurjective.dpow_apply'
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
hx : Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) a : B)
⊢ Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) (hI.dpow n a) : B)

Tactic:
mem_map_of_mem _ (hI.dpow_mem hn ha)

Premises used: DividedPowers.dpow_mem, Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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 : ℕ
hn : n ≠ 0
a : A
ha : a ∈ I
hx : Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) a : B)
⊢ Membership.mem.{u_2, u_2} (α := B) (γ := Ideal B) (Ideal.map f I) ((f : (a : A) → B) (hI.dpow n a) : B)

Tactic:
exact mem_map_of_mem _ (hI.dpow_mem hn ha)

Premises used: DividedPowers.dpow_mem, Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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
hx : x ∈ J
hy : y ∈ J
obtain :
  ∀ (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
⊢ dpow hI f n (x + y) = ∑ k ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n, dpow hI f k.1 x * dpow hI f k.2 y

Tactic:
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
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)
⊢ 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

Tactic:
obtain ⟨b, hb, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hy)

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
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)
⊢ 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:
rw [← map_add, dpow_apply' hI hIf (I.add_mem ha hb), hI.dpow_add ha hb, map_sum,
      Finset.sum_congr rfl]

Premises used: DividedPowers.dpow_add, map_add, Ideal.add_mem, map_sum, DividedPowers.Quotient.OfSurjective.dpow_apply', Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
rw₂ 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)
⊢ (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)

Tactic:
rw [dpow_apply' hI hIf ha, dpow_apply' hI hIf hb, ← _root_.map_mul]

Premises used: DividedPowers.Quotient.OfSurjective.dpow_apply', map_mul
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
⊢ ∀ 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:
exact fun k _ ↦ by rw [dpow_apply' hI hIf ha, dpow_apply' hI hIf hb, ← _root_.map_mul]
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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
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
⊢ dpow hI f n (x * y) = x ^ n * dpow hI f n y

Tactic:
obtain ⟨a, rfl⟩ := hf x

Premises used: rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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
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)
⊢ 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 ⟨b, hb, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hy)

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
rw₅ 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)
⊢ 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:
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]

Premises used: map_pow, DividedPowers.Quotient.OfSurjective.dpow_apply', DividedPowers.dpow_mul, map_mul, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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
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)
⊢ dpow hI f m x * dpow hI f n x = (↑((m + n).choose m) : B) * dpow hI f (m + n) x

Tactic:
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
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)
⊢ 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:
simp only [dpow_apply' hI hIf ha]

Premises used: DividedPowers.Quotient.OfSurjective.dpow_apply'
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
rw₃ 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)
⊢ 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:
rw [← _root_.map_mul, hI.mul_dpow ha, _root_.map_mul, map_natCast]

Premises used: DividedPowers.mul_dpow, map_mul, map_natCast
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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
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)
⊢ dpow hI f m (dpow hI f n x) = (↑(m.uniformBell n) : B) * dpow hI f (m * n) x

Tactic:
obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)

Premises used: Iff.mp, Ideal.mem_map_iff_of_surjective, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
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)
⊢ 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:
simp only [dpow_apply' hI hIf, ha, hI.dpow_mem hn ha]

Premises used: DividedPowers.dpow_mem, DividedPowers.Quotient.OfSurjective.dpow_apply'
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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)
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)
rw₁ :
  HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (↑(m.uniformBell n) : A) : B)
      ((f : (a : A) → B) (hI.dpow (m * n) a) : B) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B)
rw₂ rw₃ :
  HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) a) : B) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B) ((f : (a : A) → B) (hI.dpow (m * n) 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)

Tactic:
rw [hI.dpow_comp hn ha, _root_.map_mul, map_natCast]

Premises used: DividedPowers.dpow_comp, map_mul, map_natCast
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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 : B
⊢ (dividedPowers hI hf hIJ hIf).dpow n x = dpow hI f n x

Tactic:
rfl

Premises used: dite, Function.extend, DividedPowers.Quotient.OfSurjective.dpow, rfl
-- Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal
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
rw : dpow hI f n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
rw₁ rw₂ : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (hI.dpow n a) : B) ((f : (a : A) → B) (hI.dpow n a) : B)
⊢ (dividedPowers hI hf hIJ hIf).dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)

Tactic:
rw [dpow_def, dpow_apply' hI hIf ha]

Premises used: DividedPowers.Quotient.OfSurjective.dpow_def, DividedPowers.Quotient.OfSurjective.dpow_apply'