Theorem: DividedPowers.eq_of_eq_on_ideal (DividedPowers/Basic.lean)

State before:
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:
ext n x
State after:
case dpow.h.h
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
n : ℕ
x : A
⊢ hI.dpow n x = hI'.dpow n x

State before:
case dpow.h.h
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
n : ℕ
x : A
⊢ hI.dpow n x = hI'.dpow n x
Tactic:
by_cases hx : x ∈ I
State after:
case pos
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
n : ℕ
x : A
hx : x ∈ I
⊢ hI.dpow n x = hI'.dpow n x

case neg
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
n : ℕ
x : A
hx : x ∉ I
⊢ hI.dpow n x = hI'.dpow n x

State before:
case pos
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
n : ℕ
x : A
hx : x ∈ I
⊢ hI.dpow n x = hI'.dpow n x
Tactic:
exact h_eq n hx
State after:
no goals

State before:
case neg
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
n : ℕ
x : A
hx : x ∉ I
⊢ hI.dpow n x = hI'.dpow n x
Tactic:
rw [hI.dpow_null hx, hI'.dpow_null hx]
State after:
no goals