case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)

case neg
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬Set.Finite (s ∩ mulSupport (f ∘ g))
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
by_cases hs : (s ∩ mulSupport (f ∘ g)).Finite
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
have hg : ∀ x ∈ hs.toFinset, ∀ y ∈ hs.toFinset, g x = g y → x = y := by
  simpa only [hs.mem_toFinset]
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : (∏ᶠ (i : β) (_ : i ∈ s), (f ∘ g) i) = ∏ i in Finite.toFinset hs, (f ∘ g) i
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
have := finprod_mem_eq_prod (comp f g) hs
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : (∏ᶠ (i : β) (_ : i ∈ s), f (g i)) = ∏ i in Finite.toFinset hs, f (g i)
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : (∏ᶠ (i : β) (_ : i ∈ s), (f ∘ g) i) = ∏ i in Finite.toFinset hs, (f ∘ g) i
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
unfold Function.comp at this
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : (∏ᶠ (i : β) (_ : i ∈ s), f (g i)) = ∏ i in Finite.toFinset hs, f (g i)
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ x in Finset.image (fun x => g x) (Finite.toFinset hs), f x
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : (∏ᶠ (i : β) (_ : i ∈ s), f (g i)) = ∏ i in Finite.toFinset hs, f (g i)
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
rw [this, ← Finset.prod_image hg]
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : (∏ᶠ (i : β) (_ : i ∈ s), f (g i)) = ∏ i in Finite.toFinset hs, f (g i)
⊢ g '' s ∩ mulSupport f = ↑(Finset.image (fun x => g x) (Finite.toFinset hs)) ∩ mulSupport f
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : (∏ᶠ (i : β) (_ : i ∈ s), f (g i)) = ∏ i in Finite.toFinset hs, f (g i)
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ x in Finset.image (fun x => g x) (Finite.toFinset hs), f x
refine' finprod_mem_eq_prod_of_inter_mulSupport_eq f _
no goals
case pos
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg✝ : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
hg : ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
this : (∏ᶠ (i : β) (_ : i ∈ s), f (g i)) = ∏ i in Finite.toFinset hs, f (g i)
⊢ g '' s ∩ mulSupport f = ↑(Finset.image (fun x => g x) (Finite.toFinset hs)) ∩ mulSupport f
rw [Finset.coe_image, hs.coe_toFinset, ← image_inter_mulSupport_eq, inter_assoc, inter_self]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : Set.Finite (s ∩ mulSupport (f ∘ g))
⊢ ∀ (x : β), x ∈ Finite.toFinset hs → ∀ (y : β), y ∈ Finite.toFinset hs → g x = g y → x = y
simpa only [hs.mem_toFinset]
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬Set.Finite (s ∩ mulSupport fun x => f (g x))
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬Set.Finite (s ∩ mulSupport (f ∘ g))
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
unfold Function.comp at hs
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬Set.Finite (s ∩ mulSupport fun x => f (g x))
⊢ Set.Infinite (g '' s ∩ mulSupport fun i => f i)
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬Set.Finite (s ∩ mulSupport fun x => f (g x))
⊢ (∏ᶠ (i : α) (_ : i ∈ g '' s), f i) = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
rw [finprod_mem_eq_one_of_infinite hs, finprod_mem_eq_one_of_infinite]
no goals
case neg
α : Type u_2
β : Type u_1
ι : Type ?u.350982
G : Type ?u.350985
M : Type u_3
N : Type ?u.350991
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s✝ t : Set α
s : Set β
g : β → α
hg : InjOn g (s ∩ mulSupport (f ∘ g))
hs : ¬Set.Finite (s ∩ mulSupport fun x => f (g x))
⊢ Set.Infinite (g '' s ∩ mulSupport fun i => f i)
rwa [image_inter_mulSupport_eq, infinite_image_iff hg]