Theorem: DividedPowerAlgebra.on_dp_algebra_unique (DividedPowers/DPAlgebra/Dpow.lean)

State before:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
⊢ h = h'
Tactic:
apply DividedPowers.dp_uniqueness_self h' h (augIdeal_eq_span R M)
State after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
⊢ ∀ (n : ℕ), ∀ a ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, h'.dpow n a = h.dpow n a

State before:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
⊢ ∀ (n : ℕ), ∀ a ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, h'.dpow n a = h.dpow n a
Tactic:
rintro n f ⟨q, hq : 0 < q, m, _, rfl⟩
State after:
case intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n✝ : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ h'.dpow n (dp R q m) = h.dpow n (dp R q m)

State before:
case intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n✝ : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ h'.dpow n (dp R q m) = h.dpow n (dp R q m)
Tactic:
nth_rw 1 [← h1' q m]
State after:
case intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n✝ : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ h'.dpow n (h'.dpow q ((ι R M) m)) = h.dpow n (dp R q m)

State before:
case intro.intro.intro.intro
R : Type u
inst✝⁴ : CommRing R
inst✝³ : DecidableEq R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : DecidableEq M
inst✝ : Module R M
x : M
n✝ : ℕ
h h' : DividedPowers (augIdeal R M)
h1 : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
h1' : ∀ (n : ℕ) (x : M), h'.dpow n ((ι R M) x) = dp R n x
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ h'.dpow n (h'.dpow q ((ι R M) m)) = h.dpow n (dp R q m)
Tactic:
rw [← h1 q m, h.dpow_comp n (ne_of_gt hq) (ι_mem_augIdeal R M m),
  h'.dpow_comp n (ne_of_gt hq) (ι_mem_augIdeal R M m), h1 _ m, h1' _ m]
State after:
no goals