Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply' (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ dpow hI f n (f a) = f (hI.dpow n a)
Tactic:
classical
simp only [dpow, Function.extend_def]
have h : ∃ (a_1 : I), f ↑a_1 = f a := by use ⟨a, ha⟩
rw [dif_pos h]
rw [← sub_eq_zero, ← map_sub, ← RingHom.mem_ker]
rw [isSubDPIdeal_inf_iff] at hIf
apply hIf n _ a _ ha
rw [RingHom.mem_ker, map_sub, sub_eq_zero]
rw [h.choose_spec]
simp only [Submodule.coe_mem]
State after:
no goals

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ dpow hI f n (f a) = f (hI.dpow n a)
Tactic:
simp only [dpow, Function.extend_def]
State after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ (if h : ∃ a_1, f ↑a_1 = f a then f (hI.dpow n ↑(Classical.choose ⋯)) else OfNat.ofNat 0 (f a)) = f (hI.dpow n a)

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ (if h : ∃ a_1, f ↑a_1 = f a then f (hI.dpow n ↑(Classical.choose ⋯)) else OfNat.ofNat 0 (f a)) = f (hI.dpow n a)
Tactic:
have h : ∃ (a_1 : I), f ↑a_1 = f a := by use ⟨a, ha⟩
State after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ (if h : ∃ a_1, f ↑a_1 = f a then f (hI.dpow n ↑(Classical.choose ⋯)) else OfNat.ofNat 0 (f a)) = f (hI.dpow n a)

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ (if h : ∃ a_1, f ↑a_1 = f a then f (hI.dpow n ↑(Classical.choose ⋯)) else OfNat.ofNat 0 (f a)) = f (hI.dpow n a)
Tactic:
rw [dif_pos h]
State after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ f (hI.dpow n ↑(Classical.choose ⋯)) = f (hI.dpow n a)

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ f (hI.dpow n ↑(Classical.choose ⋯)) = f (hI.dpow n a)
Tactic:
rw [← sub_eq_zero, ← map_sub, ← RingHom.mem_ker]
State after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ hI.dpow n ↑(Classical.choose ⋯) - hI.dpow n a ∈ RingHom.ker f

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ hI.dpow n ↑(Classical.choose ⋯) - hI.dpow n a ∈ RingHom.ker f
Tactic:
rw [isSubDPIdeal_inf_iff] at hIf
State after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ hI.dpow n ↑(Classical.choose ⋯) - hI.dpow n a ∈ RingHom.ker f

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ hI.dpow n ↑(Classical.choose ⋯) - hI.dpow n a ∈ RingHom.ker f
Tactic:
apply hIf n _ a _ ha
State after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose ⋯) - a ∈ RingHom.ker f

A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose ⋯) ∈ I

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose ⋯) - a ∈ RingHom.ker f

A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose ⋯) ∈ I
Tactic:
rw [RingHom.mem_ker, map_sub, sub_eq_zero]
State after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ f ↑(Classical.choose ⋯) = f a

A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose ⋯) ∈ I

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ f ↑(Classical.choose ⋯) = f a

A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose ⋯) ∈ I
Tactic:
rw [h.choose_spec]
State after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose ⋯) ∈ I

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ RingHom.ker f → hI.dpow n a - hI.dpow n b ∈ RingHom.ker f
n : ℕ
a : A
ha : a ∈ I
h : ∃ a_1, f ↑a_1 = f a
⊢ ↑(Classical.choose ⋯) ∈ I
Tactic:
simp only [Submodule.coe_mem]
State after:
no goals

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ ∃ a_1, f ↑a_1 = f a
Tactic:
use ⟨a, ha⟩
State after:
no goals