awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (hypothesis)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ r a ^ n * HPow.hPow (α := A) (↑n ! : A) (#s - 1) = HPow.hPow (α := A) (↑n ! : A) #s * hI.dpow n (r a)
have this : #s = #s - 1 + 1
Tactic: have : #s = #s - 1 + 1 := by grind
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
this : #s = #s - 1 + 1
⊢ r a ^ n * HPow.hPow (α := A) (↑n ! : A) (#s - 1) = HPow.hPow (α := A) (↑n ! : A) #s * hI.dpow n (r a)
have nth_rewrite : r a ^ n * HPow.hPow (α := A) (↑n ! : A) (#s - 1) = HPow.hPow (α := A) (↑n ! : A) (#s - 1 + 1) * hI.dpow n (r a)
Tactic: nth_rewrite 2 [this]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
h : s.Nonempty
⊢ ∏ x ∈ s, r x ∈ I
have pos : ∀ (j : ι) (hj : j ∈ s), ∏ x ∈ s, r x ∈ I
Tactic: obtain ⟨j, hj⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
n : ℕ
a : ι
s : Finset ι
has : a ∉ s
hrec :
  ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
    hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
hs : (insert a s).Nonempty
hs' : ∀ i ∈ insert a s, r i ∈ I
j : ι
hj : j ∈ s
⊢ ∏ x ∈ s, r x ∈ I
have pos : (∏ x ∈ s \ {j}, r x) * r j ∈ I
Tactic: rw [Finset.prod_eq_prod_diff_singleton_mul hj]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
s : Finset ι
hs : s.Nonempty
hs' : ∀ i ∈ s, r i ∈ I
n : ℕ
⊢ hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
have empty : ∀ (hs : Finset.Nonempty.{u_3} (α := ι) ∅) (hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → r i ∈ I),
  hI.dpow n (∏ i ∈ ∅, r i) = HSMul.hSMul (β := A) (n ! ^ (card.{u_3} (α := ι) ∅ - 1)) (∏ i ∈ ∅, hI.dpow n (r i))
Tactic: induction s using Finset.induction with
  | empty => simp_all
  | @insert a s has hrec =>
    rw [Finset.prod_insert has]
    by_cases h : s.Nonempty
    · rw [dpow_mul]
      · simp only [Finset.card_insert_of_notMem has, add_tsub_cancel_right, nsmul_eq_mul,
          Nat.cast_pow, Finset.prod_insert has,
          hrec h (fun i hi ↦ hs' i (mem_insert_of_mem hi)), ← mul_assoc]
        apply congr_arg₂ _ _ rfl
        have : #s = #s - 1 + 1 := by grind
        nth_rewrite 2 [this]
        rw [mul_comm, pow_succ, mul_assoc, hI.factorial_mul_dpow_eq_pow]
        exact hs' a (mem_insert_self a s)
      · obtain ⟨j, hj⟩ := h
        rw [Finset.prod_eq_prod_diff_singleton_mul hj]
        exact I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))
    · simp [not_nonempty_iff_eq_empty.mp h]
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
s : Finset ι
hs : s.Nonempty
hs' : ∀ i ∈ s, r i ∈ I
n : ℕ
empty :
  ∀ (hs : Finset.Nonempty.{u_3} (α := ι) ∅) (hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → r i ∈ I),
    hI.dpow n (∏ i ∈ ∅, r i) = HSMul.hSMul (β := A) (n ! ^ (card.{u_3} (α := ι) ∅ - 1)) (∏ i ∈ ∅, hI.dpow n (r i))
⊢ hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hrec :
    ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
      hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i)))
  (hs : (insert a s).Nonempty) (hs' : ∀ i ∈ insert a s, r i ∈ I),
  hI.dpow n (∏ i ∈ insert a s, r i) =
    HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
Tactic: induction s using Finset.induction with
  | empty => simp_all
  | @insert a s has hrec =>
    rw [Finset.prod_insert has]
    by_cases h : s.Nonempty
    · rw [dpow_mul]
      · simp only [Finset.card_insert_of_notMem has, add_tsub_cancel_right, nsmul_eq_mul,
          Nat.cast_pow, Finset.prod_insert has,
          hrec h (fun i hi ↦ hs' i (mem_insert_of_mem hi)), ← mul_assoc]
        apply congr_arg₂ _ _ rfl
        have : #s = #s - 1 + 1 := by grind
        nth_rewrite 2 [this]
        rw [mul_comm, pow_succ, mul_assoc, hI.factorial_mul_dpow_eq_pow]
        exact hs' a (mem_insert_self a s)
      · obtain ⟨j, hj⟩ := h
        rw [Finset.prod_eq_prod_diff_singleton_mul hj]
        exact I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))
    · simp [not_nonempty_iff_eq_empty.mp h]
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
s : Finset ι
hs : s.Nonempty
hs' : ∀ i ∈ s, r i ∈ I
n : ℕ
⊢ hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
have empty : ∀ (hs : Finset.Nonempty.{u_3} (α := ι) ∅) (hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → r i ∈ I),
  hI.dpow n (∏ i ∈ ∅, r i) = HSMul.hSMul (β := A) (n ! ^ (card.{u_3} (α := ι) ∅ - 1)) (∏ i ∈ ∅, hI.dpow n (r i))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp_all
  | @insert a s has hrec =>
    rw [Finset.prod_insert has]
    by_cases h : s.Nonempty
    · rw [dpow_mul]
      · simp only [Finset.card_insert_of_notMem has, add_tsub_cancel_right, nsmul_eq_mul,
          Nat.cast_pow, Finset.prod_insert has,
          hrec h (fun i hi ↦ hs' i (mem_insert_of_mem hi)), ← mul_assoc]
        apply congr_arg₂ _ _ rfl
        have : #s = #s - 1 + 1 := by grind
        nth_rewrite 2 [this]
        rw [mul_comm, pow_succ, mul_assoc, hI.factorial_mul_dpow_eq_pow]
        exact hs' a (mem_insert_self a s)
      · obtain ⟨j, hj⟩ := h
        rw [Finset.prod_eq_prod_diff_singleton_mul hj]
        exact I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))
    · simp [not_nonempty_iff_eq_empty.mp h]
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
hI : DividedPowers I
ι : Type u_3
r : ι → A
s : Finset ι
hs : s.Nonempty
hs' : ∀ i ∈ s, r i ∈ I
n : ℕ
empty :
  ∀ (hs : Finset.Nonempty.{u_3} (α := ι) ∅) (hs' : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → r i ∈ I),
    hI.dpow n (∏ i ∈ ∅, r i) = HSMul.hSMul (β := A) (n ! ^ (card.{u_3} (α := ι) ∅ - 1)) (∏ i ∈ ∅, hI.dpow n (r i))
⊢ hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i))
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hrec :
    ∀ (hs : s.Nonempty) (hs' : ∀ i ∈ s, r i ∈ I),
      hI.dpow n (∏ i ∈ s, r i) = HSMul.hSMul (β := A) (n ! ^ (#s - 1)) (∏ i ∈ s, hI.dpow n (r i)))
  (hs : (insert a s).Nonempty) (hs' : ∀ i ∈ insert a s, r i ∈ I),
  hI.dpow n (∏ i ∈ insert a s, r i) =
    HSMul.hSMul (β := A) (n ! ^ (#(insert a s) - 1)) (∏ i ∈ insert a s, hI.dpow n (r i))
Tactic: classical
  induction s using Finset.induction with
  | empty => simp_all
  | @insert a s has hrec =>
    rw [Finset.prod_insert has]
    by_cases h : s.Nonempty
    · rw [dpow_mul]
      · simp only [Finset.card_insert_of_notMem has, add_tsub_cancel_right, nsmul_eq_mul,
          Nat.cast_pow, Finset.prod_insert has,
          hrec h (fun i hi ↦ hs' i (mem_insert_of_mem hi)), ← mul_assoc]
        apply congr_arg₂ _ _ rfl
        have : #s = #s - 1 + 1 := by grind
        nth_rewrite 2 [this]
        rw [mul_comm, pow_succ, mul_assoc, hI.factorial_mul_dpow_eq_pow]
        exact hs' a (mem_insert_self a s)
      · obtain ⟨j, hj⟩ := h
        rw [Finset.prod_eq_prod_diff_singleton_mul hj]
        exact I.mul_mem_left _ (hs' j (mem_insert_of_mem hj))
    · simp [not_nonempty_iff_eq_empty.mp h]
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hx : x ∉ J
⊢ Eq.{u_2 + 1} (α := B) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B) (0 : B)
have rw : ((e.symm : (a : B) → A) x : A) ∉ I
Tactic: rw [EmbeddingLike.map_eq_zero_iff, hI.dpow_null]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hx : x ∉ J
⊢ ((e.symm : (a : B) → A) x : A) ∉ I
have rwa : x ∉ Ideal.map e I
Tactic: rwa [symm_apply_mem_of_equiv_iff, h]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x : B
hx : x ∈ J
⊢ Eq.{u_2 + 1} (α := B) ((e : (a : A) → B) (hI.dpow 0 ((e.symm : (a : B) → A) x)) : B) (1 : B)
have rw : Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
Tactic: rw [EmbeddingLike.map_eq_one_iff, hI.dpow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x : B
hx : x ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
have rwa : Membership.mem (γ := Ideal B) (Ideal.map e I) x
Tactic: rwa [symm_apply_mem_of_equiv_iff, h]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x : B
hx : x ∈ J
⊢ (e : (a : A) → B) (hI.dpow 1 ((e.symm : (a : B) → A) x)) = x
have x : Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
Tactic: rw [dpow_one, RingEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
x : B
hx : x ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
have x : Membership.mem (γ := Ideal B) (Ideal.map e I) x
Tactic: rwa [I.symm_apply_mem_of_equiv_iff, h]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ Membership.mem (α := B) J ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
have rw : hI.dpow n ((e.symm : (a : B) → A) x) ∈ I
Tactic: rw [← h, I.apply_mem_of_equiv_iff]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ hI.dpow n ((e.symm : (a : B) → A) x) ∈ I
have apply : Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
Tactic: apply hI.dpow_mem hn
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
have rwa : Membership.mem (γ := Ideal B) (Ideal.map e I) x
Tactic: rwa [I.symm_apply_mem_of_equiv_iff, h]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x y : B
hx : x ∈ J
hy : y ∈ J
⊢ Eq.{u_2 + 1} (α := B) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) (x + y))) : B)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow k.1 ((e.symm : (a : B) → A) x)) : B)
          ((e : (a : A) → B) (hI.dpow k.2 ((e.symm : (a : B) → A) y)) : B) :
      B)
have simp : Eq.{u_2 + 1} (α := B)
  ((e : (a : A) → B)
      (hI.dpow n (HAdd.hAdd (α := A) (β := A) ((e.symm : (a : B) → A) x : A) ((e.symm : (a : B) → A) y : A))) :
    B)
  (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow k.1 ((e.symm : (a : B) → A) x)) : B)
        ((e : (a : A) → B) (hI.dpow k.2 ((e.symm : (a : B) → A) y)) : B) :
    B)
Tactic: simp only [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
x y : B
hx : x ∈ J
hy : y ∈ J
⊢ Eq.{u_2 + 1} (α := B)
    ((e : (a : A) → B)
        (hI.dpow n (HAdd.hAdd (α := A) (β := A) ((e.symm : (a : B) → A) x : A) ((e.symm : (a : B) → A) y : A))) :
      B)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow k.1 ((e.symm : (a : B) → A) x)) : B)
          ((e : (a : A) → B) (hI.dpow k.2 ((e.symm : (a : B) → A) y)) : B) :
      B)
