case hst
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Disjoint (s ∩ t) (s \ t)

case hs
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s ∩ t ∩ mulSupport fun i => f i)

case ht
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s \ t ∩ mulSupport fun i => f i)
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ ((∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i) = ∏ᶠ (i : α) (_ : i ∈ s), f i
rw [← finprod_mem_union', inter_union_diff]
case hst
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ s ∩ t ⊓ s \ t ≤ ⊥

case hs
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s ∩ t ∩ mulSupport fun i => f i)

case ht
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s \ t ∩ mulSupport fun i => f i)
case hst
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Disjoint (s ∩ t) (s \ t)

case hs
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s ∩ t ∩ mulSupport fun i => f i)

case ht
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s \ t ∩ mulSupport fun i => f i)
rw [disjoint_iff_inf_le]
no goals
case hst
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ s ∩ t ⊓ s \ t ≤ ⊥

case hs
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s ∩ t ∩ mulSupport fun i => f i)

case ht
α : Type u_1
β : Type ?u.358627
ι : Type ?u.358630
G : Type ?u.358633
M : Type u_2
N : Type ?u.358639
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t✝ t : Set α
h : Set.Finite (s ∩ mulSupport f)
⊢ Set.Finite (s \ t ∩ mulSupport fun i => f i)
exacts [fun x hx => hx.2.2 hx.1.2, h.subset fun x hx => ⟨hx.1.1, hx.2⟩,
  h.subset fun x hx => ⟨hx.1.1, hx.2⟩]