[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
⊢ ⨆ (i : ι) (_ : i ∈ t), ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j = ⊤ ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
haveI : DecidableEq ι := Classical.decEq ι
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
this : DecidableEq ι
⊢ ⨆ (i : ι) (_ : i ∈ t), ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j = ⊤ ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
rw [eq_top_iff_one, Submodule.mem_iSup_finset_iff_exists_sum]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
this : DecidableEq ι
⊢ (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
refine' h.cons_induction _ _
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), (∃ μ, (Finset.sum {a} fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑{a} fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
clear t h
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
t : Finset ι
h : Finset.Nonempty t
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ (s : Finset ι) (h : ¬a ∈ s),
    Finset.Nonempty s →
      ((∃ μ, (Finset.sum s fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑s fun i j => I i ⊔ I j = ⊤) →
        ((∃ μ, (Finset.sum (Finset.cons a s h) fun i => ↑(μ i)) = 1) ↔
          Set.Pairwise ↑(Finset.cons a s h) fun i j => I i ⊔ I j = ⊤)
[PROOFSTEP]
clear t h
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), (∃ μ, (Finset.sum {a} fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑{a} fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
simp only [Finset.sum_singleton, Finset.coe_singleton, Set.pairwise_singleton, iff_true_iff]
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ (a : ι), ∃ μ, ↑(μ a) = 1
[PROOFSTEP]
refine' fun a => ⟨fun i => if h : i = a then ⟨1, _⟩ else 0, _⟩
[GOAL]
case refine'_1.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a i : ι
h : i = a
⊢ 1 ∈ ⨅ (j : ι) (_ : j ∈ {a}) (_ : j ≠ i), I j
[PROOFSTEP]
simp [h]
[GOAL]
case refine'_1.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
⊢ ↑((fun i => if h : i = a then { val := 1, property := (_ : 1 ∈ ⨅ (x : ι) (_ : x ∈ {a}) (_ : x ≠ i), I x) } else 0)
        a) =
    1
[PROOFSTEP]
simp only [dif_pos, dif_ctx_congr, Submodule.coe_mk, eq_self_iff_true]
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
⊢ ∀ ⦃a : ι⦄ (s : Finset ι) (h : ¬a ∈ s),
    Finset.Nonempty s →
      ((∃ μ, (Finset.sum s fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑s fun i j => I i ⊔ I j = ⊤) →
        ((∃ μ, (Finset.sum (Finset.cons a s h) fun i => ↑(μ i)) = 1) ↔
          Set.Pairwise ↑(Finset.cons a s h) fun i j => I i ⊔ I j = ⊤)
[PROOFSTEP]
intro a t hat h ih
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
⊢ (∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1) ↔
    Set.Pairwise ↑(Finset.cons a t hat) fun i j => I i ⊔ I j = ⊤
[PROOFSTEP]
rw [Finset.coe_cons, Set.pairwise_insert_of_symmetric fun i j (h : I i ⊔ I j = ⊤) => sup_comm.trans h]
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
⊢ (∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1) ↔
    (Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
[PROOFSTEP]
constructor
[GOAL]
case refine'_2.mp
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
⊢ (∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1) →
    (Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
[PROOFSTEP]
rintro ⟨μ, hμ⟩
[GOAL]
case refine'_2.mp.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
⊢ (Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
[PROOFSTEP]
rw [Finset.sum_cons] at hμ 
[GOAL]
case refine'_2.mp.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
[PROOFSTEP]
refine ⟨ih.mp ⟨Pi.single h.choose ⟨μ a, ?a1⟩ + fun i => ⟨μ i, ?a2⟩, ?a3⟩, fun b hb ab => ?a4⟩
[GOAL]
case a3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i => ↑((Pi.single (Exists.choose h) { val := ↑(μ a), property := ?a1 } + fun i => ?m.8605 i) i)) = 1
case a4
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
case a1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j
case a2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
case a1 =>
  have := Submodule.coe_mem (μ a)
  rw [mem_iInf] at this ⊢
    --for some reason `simp only [mem_iInf]` times out
  intro i
  specialize this i
  rw [mem_iInf, mem_iInf] at this ⊢
  intro hi _
  apply this (Finset.subset_cons _ hi)
  rintro rfl
  exact hat hi
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j
[PROOFSTEP]
case a1 =>
  have := Submodule.coe_mem (μ a)
  rw [mem_iInf] at this ⊢
    --for some reason `simp only [mem_iInf]` times out
  intro i
  specialize this i
  rw [mem_iInf, mem_iInf] at this ⊢
  intro hi _
  apply this (Finset.subset_cons _ hi)
  rintro rfl
  exact hat hi
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j
[PROOFSTEP]
have := Submodule.coe_mem (μ a)
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
this : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j
⊢ ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j
[PROOFSTEP]
rw [mem_iInf] at this ⊢
  --for some reason `simp only [mem_iInf]` times out
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
this : ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ Finset.cons a t hat) (_ : i ≠ a), I i
⊢ ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ t) (_ : i ≠ Exists.choose h), I i
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
this : ∀ (i : ι), ↑(μ a) ∈ ⨅ (_ : i ∈ Finset.cons a t hat) (_ : i ≠ a), I i
i : ι
⊢ ↑(μ a) ∈ ⨅ (_ : i ∈ t) (_ : i ≠ Exists.choose h), I i
[PROOFSTEP]
specialize this i
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : ↑(μ a) ∈ ⨅ (_ : i ∈ Finset.cons a t hat) (_ : i ≠ a), I i
⊢ ↑(μ a) ∈ ⨅ (_ : i ∈ t) (_ : i ≠ Exists.choose h), I i
[PROOFSTEP]
rw [mem_iInf, mem_iInf] at this ⊢
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
⊢ i ∈ t → i ≠ Exists.choose h → ↑(μ a) ∈ I i
[PROOFSTEP]
intro hi _
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
hi : i ∈ t
i✝ : i ≠ Exists.choose h
⊢ ↑(μ a) ∈ I i
[PROOFSTEP]
apply this (Finset.subset_cons _ hi)
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
hi : i ∈ t
i✝ : i ≠ Exists.choose h
⊢ i ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
t : Finset ι
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
i : ι
hi : i ∈ t
i✝ : i ≠ Exists.choose h
hat : ¬i ∈ t
μ : (i_1 : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons i t hat) (_ : j ≠ i_1), I j }
hμ : (↑(μ i) + Finset.sum t fun x => ↑(μ x)) = 1
this : i ∈ Finset.cons i t hat → i ≠ i → ↑(μ i) ∈ I i
⊢ False
[PROOFSTEP]
exact hat hi
[GOAL]
case a3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => ?m.8605 i)
          i)) =
    1
case a4
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
case a2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
case a2 =>
  have := Submodule.coe_mem (μ i)
  simp only [mem_iInf] at this ⊢
  intro j hj ij
  exact this _ (Finset.subset_cons _ hj) ij
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
case a2 =>
  have := Submodule.coe_mem (μ i)
  simp only [mem_iInf] at this ⊢
  intro j hj ij
  exact this _ (Finset.subset_cons _ hj) ij
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
have := Submodule.coe_mem (μ i)
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j
⊢ ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
[PROOFSTEP]
simp only [mem_iInf] at this ⊢
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : ∀ (i_1 : ι), i_1 ∈ Finset.cons a t hat → i_1 ≠ i → ↑(μ i) ∈ I i_1
⊢ ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
[PROOFSTEP]
intro j hj ij
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
i : ι
this : ∀ (i_1 : ι), i_1 ∈ Finset.cons a t hat → i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ t
ij : j ≠ i
⊢ ↑(μ i) ∈ I j
[PROOFSTEP]
exact this _ (Finset.subset_cons _ hj) ij
[GOAL]
case a3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
          i)) =
    1
case a4
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
[PROOFSTEP]
case a3 =>
  rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib] at hμ 
  convert hμ
  rename_i i _
  rw [Pi.add_apply, Submodule.coe_add, Submodule.coe_mk]
  by_cases hi : i = h.choose
  · rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]
  · rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
          i)) =
    1
