internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
case dpow_mem.left
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ hI'.dpow n x ∈ I

case dpow_mem.right
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ ∀ (n_1 : ℕ), hI.dpow n_1 (hI'.dpow n x) = hI'.dpow n_1 (hI'.dpow n x)
Tactic:
apply hI'.dpow_mem hn hx.1
Proof state after:
case dpow_mem.right
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ ∀ (n_1 : ℕ), hI.dpow n_1 (hI'.dpow n x) = hI'.dpow n_1 (hI'.dpow n x)
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
case dpow_mem.right
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ ∀ (n_1 : ℕ), hI.dpow n_1 (hI'.dpow n x) = hI'.dpow n_1 (hI'.dpow n x)
Tactic:
intro m
Proof state after:
case dpow_mem.right
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
m : ℕ
⊢ hI.dpow m (hI'.dpow n x) = hI'.dpow m (hI'.dpow n x)
Theorem: DividedPowers.dpEqualizer_is_dp_ideal_right
Proof state before:
case dpow_mem.right
A✝ : Type ?u.87809
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
n : ℕ
hn : n ≠ 0
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
m : ℕ
⊢ hI.dpow m (hI'.dpow n x) = hI'.dpow m (hI'.dpow n x)
Tactic:
rw [← hx.2, hI.dpow_comp m hn hx.1, hx.2, hx.2, hI'.dpow_comp m hn hx.1]
Proof state after:
no goals
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ Ideal.map f I ≤ hK.dpEqualizer hK'
Tactic:
rw [Ideal.map]
Proof state after:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ Ideal.span (⇑f '' ↑I) ≤ hK.dpEqualizer hK'
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ Ideal.span (⇑f '' ↑I) ≤ hK.dpEqualizer hK'
Tactic:
rw [Ideal.span_le]
Proof state after:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ ⇑f '' ↑I ⊆ ↑(hK.dpEqualizer hK')
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ ⇑f '' ↑I ⊆ ↑(hK.dpEqualizer hK')
Tactic:
rintro b ⟨a, ha, rfl⟩
Proof state after:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ ↑I
⊢ f a ∈ ↑(hK.dpEqualizer hK')
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ ↑I
⊢ f a ∈ ↑(hK.dpEqualizer hK')
Tactic:
simp only [SetLike.mem_coe] at ha ⊢
Proof state after:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ hK.dpEqualizer hK'
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ hK.dpEqualizer hK'
Tactic:
rw [mem_dpEqualizer_iff]
Proof state after:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ K ∧ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ K ∧ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
constructor
Proof state after:
case intro.intro.left
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ K

case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
case intro.intro.left
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ K

case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
apply hI_le_K
Proof state after:
case intro.intro.left.a
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ Ideal.map f I

case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
case intro.intro.left.a
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ Ideal.map f I

case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
exact Ideal.mem_map_of_mem f ha
Proof state after:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
simp only [isDPMorphism, Ideal.map_id, RingHom.id_apply] at hIK hIK'
Proof state after:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n (f a) = f (hI.dpow n a)
hIK' : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK'.dpow n (f a) = f (hI.dpow n a)
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n (f a) = f (hI.dpow n a)
hIK' : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK'.dpow n (f a) = f (hI.dpow n a)
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
intro n
Proof state after:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n (f a) = f (hI.dpow n a)
hIK' : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK'.dpow n (f a) = f (hI.dpow n a)
a : A
ha : a ∈ I
n : ℕ
⊢ hK.dpow n (f a) = hK'.dpow n (f a)
Theorem: DividedPowers.le_equalizer_of_dp_morphism
Proof state before:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n (f a) = f (hI.dpow n a)
hIK' : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK'.dpow n (f a) = f (hI.dpow n a)
a : A
ha : a ∈ I
n : ℕ
⊢ hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
rw [hIK.2 n a ha, hIK'.2 n a ha]
Proof state after:
no goals
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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]
Proof 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)
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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⟩
Proof 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)
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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]
Proof 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)
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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]
Proof 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
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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
Proof 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
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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
Proof 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
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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]
Proof 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
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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]
Proof 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
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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]
Proof state after:
no goals
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply'
Proof 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⟩
Proof state after:
no goals
Theorem: DividedPowers.Quotient.OfSurjective.dpow_apply
Proof 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
⊢ (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Tactic:
rw [dpow_def, dpow_apply' hI hIf ha]
Proof state after:
no goals
Theorem: DividedPowers.Quotient.OfSurjective.isDPMorphism
Proof 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)
⊢ hI.isDPMorphism (dividedPowers hI hf hIf) f
Tactic:
constructor
Proof state after:
case left
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)
⊢ Ideal.map f I ≤ Ideal.map f I

case right
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 ∈ I, (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)