have rw : Eq.{u_2 + 1} (α := B)
  ((e : (a : A) → B)
      (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
        hI.dpow k.1 ((e.symm : (a : B) → A) x) * hI.dpow k.2 ((e.symm : (a : B) → A) y)) :
    B)
  (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow k.1 ((e.symm : (a : B) → A) x)) : B)
        ((e : (a : A) → B) (hI.dpow k.2 ((e.symm : (a : B) → A) y)) : B) :
    B)
Tactic: rw [hI.dpow_add (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))
        (symm_apply_mem_of_equiv_iff.mpr (h ▸ hy))]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a x : B
hx : x ∈ J
⊢ (e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) (a * x))) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
have simp : (e : (a : A) → B)
    (hI.dpow n (HMul.hMul (α := A) (β := A) ((e.symm : (a : B) → A) a : A) ((e.symm : (a : B) → A) x : A))) =
  HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
Tactic: simp only [map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a x : B
hx : x ∈ J
⊢ (e : (a : A) → B)
      (hI.dpow n (HMul.hMul (α := A) (β := A) ((e.symm : (a : B) → A) a : A) ((e.symm : (a : B) → A) x : A))) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
have rw : (e : (a : A) → B) (HPow.hPow (α := A) ((e.symm : (a : B) → A) a : A) n * hI.dpow n ((e.symm : (a : B) → A) x)) =
  HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
Tactic: rw [hI.dpow_mul (symm_apply_mem_of_equiv_iff.mpr (h ▸ hx))]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
n : ℕ
a x : B
hx : x ∈ J
⊢ (e : (a : A) → B) (HPow.hPow (α := A) ((e.symm : (a : B) → A) a : A) n * hI.dpow n ((e.symm : (a : B) → A) x)) =
    HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
have rw : HMul.hMul (β := B) (HPow.hPow (α := B) ((e : (a : A) → B) ((e.symm : (a : B) → A) a : A) : B) n)
    ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B) =
  HMul.hMul (β := B) (a ^ n) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B)
