-- 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.h.h
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
⊢ hI n x = hI' n x

Tactic:
by_cases hx : x ∈ I

Result:
case pos
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

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

Proof state:
case pos
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:
exact h_eq n hx

Result:
no goals