Theorem: DividedPowers.Quotient.OfSurjective.unique (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers (Ideal.map f I)
hm : hI.isDPMorphism hquot f
n : ℕ
x : B
hx : x ∈ Ideal.map f I
⊢ hquot.dpow n x = (dividedPowers hI hf hIf).dpow n x
Tactic:
obtain ⟨a, ha, rfl⟩ := (Ideal.mem_map_iff_of_surjective f hf).mp hx
State after:
case intro.intro
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers (Ideal.map f I)
hm : hI.isDPMorphism hquot f
n : ℕ
a : A
ha : a ∈ I
hx : f a ∈ Ideal.map f I
⊢ hquot.dpow n (f a) = (dividedPowers hI hf hIf).dpow n (f a)

State before:
case intro.intro
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
hquot : DividedPowers (Ideal.map f I)
hm : hI.isDPMorphism hquot f
n : ℕ
a : A
ha : a ∈ I
hx : f a ∈ Ideal.map f I
⊢ hquot.dpow n (f a) = (dividedPowers hI hf hIf).dpow n (f a)
Tactic:
rw [hm.2 n a ha, dpow_apply hI hf hIf ha]
State after:
no goals