-- Mathlib/RingTheory/Coprime/Ideal.lean
theorem iSup_iInf_eq_top_iff_pairwise {t : Finset ι} (h : t.Nonempty) (I : ι → Ideal R) :
    (⨆ i ∈ t, ⨅ (j) (_ : j ∈ t) (_ : j ≠ i), I j) = ⊤ ↔
      (t : Set ι).Pairwise fun i j => I i ⊔ I j = ⊤

Proof state:
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 ⟨1, ⋯⟩ else 0) a) = 1

Tactic:
simp only [dif_pos, Submodule.coe_mk, eq_self_iff_true]

Result:
no goals

Proof state:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
hs : (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
⊢ ∑ i ∈ Finset.cons a t hat, ↑((fun i => if hi : i = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ i), ⋯⟩) i) = 1

Tactic:
dsimp only

Result:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
hs : (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
⊢ ∑ i ∈ Finset.cons a t hat, ↑(if hi : i = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ i), ⋯⟩) = 1

Proof state:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
hs : (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ↑(μ i) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j
⊢ u * ↑(μ i) ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j

Tactic:
simp only [mem_iInf] at this ⊢

Result:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
hs : (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
⊢ ∀ i_1 ∈ Finset.cons a t hat, i_1 ≠ i → u * ↑(μ i) ∈ I i_1

Proof state:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
⊢ ↑(μ x) ∈ I a

Tactic:
have := Submodule.coe_mem (μ x)

Result:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ∑ x ∈ t, ↑(μ x) + ↑(μ a) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
x : ι
hx : x ∈ t
this : ↑(μ x) ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j
⊢ ↑(μ x) ∈ I a

Proof state:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
hs : (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ↑(if hi : j = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ j), ⋯⟩) = u * ↑(μ j)

Tactic:
rw [dif_neg]

Result:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
hs : (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ¬j = a

Proof state:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
hs : (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
⊢ ∀ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) = u * ↑(μ x)

Tactic:
intro j hj

Result:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
hs : (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ ↑(if hi : j = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ j), ⋯⟩) = u * ↑(μ j)

Proof state:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
x✝ : ι
a✝ : x✝ ∈ t
⊢ ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i => ⟨↑(μ i), ⋯⟩) x✝) =
    Pi.single (Exists.choose h) (↑(μ a)) x✝ + ↑(μ x✝)

Tactic:
rename_i i _

Result:
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 : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j => I i ⊔ I j = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
i : ι
a✝ : i ∈ t
⊢ ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i => ⟨↑(μ i), ⋯⟩) i) =
    Pi.single (Exists.choose h) (↑(μ a)) i + ↑(μ i)