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

State before:
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
⊢ hI'.isSubDPIdeal (hI.dpEqualizer hI')
Tactic:
apply isSubDPIdeal.mk
State after:
case isSubIdeal
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
⊢ hI.dpEqualizer hI' ≤ I

case dpow_mem
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 : ℕ), n ≠ 0 → ∀ j ∈ hI.dpEqualizer hI', hI'.dpow n j ∈ hI.dpEqualizer hI'

State before:
case isSubIdeal
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
⊢ hI.dpEqualizer hI' ≤ I
Tactic:
intro x hx
State after:
case isSubIdeal
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
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ x ∈ I

State before:
case isSubIdeal
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
x : A
hx : x ∈ hI.dpEqualizer hI'
⊢ x ∈ I
Tactic:
rw [mem_dpEqualizer_iff] at hx
State after:
case isSubIdeal
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
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ x ∈ I

State before:
case isSubIdeal
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
x : A
hx : x ∈ I ∧ ∀ (n : ℕ), hI.dpow n x = hI'.dpow n x
⊢ x ∈ I
Tactic:
exact hx.1
State after:
no goals

State before:
case dpow_mem
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 : ℕ), n ≠ 0 → ∀ j ∈ hI.dpEqualizer hI', hI'.dpow n j ∈ hI.dpEqualizer hI'
Tactic:
intro n hn x hx
State after:
case dpow_mem
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 ∈ hI.dpEqualizer hI'
⊢ hI'.dpow n x ∈ hI.dpEqualizer hI'

State before:
case dpow_mem
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 ∈ hI.dpEqualizer hI'
⊢ hI'.dpow n x ∈ hI.dpEqualizer hI'
Tactic:
rw [mem_dpEqualizer_iff] at hx ⊢
State after:
case dpow_mem
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 ∧ ∀ (n_1 : ℕ), hI.dpow n_1 (hI'.dpow n x) = hI'.dpow n_1 (hI'.dpow n x)

State before:
case dpow_mem
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 ∧ ∀ (n_1 : ℕ), hI.dpow n_1 (hI'.dpow n x) = hI'.dpow n_1 (hI'.dpow n x)
Tactic:
constructor
State after:
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)

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
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)

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
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)

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]
State after:
no goals