awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
hn : n ≠ 0
h : Membership.mem (γ := Ideal A) ⊥ a
simp : a = 0 → n = 0 → Eq.{u_1 + 1} (α := A) 1 0
⊢ Membership.mem (γ := Ideal A) ⊥ (if a = 0 ∧ n = 0 then 1 else 0)

Tactic:
simp only [mem_bot, ite_eq_right_iff, and_imp]

Premises used: Ideal.mem_bot, and_imp, ite_eq_right_iff
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
hn : n ≠ 0
h : Membership.mem (γ := Ideal A) ⊥ a
⊢ a = 0 → n = 0 → Eq.{u_1 + 1} (α := A) 1 0

Tactic:
fun _ a ↦ False.elim (hn a)

Premises used: False.elim
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
a : A
hn : n ≠ 0
h : Membership.mem (γ := Ideal A) ⊥ a
⊢ a = 0 → n = 0 → Eq.{u_1 + 1} (α := A) 1 0

Tactic:
exact fun _ a ↦ False.elim (hn a)

Premises used: False.elim
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
rw :
  Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ k.1 = 0 then 1 else 0)
        (if Eq.{u_1 + 1} (α := A) 0 0 ∧ k.2 = 0 then 1 else 0))
⊢ Eq.{u_1 + 1} (α := A) (if x + y = 0 ∧ n = 0 then 1 else 0)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (if x = 0 ∧ k.1 = 0 then 1 else 0) (if y = 0 ∧ k.2 = 0 then 1 else 0))

Tactic:
rw [mem_bot.mp ha, mem_bot.mp hb, add_zero]

Premises used: Ideal.mem_bot, Iff.mp, add_zero
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
simp :
  Eq.{u_1 + 1} (α := A) (if n = 0 then 1 else 0)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
⊢ Eq.{u_1 + 1} (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      HMul.hMul (α := A) (if Eq.{u_1 + 1} (α := A) 0 0 ∧ k.1 = 0 then 1 else 0)
        (if Eq.{u_1 + 1} (α := A) 0 0 ∧ k.2 = 0 then 1 else 0))

Tactic:
simp only [true_and, mul_ite, mul_one, mul_zero]