[PROOFSTEP]
case a3 =>
  rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib] at hμ 
  convert hμ
  rename_i i _
  rw [Pi.add_apply, Submodule.coe_add, Submodule.coe_mk]
  by_cases hi : i = h.choose
  · rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]
  · rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
          i)) =
    1
[PROOFSTEP]
rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib] at hμ 
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
⊢ (Finset.sum t fun i =>
      ↑((Pi.single (Exists.choose h)
              { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
            fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
          i)) =
    1
[PROOFSTEP]
convert hμ
[GOAL]
case h.e'_2.a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
x✝ : ι
a✝ : x✝ ∈ t
⊢ ↑((Pi.single (Exists.choose h)
            { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
          fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
        x✝) =
    Pi.single (Exists.choose h) (↑(μ a)) x✝ + ↑(μ x✝)
[PROOFSTEP]
rename_i i _
[GOAL]
case h.e'_2.a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
⊢ ↑((Pi.single (Exists.choose h)
            { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } +
          fun i => { val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) })
        i) =
    Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
[PROOFSTEP]
rw [Pi.add_apply, Submodule.coe_add, Submodule.coe_mk]
[GOAL]
case h.e'_2.a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
⊢ ↑(Pi.single (Exists.choose h)
          { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } i) +
      ↑{ val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) } =
    Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
[PROOFSTEP]
by_cases hi : i = h.choose
[GOAL]
case pos
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h)
          { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } i) +
      ↑{ val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) } =
    Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