Tactic: rw [map_mul, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hx : x ∈ J
⊢ HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow m ((e.symm : (a : B) → A) x)) : B)
      ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B)
have rw : HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (↑((m + n).choose m) : A) : B)
    ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B) =
  HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B)
    ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B)
Tactic: rw [← map_mul, hI.mul_dpow, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hx : x ∈ J
rw :
  HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (↑((m + n).choose m) : A) : B)
      ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B)
⊢ HMul.hMul (α := B) (β := B) ((e : (a : A) → B) (hI.dpow m ((e.symm : (a : B) → A) x)) : B)
      ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B) =
    HMul.hMul (α := B) (β := B) ((↑((m + n).choose m) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m + n) ((e.symm : (a : B) → A) x)) : B)
have rw₁ : Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
Tactic: rw [← map_mul, hI.mul_dpow, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hx : x ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
have rwa : Membership.mem (γ := Ideal B) (Ideal.map e I) x
Tactic: rwa [symm_apply_mem_of_equiv_iff, h]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ (e : (a : A) → B)
      (hI.dpow m ((e.symm : (a : B) → A) ((e : (a : A) → B) (hI.dpow n ((e.symm : (a : B) → A) x)) : B))) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)
have simp : (e : (a : A) → B) (hI.dpow m (hI.dpow n ((e.symm : (a : B) → A) x))) =
  HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
    ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)
