Theorem: DividedPowers.isSubDPIdeal_map (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ hJ.isSubDPIdeal (Ideal.map f K)
Tactic:
simp only [Ideal.map]
State after:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ hJ.isSubDPIdeal (Ideal.span (⇑f '' ↑K))

State before:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ hJ.isSubDPIdeal (Ideal.span (⇑f '' ↑K))
Tactic:
rw [span_isSubDPIdeal_iff]
State after:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ ⇑f '' ↑K, hJ.dpow n s ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J

State before:
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ∀ (n : ℕ), n ≠ 0 → ∀ s ∈ ⇑f '' ↑K, hJ.dpow n s ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
rintro n hn y ⟨x, hx, rfl⟩
State after:
case intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ hJ.dpow n (f x) ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J

State before:
case intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ hJ.dpow n (f x) ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
rw [hf.2 n x (hK.1 hx)]
State after:
case intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ f (hI.dpow n x) ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J

State before:
case intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ f (hI.dpow n x) ∈ Ideal.span (⇑f '' ↑K)

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
apply Ideal.mem_map_of_mem
State after:
case intro.intro.h
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ hI.dpow n x ∈ K

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J

State before:
case intro.intro.h
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ ↑K
⊢ hI.dpow n x ∈ K

case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
exact hK.2 n hn x hx
State after:
case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J

State before:
case hS
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
⊢ ⇑f '' ↑K ⊆ ↑J
Tactic:
rintro y ⟨x, hx, rfl⟩
State after:
case hS.intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
x : A
hx : x ∈ ↑K
⊢ f x ∈ ↑J

State before:
case hS.intro.intro
A : Type u_2
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommSemiring B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
K : Ideal A
hK : hI.isSubDPIdeal K
x : A
hx : x ∈ ↑K
⊢ f x ∈ ↑J
Tactic:
exact hf.1 (Ideal.mem_map_of_mem f (hK.1 hx))
State after:
no goals