[PROOFSTEP]
rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ✝ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
hμ : (Finset.sum t fun x => Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
hi : ¬i = Exists.choose h
⊢ ↑(Pi.single (Exists.choose h)
          { val := ↑(μ a), property := (_ : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ Exists.choose h), I j) } i) +
      ↑{ val := ↑(μ i), property := (_ : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j) } =
    Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)
[PROOFSTEP]
rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]
[GOAL]
case a4
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
[PROOFSTEP]
case a4 =>
  rw [eq_top_iff_one, Submodule.mem_sup]
  rw [add_comm] at hμ 
  refine' ⟨_, _, _, _, hμ⟩
  · refine' sum_mem _ fun x hx => _
    have := Submodule.coe_mem (μ x)
    simp only [mem_iInf] at this 
    apply this _ (Finset.mem_cons_self _ _)
    rintro rfl
    exact hat hx
  · have := Submodule.coe_mem (μ a)
    simp only [mem_iInf] at this 
    exact this _ (Finset.subset_cons _ hb) ab.symm
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
[PROOFSTEP]
case a4 =>
  rw [eq_top_iff_one, Submodule.mem_sup]
  rw [add_comm] at hμ 
  refine' ⟨_, _, _, _, hμ⟩
  · refine' sum_mem _ fun x hx => _
    have := Submodule.coe_mem (μ x)
    simp only [mem_iInf] at this 
    apply this _ (Finset.mem_cons_self _ _)
    rintro rfl
    exact hat hx
  · have := Submodule.coe_mem (μ a)
    simp only [mem_iInf] at this 
    exact this _ (Finset.subset_cons _ hb) ab.symm
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤
[PROOFSTEP]
rw [eq_top_iff_one, Submodule.mem_sup]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (↑(μ a) + Finset.sum t fun x => ↑(μ x)) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∃ y, y ∈ I a ∧ ∃ z, z ∈ I b ∧ y + z = 1
[PROOFSTEP]
rw [add_comm] at hμ 
[GOAL]
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ∃ y, y ∈ I a ∧ ∃ z, z ∈ I b ∧ y + z = 1
[PROOFSTEP]
refine' ⟨_, _, _, _, hμ⟩
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ (Finset.sum t fun x => ↑(μ x)) ∈ I a
[PROOFSTEP]
refine' sum_mem _ fun x hx => _
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
⊢ ↑(μ x) ∈ I a
[PROOFSTEP]
have := Submodule.coe_mem (μ x)
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
this : ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j
⊢ ↑(μ x) ∈ I a
[PROOFSTEP]
simp only [mem_iInf] at this 
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
this : ∀ (i : ι), i ∈ Finset.cons a t hat → i ≠ x → ↑(μ x) ∈ I i
⊢ ↑(μ x) ∈ I a
[PROOFSTEP]
apply this _ (Finset.mem_cons_self _ _)
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
this : ∀ (i : ι), i ∈ Finset.cons a t hat → i ≠ x → ↑(μ x) ∈ I i
⊢ a ≠ x
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
hx : a ∈ t
this : ∀ (i : ι), i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
⊢ False
[PROOFSTEP]
exact hat hx
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ ↑(μ a) ∈ I b
[PROOFSTEP]
have := Submodule.coe_mem (μ a)
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
this : ↑(μ a) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j
⊢ ↑(μ a) ∈ I b
[PROOFSTEP]
simp only [mem_iInf] at this 
[GOAL]
case refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun x => ↑(μ x)) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
this : ∀ (i : ι), i ∈ Finset.cons a t hat → i ≠ a → ↑(μ a) ∈ I i
⊢ ↑(μ a) ∈ I b
[PROOFSTEP]
exact this _ (Finset.subset_cons _ hb) ab.symm
[GOAL]
case refine'_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
⊢ ((Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤) ∧ ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
rintro ⟨hs, Hb⟩
[GOAL]
case refine'_2.mpr.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
obtain ⟨μ, hμ⟩ := ih.mpr hs
[GOAL]
case refine'_2.mpr.intro.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
have := sup_iInf_eq_top fun b hb => Hb b hb (ne_of_mem_of_not_mem hb hat).symm
[GOAL]
case refine'_2.mpr.intro.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
this : I a ⊔ ⨅ (i : ι) (_ : i ∈ t), I i = ⊤
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
rw [eq_top_iff_one, Submodule.mem_sup] at this 
[GOAL]
case refine'_2.mpr.intro.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
this : ∃ y, y ∈ I a ∧ ∃ z, z ∈ ⨅ (i : ι) (_ : i ∈ t), I i ∧ y + z = 1
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
obtain ⟨u, hu, v, hv, huv⟩ := this
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
⊢ ∃ μ, (Finset.sum (Finset.cons a t hat) fun i => ↑(μ i)) = 1
[PROOFSTEP]
refine' ⟨fun i => if hi : i = a then ⟨v, _⟩ else ⟨u * μ i, _⟩, _⟩
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : i = a
⊢ v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j
[PROOFSTEP]
simp only [mem_iInf] at hv ⊢
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι), i ∈ t → v ∈ I i
⊢ ∀ (i_1 : ι), i_1 ∈ Finset.cons a t hat → i_1 ≠ i → v ∈ I i_1
[PROOFSTEP]
intro j hj ij
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι), i ∈ t → v ∈ I i
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ v ∈ I j
[PROOFSTEP]
rw [Finset.mem_cons, ← hi] at hj 
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι), i ∈ t → v ∈ I i
j : ι
hj : j = i ∨ j ∈ t
ij : j ≠ i
⊢ v ∈ I j
[PROOFSTEP]
exact hv _ (hj.resolve_left ij)
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
⊢ u * ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j
[PROOFSTEP]
have := Submodule.coe_mem (μ i)
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j
⊢ u * ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j
[PROOFSTEP]
simp only [mem_iInf] at this ⊢
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
⊢ ∀ (i_1 : ι), i_1 ∈ Finset.cons a t hat → i_1 ≠ i → u * ↑(μ i) ∈ I i_1
[PROOFSTEP]
intro j hj ij
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ u * ↑(μ i) ∈ I j
[PROOFSTEP]
rcases Finset.mem_cons.mp hj with (rfl | hj)
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2.inl
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
t : Finset ι
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
this : ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
ij : j ≠ i
hat : ¬j ∈ t
Hb : ∀ (b : ι), b ∈ ↑t → j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
hi : ¬i = j
hj : j ∈ Finset.cons j t hat
⊢ u * ↑(μ i) ∈ I j
[PROOFSTEP]
exact mul_mem_right _ _ hu
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_2.inr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ (i_1 : ι), i_1 ∈ t → i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj✝ : j ∈ Finset.cons a t hat
ij : j ≠ i
hj : j ∈ t
⊢ u * ↑(μ i) ∈ I j
[PROOFSTEP]
exact mul_mem_left _ _ (this _ hj ij)
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
⊢ (Finset.sum (Finset.cons a t hat) fun i =>
      ↑((fun i =>
            if hi : i = a then
              { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j) }
            else
              { val := u * ↑(μ i),
                property := (_ : u * ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j) })
          i)) =
    1
