Theorem: DividedPowerAlgebra.lift_augIdeal_le (DividedPowers/DPAlgebra/Graded/GradeZero.lean)

State before:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ Ideal.map (lift hI φ hφ) (augIdeal R M) ≤ I
Tactic:
simp only [augIdeal_eq_span, Ideal.map_span, Ideal.span_le, SetLike.mem_coe]
State after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ ⇑(lift hI φ hφ) '' Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑I

State before:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
⊢ ⇑(lift hI φ hφ) '' Set.image2 (dp R) {n | 0 < n} Set.univ ⊆ ↑I
Tactic:
rintro y ⟨x, ⟨n, hn, m, _, rfl⟩, rfl⟩
State after:
case intro.intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
hn : n ∈ {n | 0 < n}
m : M
left✝ : m ∈ Set.univ
⊢ (lift hI φ hφ) (dp R n m) ∈ ↑I

State before:
case intro.intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
hn : n ∈ {n | 0 < n}
m : M
left✝ : m ∈ Set.univ
⊢ (lift hI φ hφ) (dp R n m) ∈ ↑I
Tactic:
simp only [liftAlgHom_apply_dp]
State after:
case intro.intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
hn : n ∈ {n | 0 < n}
m : M
left✝ : m ∈ Set.univ
⊢ hI.dpow n (φ m) ∈ ↑I

State before:
case intro.intro.intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : DecidableEq R
inst✝² : DecidableEq M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
hn : n ∈ {n | 0 < n}
m : M
left✝ : m ∈ Set.univ
⊢ hI.dpow n (φ m) ∈ ↑I
Tactic:
refine hI.dpow_mem (ne_of_gt hn) (hφ m)
State after:
no goals