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

State before:
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
⊢ hI.isSubDPIdeal (J ⊓ I) ↔ ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
Tactic:
refine' ⟨fun hIJ n a b ha hb hab => _, fun hIJ => _⟩
State after:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
⊢ hI.dpow n a - hI.dpow n b ∈ J

case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
⊢ hI.isSubDPIdeal (J ⊓ I)

State before:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
⊢ hI.dpow n a - hI.dpow n b ∈ J
Tactic:
have hab' : a - b ∈ I := I.sub_mem ha hb
State after:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ hI.dpow n a - hI.dpow n b ∈ J

State before:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ hI.dpow n a - hI.dpow n b ∈ J
Tactic:
rw [← add_sub_cancel b a, hI.dpow_add' n hb hab', Finset.range_succ,
  Finset.sum_insert Finset.not_mem_range_self, tsub_self, hI.dpow_zero hab', mul_one,
  add_sub_cancel_left]
State after:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∑ x ∈ Finset.range n, hI.dpow x b * hI.dpow (n - x) (a - b) ∈ J

State before:
case refine'_1
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∑ x ∈ Finset.range n, hI.dpow x b * hI.dpow (n - x) (a - b) ∈ J
Tactic:
apply Ideal.sum_mem
State after:
case refine'_1.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∀ c ∈ Finset.range n, hI.dpow c b * hI.dpow (n - c) (a - b) ∈ J

State before:
case refine'_1.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
⊢ ∀ c ∈ Finset.range n, hI.dpow c b * hI.dpow (n - c) (a - b) ∈ J
Tactic:
intro i hi
State after:
case refine'_1.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
i : ℕ
hi : i ∈ Finset.range n
⊢ hI.dpow i b * hI.dpow (n - i) (a - b) ∈ J

State before:
case refine'_1.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
i : ℕ
hi : i ∈ Finset.range n
⊢ hI.dpow i b * hI.dpow (n - i) (a - b) ∈ J
Tactic:
apply SemilatticeInf.inf_le_left J I
State after:
case refine'_1.a.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
i : ℕ
hi : i ∈ Finset.range n
⊢ hI.dpow i b * hI.dpow (n - i) (a - b) ∈ J ⊓ I

State before:
case refine'_1.a.a
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : hI.isSubDPIdeal (J ⊓ I)
n : ℕ
a b : A
ha : a ∈ I
hb : b ∈ I
hab : a - b ∈ J
hab' : a - b ∈ I
i : ℕ
hi : i ∈ Finset.range n
⊢ hI.dpow i b * hI.dpow (n - i) (a - b) ∈ J ⊓ I
Tactic:
exact
  (J ⊓ I).smul_mem _
    (hIJ.dpow_mem (n - i) (ne_of_gt (Nat.sub_pos_of_lt (Finset.mem_range.mp hi))) _
      ⟨hab, hab'⟩)
State after:
no goals

State before:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
⊢ hI.isSubDPIdeal (J ⊓ I)
Tactic:
refine' ⟨SemilatticeInf.inf_le_right J I, fun n hn a ha => ⟨_, hI.dpow_mem hn ha.right⟩⟩
State after:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a ∈ ↑J

State before:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a ∈ ↑J
Tactic:
rw [← sub_zero (hI.dpow n a), ← hI.dpow_eval_zero hn]
State after:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a - hI.dpow n 0 ∈ ↑J

State before:
case refine'_2
A✝ : Type ?u.19361
inst✝¹ : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝ : CommRing A
I : Ideal A
hI : DividedPowers I
J : Ideal A
hIJ : ∀ (n : ℕ) (a b : A), a ∈ I → b ∈ I → a - b ∈ J → hI.dpow n a - hI.dpow n b ∈ J
n : ℕ
hn : n ≠ 0
a : A
ha : a ∈ J ⊓ I
⊢ hI.dpow n a - hI.dpow n 0 ∈ ↑J
Tactic:
exact hIJ n a 0 ha.right I.zero_mem (J.sub_mem ha.left J.zero_mem)
State after:
no goals