[PROOFSTEP]
dsimp only
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
⊢ (Finset.sum (Finset.cons a t hat) fun i =>
      ↑(if hi : i = a then { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j) }
        else
          { val := u * ↑(μ i),
            property := (_ : u * ↑(μ i) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ i), I j) })) =
    1
[PROOFSTEP]
rw [Finset.sum_cons, dif_pos rfl, add_comm]
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u + v = 1
⊢ (Finset.sum t fun x =>
        ↑(if hi : x = a then
            { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
          else
            { val := u * ↑(μ x),
              property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) })) +
      ↑{ val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j) } =
    1
[PROOFSTEP]
rw [← mul_one u] at huv 
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
⊢ (Finset.sum t fun x =>
        ↑(if hi : x = a then
            { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
          else
            { val := u * ↑(μ x),
              property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) })) +
      ↑{ val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j) } =
    1
[PROOFSTEP]
rw [← huv, ← hμ, Finset.mul_sum]
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
⊢ (Finset.sum t fun x =>
        ↑(if hi : x = a then
            { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
          else
            { val := u * ↑(μ x),
              property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) })) +
      ↑{ val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ a), I j) } =
    (Finset.sum t fun x => u * ↑(μ x)) + v
[PROOFSTEP]
congr 1
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
⊢ (Finset.sum t fun x =>
      ↑(if hi : x = a then { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
        else
          { val := u * ↑(μ x),
            property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) })) =
    Finset.sum t fun x => u * ↑(μ x)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