Tactic: simp only [RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ (e : (a : A) → B) (hI.dpow m (hI.dpow n ((e.symm : (a : B) → A) x))) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)
have rw : (e : (a : A) → B) ((↑(m.uniformBell n) : A) * hI.dpow (m * n) ((e.symm : (a : B) → A) x)) =
  HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
    ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)
Tactic: rw [hI.dpow_comp hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
rw :
  (e : (a : A) → B) ((↑(m.uniformBell n) : A) * hI.dpow (m * n) ((e.symm : (a : B) → A) x)) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)
⊢ (e : (a : A) → B) (hI.dpow m (hI.dpow n ((e.symm : (a : B) → A) x))) =
    HMul.hMul (α := B) (β := B) ((↑(m.uniformBell n) : B) : B)
      ((e : (a : A) → B) (hI.dpow (m * n) ((e.symm : (a : B) → A) x)) : B)
have rw₁ : Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
Tactic: rw [hI.dpow_comp hn]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
m n : ℕ
x : B
hn : n ≠ 0
hx : x ∈ J
⊢ Membership.mem (α := A) I ((e.symm : (a : B) → A) x : A)
have rwa : Membership.mem (γ := Ideal B) (Ideal.map e I) x
Tactic: rwa [symm_apply_mem_of_equiv_iff, h]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
⊢ Ideal.map e.symm J = I
have rw : Ideal.map (R := B) e.symm (Ideal.map e I) = I
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hI : DividedPowers I
⊢ ofRingEquiv (e := e.symm) ⋯ (ofRingEquiv h hI) = hI
have h_eq : ∀ (n : ℕ) {a : A}, a ∈ I → dpow (I := I) (ofRingEquiv (e := e.symm) sorry (ofRingEquiv h hI)) n a = hI.dpow n a
Tactic: ext n a
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
I : Ideal A
inst_1 : CommSemiring B
J : Ideal B
e : A ≃+* B
h : Ideal.map e I = J
hJ : DividedPowers J
⊢ ofRingEquiv h (ofRingEquiv (e := e.symm) ⋯ hJ) = hJ
have h_eq : ∀ (n : ℕ) {b : B}, b ∈ J → (ofRingEquiv h (ofRingEquiv (e := e.symm) sorry hJ)).dpow n b = hJ.dpow n b
Tactic: ext n b
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowers.DPMorphism (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommSemiring A
inst_1 : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
⊢ hI.IsDPMorphism hJ f ↔
    map f I ≤ J ∧ ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)
have rw : map f I ≤ J →
  ((∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a)) ↔
    ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n ((f : (a : A) → B) a) = (f : (a : A) → B) (hI.dpow n a))
Tactic: rw [isDPMorphism_def, and_congr_right_iff]