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

State before:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ h.isDPMorphism hJ ↑(lift hJ f hf)
Tactic:
constructor
State after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ Ideal.map (↑(lift hJ f hf)) (augIdeal R M) ≤ J

case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ ∀ (n : ℕ), ∀ a ∈ augIdeal R M, hJ.dpow n (↑(lift hJ f hf) a) = ↑(lift hJ f hf) (h.dpow n a)

State before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ Ideal.map (↑(lift hJ f hf)) (augIdeal R M) ≤ J
Tactic:
rw [augIdeal_eq_span]
State after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ Ideal.map (↑(lift hJ f hf)) (span (Set.image2 (dp R) {n | 0 < n} Set.univ)) ≤ J

State before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ Ideal.map (↑(lift hJ f hf)) (span (Set.image2 (dp R) {n | 0 < n} Set.univ)) ≤ J
Tactic:
rw [Ideal.map_span]
State after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ span (⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ) ≤ J

State before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ span (⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ) ≤ J
Tactic:
rw [Ideal.span_le]
State after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ ⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑J

State before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ ⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑J
Tactic:
intro s
State after:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
s : S
⊢ s ∈ ⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ → s ∈ ↑J

State before:
case left
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
s : S
⊢ s ∈ ⇑↑(lift hJ f hf) '' Set.image2 (dp R) {n | 0 < n} Set.univ → s ∈ ↑J
Tactic:
rintro ⟨a, ⟨n, hn : 0 < n, m, _, rfl⟩, rfl⟩
State after:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (dp R n m) ∈ ↑J

State before:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (dp R n m) ∈ ↑J
Tactic:
simp only [AlgHom.coe_toRingHom, SetLike.mem_coe]
State after:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (dp R n m) ∈ J

State before:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (dp R n m) ∈ J
Tactic:
rw [liftAlgHom_apply_dp]
State after:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ hJ.dpow n (f m) ∈ J

State before:
case left.intro.intro.intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
hn : 0 < n
m : M
left✝ : m ∈ Set.univ
⊢ hJ.dpow n (f m) ∈ J
Tactic:
apply hJ.dpow_mem (ne_of_gt hn) (hf m)
State after:
no goals

State before:
case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
⊢ ∀ (n : ℕ), ∀ a ∈ augIdeal R M, hJ.dpow n (↑(lift hJ f hf) a) = ↑(lift hJ f hf) (h.dpow n a)
Tactic:
intro n a ha
State after:
case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ hJ.dpow n (↑(lift hJ f hf) a) = ↑(lift hJ f hf) (h.dpow n a)

State before:
case right
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ hJ.dpow n (↑(lift hJ f hf) a) = ↑(lift hJ f hf) (h.dpow n a)
Tactic:
apply symm
State after:
case right.a
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ↑(lift hJ f hf) (h.dpow n a) = hJ.dpow n (↑(lift hJ f hf) a)

State before:
case right.a
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ↑(lift hJ f hf) (h.dpow n a) = hJ.dpow n (↑(lift hJ f hf) a)
Tactic:
rw [(dp_uniqueness h hJ (lift hJ f hf) (augIdeal_eq_span R M) _ _) n a ha]
State after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ∀ s ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, ↑(lift hJ f hf) s ∈ J

R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ∀ (n : ℕ), ∀ a ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, ↑(lift hJ f hf) (h.dpow n a) = hJ.dpow n (↑(lift hJ f hf) a)

State before:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ∀ s ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, ↑(lift hJ f hf) s ∈ J
Tactic:
rintro a ⟨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✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (dp R q m) ∈ J

State before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (dp R q m) ∈ J
Tactic:
simp only [AlgHom.coe_toRingHom, liftAlgHom_apply_dp]
State after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ hJ.dpow q (f m) ∈ J

State before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ hJ.dpow q (f m) ∈ J
Tactic:
exact hJ.dpow_mem (ne_of_gt hq) (hf m)
State after:
no goals

State before:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
⊢ ∀ (n : ℕ), ∀ a ∈ Set.image2 (dp R) {n | 0 < n} Set.univ, ↑(lift hJ f hf) (h.dpow n a) = hJ.dpow n (↑(lift hJ f hf) a)
Tactic:
rintro n a ⟨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✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (h.dpow n (dp R q m)) = hJ.dpow n (↑(lift hJ f hf) (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✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(lift hJ f hf) (h.dpow n (dp R q m)) = hJ.dpow n (↑(lift hJ f hf) (dp R q m))
Tactic:
simp only [AlgHom.coe_toRingHom, liftAlgHom_apply_dp]
State after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (h.dpow n (dp R q m)) = hJ.dpow n (hJ.dpow q (f m))

State before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (h.dpow n (dp R q m)) = hJ.dpow n (hJ.dpow q (f m))
Tactic:
rw [hJ.dpow_comp n (ne_of_gt hq) (hf m),← hh q m,
  h.dpow_comp n (ne_of_gt hq) (ι_mem_augIdeal R M m), _root_.map_mul, map_natCast]
State after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(mchoose n q) * (lift hJ f hf) (h.dpow (n * q) ((ι R M) m)) = ↑(mchoose n q) * hJ.dpow (n * q) (f m)

State before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ ↑(mchoose n q) * (lift hJ f hf) (h.dpow (n * q) ((ι R M) m)) = ↑(mchoose n q) * hJ.dpow (n * q) (f m)
Tactic:
apply congr_arg₂ _ rfl
State after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (h.dpow (n * q) ((ι R M) m)) = hJ.dpow (n * q) (f m)

State before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (h.dpow (n * q) ((ι R M) m)) = hJ.dpow (n * q) (f m)
Tactic:
rw [hh]
State after:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (dp R (n * q) m) = hJ.dpow (n * q) (f m)

State before:
case intro.intro.intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : DecidableEq R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
h : DividedPowers (augIdeal R M)
hh : ∀ (n : ℕ) (x : M), h.dpow n ((ι R M) x) = dp R n x
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
J : Ideal S
hJ : DividedPowers J
f : M →ₗ[R] S
hf : ∀ (m : M), f m ∈ J
n✝ : ℕ
a : DividedPowerAlgebra R M
ha : a ∈ augIdeal R M
n q : ℕ
hq : 0 < q
m : M
left✝ : m ∈ Set.univ
⊢ (lift hJ f hf) (dp R (n * q) m) = hJ.dpow (n * q) (f m)
Tactic:
rw [liftAlgHom_apply_dp]
State after:
no goals