Theorem: DividedPowers.RatAlgebra.dividedPowers_unique (DividedPowers/RatAlgebra.lean)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
⊢ hI = dividedPowers I
Tactic:
apply eq_of_eq_on_ideal
State after:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
⊢ ∀ (n : ℕ) {x : R}, x ∈ I → hI.dpow n x = (dividedPowers I).dpow n x

State before:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
⊢ ∀ (n : ℕ) {x : R}, x ∈ I → hI.dpow n x = (dividedPowers I).dpow n x
Tactic:
intro n x hx
State after:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (dividedPowers I).dpow n x

State before:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
⊢ hI.dpow n x = (dividedPowers I).dpow n x
Tactic:
have hn : IsUnit (n.factorial : R) := Factorial.isUnit n
State after:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
hn : IsUnit ↑n !
⊢ hI.dpow n x = (dividedPowers I).dpow n x

State before:
case h_eq
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Algebra ℚ R
hI : DividedPowers I
n : ℕ
x : R
hx : x ∈ I
hn : IsUnit ↑n !
⊢ hI.dpow n x = (dividedPowers I).dpow n x
Tactic:
rw [dividedPowers_dpow_apply, dpow_eq_of_mem n hx, eq_comm, Ring.inverse_mul_eq_iff_eq_mul _ _ _ hn,
  factorial_mul_dpow_eq_pow _ _ _ hx]
State after:
no goals