⊢ ∀ (x : ι),
    x ∈ t →
      ↑(if hi : x = a then { val := v, property := (_ : v ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }
          else
            { val := u * ↑(μ x),
              property := (_ : u * ↑(μ x) ∈ ⨅ (j : ι) (_ : j ∈ Finset.cons a t hat) (_ : j ≠ x), I j) }) =
        u * ↑(μ x)
[PROOFSTEP]
intro j hj
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ↑(if hi : j = a then
        { val := v, property := (_ : v ∈ ⨅ (j_1 : ι) (_ : j_1 ∈ Finset.cons a t hat) (_ : j_1 ≠ j), I j_1) }
      else
        { val := u * ↑(μ j),
          property := (_ : u * ↑(μ j) ∈ ⨅ (j_1 : ι) (_ : j_1 ∈ Finset.cons a t hat) (_ : j_1 ≠ j), I j_1) }) =
    u * ↑(μ j)
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a.hnc
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : ¬a ∈ t
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
Hb : ∀ (b : ι), b ∈ ↑t → a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ¬j = a
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2.mpr.intro.intro.intro.intro.intro.intro.refine'_3.e_a.hnc
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
t : Finset ι
h : Finset.Nonempty t
ih : (∃ μ, (Finset.sum t fun i => ↑(μ i)) = 1) ↔ Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
hs : Set.Pairwise ↑t fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → { x // x ∈ ⨅ (j : ι) (_ : j ∈ t) (_ : j ≠ i), I j }
hμ : (Finset.sum t fun i => ↑(μ i)) = 1
u v : R
hv : v ∈ ⨅ (i : ι) (_ : i ∈ t), I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
hat : ¬j ∈ t
Hb : ∀ (b : ι), b ∈ ↑t → j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
⊢ False
[PROOFSTEP]
exact hat hj
