case refine'_1
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
⊢ (∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ ∅), s i) f = fun a => ∏ i in ∅, mulIndicator (s i) f a

case refine'_2
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
⊢ ∀ ⦃a : ι⦄ {s_1 : Finset ι},
    ¬a ∈ s_1 →
      ((∀ (i : ι), i ∈ s_1 → ∀ (j : ι), j ∈ s_1 → i ≠ j → Disjoint (s i) (s j)) →
          mulIndicator (⋃ (i : ι) (_ : i ∈ s_1), s i) f = fun a => ∏ i in s_1, mulIndicator (s i) f a) →
        (∀ (i : ι), i ∈ insert a s_1 → ∀ (j : ι), j ∈ insert a s_1 → i ≠ j → Disjoint (s i) (s j)) →
          mulIndicator (⋃ (i : ι) (_ : i ∈ insert a s_1), s i) f = fun a_4 =>
            ∏ i in insert a s_1, mulIndicator (s i) f a_4
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
⊢ (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
refine' Finset.induction_on I _ _
case refine'_2
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ insert a I), s i) f = fun a_1 => ∏ i in insert a I, mulIndicator (s i) f a_1
case refine'_2
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
⊢ ∀ ⦃a : ι⦄ {s_1 : Finset ι},
    ¬a ∈ s_1 →
      ((∀ (i : ι), i ∈ s_1 → ∀ (j : ι), j ∈ s_1 → i ≠ j → Disjoint (s i) (s j)) →
          mulIndicator (⋃ (i : ι) (_ : i ∈ s_1), s i) f = fun a => ∏ i in s_1, mulIndicator (s i) f a) →
        (∀ (i : ι), i ∈ insert a s_1 → ∀ (j : ι), j ∈ insert a s_1 → i ≠ j → Disjoint (s i) (s j)) →
          mulIndicator (⋃ (i : ι) (_ : i ∈ insert a s_1), s i) f = fun a_4 =>
            ∏ i in insert a s_1, mulIndicator (s i) f a_4
intro a I haI ih hI
case refine'_2.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ insert a I), s i) f x✝ = ∏ i in insert a I, mulIndicator (s i) f x✝
case refine'_2
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ insert a I), s i) f = fun a_1 => ∏ i in insert a I, mulIndicator (s i) f a_1
funext
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)

case refine'_2.h.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ ¬x✝ ∈ s a ∩ ⋃ (x : ι) (_ : x ∈ I), s x
case refine'_2.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ insert a I), s i) f x✝ = ∏ i in insert a I, mulIndicator (s i) f x✝
rw [Finset.prod_insert haI, Finset.set_biUnion_insert, mulIndicator_union_of_not_mem_inter,
  ih _]
case refine'_2.h.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ x✝ ∈ s a → ∀ (x : ι), x ∈ I → ¬x✝ ∈ s x
case refine'_2.h.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ ¬x✝ ∈ s a ∩ ⋃ (x : ι) (_ : x ∈ I), s x
simp only [not_exists, exists_prop, mem_iUnion, mem_inter_iff, not_and]
case refine'_2.h.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
hx : x✝ ∈ s a
a' : ι
ha' : a' ∈ I
⊢ ¬x✝ ∈ s a'
case refine'_2.h.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ x✝ ∈ s a → ∀ (x : ι), x ∈ I → ¬x✝ ∈ s x
intro hx a' ha'
case refine'_2.h.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
hx : x✝ ∈ s a
a' : ι
ha' : a' ∈ I
⊢ a ≠ a'
case refine'_2.h.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
hx : x✝ ∈ s a
a' : ι
ha' : a' ∈ I
⊢ ¬x✝ ∈ s a'
refine'
  disjoint_left.1 (hI a (Finset.mem_insert_self _ _) a' (Finset.mem_insert_of_mem ha') _) hx
no goals
case refine'_2.h.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
hx : x✝ ∈ s a
a' : ι
ha' : a' ∈ I
⊢ a ≠ a'
exact (ne_of_mem_of_not_mem ha' haI).symm
case refine'_1
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
a✝ : ∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (s i) (s j)
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ ∅), s i) f = fun a => ∏ i in ∅, mulIndicator (s i) f a
case refine'_1
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
⊢ (∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ ∅), s i) f = fun a => ∏ i in ∅, mulIndicator (s i) f a
intro
case refine'_1.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
a✝ : ∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ ∅), s i) f x✝ = ∏ i in ∅, mulIndicator (s i) f x✝
case refine'_1
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
a✝ : ∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (s i) (s j)
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ ∅), s i) f = fun a => ∏ i in ∅, mulIndicator (s i) f a
funext
no goals
case refine'_1.h
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I : Finset ι
s : ι → Set α
f : α → M
a✝ : ∀ (i : ι), i ∈ ∅ → ∀ (j : ι), j ∈ ∅ → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ mulIndicator (⋃ (i : ι) (_ : i ∈ ∅), s i) f x✝ = ∏ i in ∅, mulIndicator (s i) f x✝
simp
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
i : ι
hi : i ∈ I
j : ι
hj : j ∈ I
hij : i ≠ j
⊢ Disjoint (s i) (s j)
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
⊢ ∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)
intro i hi j hj hij
no goals
α : Type u_2
β : Type ?u.111160
ι✝ : Type ?u.111163
M : Type u_3
N : Type ?u.111169
inst✝ : CommMonoid M
ι : Type u_1
I✝ : Finset ι
s : ι → Set α
f : α → M
a : ι
I : Finset ι
haI : ¬a ∈ I
ih :
  (∀ (i : ι), i ∈ I → ∀ (j : ι), j ∈ I → i ≠ j → Disjoint (s i) (s j)) →
    mulIndicator (⋃ (i : ι) (_ : i ∈ I), s i) f = fun a => ∏ i in I, mulIndicator (s i) f a
hI : ∀ (i : ι), i ∈ insert a I → ∀ (j : ι), j ∈ insert a I → i ≠ j → Disjoint (s i) (s j)
x✝ : α
i : ι
hi : i ∈ I
j : ι
hj : j ∈ I
hij : i ≠ j
⊢ Disjoint (s i) (s j)
exact hI i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij