-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem DividedPowers.ext (hI : DividedPowers I) (hI' : DividedPowers I)
    (h_eq : ∀ (n : ℕ) {x : A} (_ : x ∈ I), hI.dpow n x = hI'.dpow n x) :
    hI = hI'

Proof state:
case mk.mk
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 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) * hI (m + n) x
dpow_comp✝¹ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI m (hI n x) = ↑(m.uniformBell n) * hI (m * n) x
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 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) * hI' (m + n) x
dpow_comp✝ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI' m (hI' n x) = ↑(m.uniformBell n) * 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✝¹ }.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✝ }.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✝¹ } =
    { 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✝ }

Tactic:
simp only [mk.injEq]

Result:
case mk.mk
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 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) * hI (m + n) x
dpow_comp✝¹ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI m (hI n x) = ↑(m.uniformBell n) * hI (m * n) x
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 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) * hI' (m + n) x
dpow_comp✝ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI' m (hI' n x) = ↑(m.uniformBell n) * 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✝¹ }.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✝ }.dpow
          n x
⊢ hI = hI'

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
h_eq : ∀ (n : ℕ) {x : A}, x ∈ I → hI.dpow n x = hI'.dpow n x
⊢ hI = hI'

Tactic:
obtain ⟨hI, h₀, _⟩ := hI

Result:
case mk
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 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) * hI (m + n) x
dpow_comp✝ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI m (hI n x) = ↑(m.uniformBell n) * 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✝ }.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✝ } =
    hI'

Proof state:
case neg
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 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) * hI (m + n) x
dpow_comp✝¹ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI m (hI n x) = ↑(m.uniformBell n) * hI (m * n) x
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 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) * hI' (m + n) x
dpow_comp✝ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI' m (hI' n x) = ↑(m.uniformBell n) * 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✝¹ }.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✝ }.dpow
          n x
n : ℕ
x : A
hx : x ∉ I
⊢ hI n x = hI' n x

Tactic:
rw [h₀ hx, h₀' hx]

Result:
no goals