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

State before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
⊢ hI.isSubDPIdeal (RingHom.ker f ⊓ I)
Tactic:
rw [isSubDPIdeal_inf_iff]
State after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
⊢ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f

State before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : hI.isDPMorphism hJ f
⊢ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Tactic:
simp only [isDPMorphism] at hf
State after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
⊢ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f

State before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
⊢ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Tactic:
intro n a b ha hb
State after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f

State before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
Tactic:
simp only [RingHom.sub_mem_ker_iff]
State after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → f (hI.dpow n a) = f (hI.dpow n b)

State before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → f (hI.dpow n a) = f (hI.dpow n b)
Tactic:
rw [← hf.2 n a ha, ← hf.2 n b hb]
State after:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → hJ.dpow n (f a) = hJ.dpow n (f b)

State before:
A : Type u_2
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_1
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : A →+* B
hf : Ideal.map f I ≤ J ∧ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
⊢ f a = f b → hJ.dpow n (f a) = hJ.dpow n (f b)
Tactic:
exact congr_arg _
State after:
no goals