Premises used: mul_ite, MulZeroClass.mul_zero, mul_one, true_and
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
pos :
  ∀ (h : n = 0),
    Eq.{u_1 + 1} (α := A) 1 (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
neg :
  ∀ (h : ¬n = 0),
    Eq.{u_1 + 1} (α := A) 0 (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)
⊢ Eq.{u_1 + 1} (α := A) (if n = 0 then 1 else 0)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
h : n = 0
⊢ Eq.{u_1 + 1} (α := A) 1 (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
h : ¬n = 0
neg : Eq.{u_1 + 1} (α := A) (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) 0
⊢ Eq.{u_1 + 1} (α := A) 0 (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0)

Tactic:
symm
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
h : ¬n = 0
neg : ∀ x ∈ @antidiagonal _ instAddMonoid _ n, Eq.{u_1 + 1} (α := A) (if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) 0
⊢ Eq.{u_1 + 1} (α := A) (∑ x ∈ @antidiagonal _ instAddMonoid _ n, if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) 0

Tactic:
apply sum_eq_zero

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x y : A
ha : Membership.mem (γ := Ideal A) ⊥ x
hb : Membership.mem (γ := Ideal A) ⊥ y
h : ¬n = 0
⊢ ∀ x ∈ @antidiagonal _ instAddMonoid _ n, Eq.{u_1 + 1} (α := A) (if x.2 = 0 then if x.1 = 0 then 1 else 0 else 0) 0

Tactic:
grind [mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
rw : (if x * 0 = 0 ∧ n = 0 then 1 else 0) = x ^ n * if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0
⊢ (if x * x_1 = 0 ∧ n = 0 then 1 else 0) = x ^ n * if x_1 = 0 ∧ n = 0 then 1 else 0

Tactic:
rw [mem_bot.mp hx]

Premises used: Ideal.mem_bot, Iff.mp
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
simp : (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
⊢ (if x * 0 = 0 ∧ n = 0 then 1 else 0) = x ^ n * if Eq.{u_1 + 1} (α := A) 0 0 ∧ n = 0 then 1 else 0

Tactic:
simp only [mul_zero, true_and, mul_ite, mul_one]

Premises used: mul_ite, MulZeroClass.mul_zero, mul_one, true_and
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
pos : ∀ (hn : n = 0), (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
neg : ∀ (hn : ¬n = 0), (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
hn : n = 0
pos : 1 = if n = 0 then x ^ n else 0
pos₁ : 1 = if Eq (α := ℕ) 0 0 then HPow.hPow (β := ℕ) x 0 else 0
pos₂ : 1 = HPow.hPow (β := ℕ) x 0
pos₃ pos₄ : Eq.{u_1 + 1} (α := A) 1 1
⊢ (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0

Tactic:
rw [if_pos hn, hn, if_pos rfl, _root_.pow_zero]

Premises used: if_pos, pow_zero, rfl
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
n : ℕ
x x_1 : A
hx : Membership.mem (γ := Ideal A) ⊥ x_1
hn : ¬n = 0
⊢ (if n = 0 then 1 else 0) = if n = 0 then x ^ n else 0

Tactic:
simp only [if_neg hn]

Premises used: if_neg
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
rw :
  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)
⊢ HMul.hMul (α := A) (if x = 0 ∧ m = 0 then 1 else 0) (if x = 0 ∧ n = 0 then 1 else 0) =
    HMul.hMul (α := A) (↑((m + n).choose m) : A) (if x = 0 ∧ m + n = 0 then 1 else 0)

Tactic:
rw [mem_bot.mp hx]

Premises used: Ideal.mem_bot, Iff.mp
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
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)
⊢ 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)

Tactic:
simp only [true_and, mul_ite, mul_one, mul_zero, add_eq_zero]

Premises used: mul_ite, MulZeroClass.mul_zero, add_eq_zero, mul_one, true_and
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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)
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)
⊢ 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
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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)

Tactic:
simp only [hn, ite_true, and_true, add_zero, choose_self, cast_one]

Premises used: and_true, ite_true, add_zero, Nat.cast_one, Nat.choose_self
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
hn : ¬n = 0
neg : ¬(m = 0 ∧ 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:
rw [if_neg hn, if_neg]

Premises used: if_neg
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
hn : ¬n = 0
⊢ ¬(m = 0 ∧ n = 0)

Tactic:
not_and_of_not_right (m = 0) hn

Premises used: not_and_of_not_right, OfNat.ofNat, Eq
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : Membership.mem (γ := Ideal A) ⊥ x
hn : ¬n = 0
⊢ ¬(m = 0 ∧ n = 0)

Tactic:
exact not_and_of_not_right (m = 0) hn

Premises used: not_and_of_not_right, OfNat.ofNat, Eq
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : Membership.mem (γ := Ideal A) ⊥ a
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)
⊢ (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)

Tactic:
rw [mem_bot.mp ha]

Premises used: Ideal.mem_bot, Iff.mp
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : Membership.mem (γ := Ideal A) ⊥ a
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)
⊢ (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:
simp only [true_and, ite_eq_right_iff, _root_.mul_eq_zero, mul_ite, mul_one, mul_zero]

Premises used: mul_ite, mul_eq_zero, MulZeroClass.mul_zero, ite_eq_right_iff, mul_one, true_and
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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)
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)
⊢ 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
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : Membership.mem (γ := Ideal A) ⊥ a
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:
simp [hm, uniformBell_zero_left, hn]

Premises used: Nat.uniformBell_zero_left
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
I : Ideal A
m n : ℕ
a : A
hn : n ≠ 0
ha : Membership.mem (γ := Ideal A) ⊥ a
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:
simp only [hm, and_false, ite_false, false_or, if_neg hn]

Premises used: ite_false, false_or, and_false, if_neg
-- Module: Mathlib.RingTheory.DividedPowers.Basic
Goal:
A : Type u_1
inst : CommSemiring A
inst_1 : DecidableEq A
n : ℕ
a : A
⊢ DividedPowers.dpow (dividedPowersBot A) n a = if a = 0 ∧ n = 0 then 1 else 0

Tactic:
simp [dividedPowersBot]

Premises used: dividedPowersBot
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
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'
⊢ hI = hI'

Tactic:
obtain ⟨hI, h₀, _⟩ := hI
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
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 }
⊢ { 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'
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
simp : hI = hI'
⊢ { 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:
simp only [mk.injEq]

Premises used: DividedPowers.mk.injEq
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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
⊢ hI = hI'

Tactic:
grind
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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')
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
⊢ hI = hI'

Tactic:
ext n x
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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')
n : ℕ
x : A
h_1 : x ∈ I
⊢ hI.dpow n x = hI'.dpow n x

Tactic:
congr_fun (congr_fun h n) x

Premises used: congr_fun
-- Module: Mathlib.RingTheory.DividedPowers.Basic
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')
n : ℕ
x : A
h_1 : x ∈ I
⊢ hI.dpow n x = hI'.dpow n x

Tactic:
exact congr_fun (congr_fun h n) x

Premises used: congr_fun