ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
⊢ Filter.map (fun s => ∏ i in s, f (g i)) atTop = Filter.map (fun s => ∏ i in s, f i) atTop
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
⊢ Filter.map (fun s => ∏ i in s, f (g i)) atTop = Filter.map (fun s => ∏ i in s, f i) atTop
haveI := Classical.decEq β
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
⊢ ∃ v, ∀ (v' : Finset γ), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x in u', f x = ∏ b in v', f (g b)

case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset γ
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x in u', f (g x) = ∏ b in v', f b
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
⊢ Filter.map (fun s => ∏ i in s, f (g i)) atTop = Filter.map (fun s => ∏ i in s, f i) atTop
apply le_antisymm <;> refine' map_atTop_finset_prod_le_of_prod_eq fun s => _
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x in u', f x = ∏ b in t, f (g b)
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
⊢ ∃ v, ∀ (v' : Finset γ), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x in u', f x = ∏ b in v', f (g b)
refine' ⟨s.preimage g (hg.injOn _), fun t ht => _⟩
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∏ x in Finset.image g t ∪ s, f x = ∏ b in t, f (g b)
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x in u', f x = ∏ b in t, f (g b)
refine' ⟨t.image g ∪ s, Finset.subset_union_right _ _, _⟩
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∏ x in Finset.image g t ∪ s, f x = ∏ x in Finset.image (fun x => g x) t, f x
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∏ x in Finset.image g t ∪ s, f x = ∏ b in t, f (g b)
rw [← Finset.prod_image (hg.injOn _)]
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∀ (x : β), x ∈ Finset.image g t ∪ s → ¬x ∈ Finset.image g t → f x = 1
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∏ x in Finset.image g t ∪ s, f x = ∏ x in Finset.image (fun x => g x) t, f x
refine' (prod_subset (subset_union_left _ _) _).symm
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∀ (x : β), (∃ a, a ∈ t ∧ g a = x) ∨ x ∈ s → (¬∃ a, a ∈ t ∧ g a = x) → f x = 1
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∀ (x : β), x ∈ Finset.image g t ∪ s → ¬x ∈ Finset.image g t → f x = 1
simp only [Finset.mem_union, Finset.mem_image]
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
y : β
hy : (∃ a, a ∈ t ∧ g a = y) ∨ y ∈ s
hyt : ¬∃ a, a ∈ t ∧ g a = y
⊢ y ∈ Set.range g → ∃ a, a ∈ t ∧ g a = y
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
⊢ ∀ (x : β), (∃ a, a ∈ t ∧ g a = x) ∨ x ∈ s → (¬∃ a, a ∈ t ∧ g a = x) → f x = 1
refine' fun y hy hyt => hf y (mt _ hyt)
case a.intro
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
x : γ
hy : (∃ a, a ∈ t ∧ g a = g x) ∨ g x ∈ s
hyt : ¬∃ a, a ∈ t ∧ g a = g x
⊢ ∃ a, a ∈ t ∧ g a = g x
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
y : β
hy : (∃ a, a ∈ t ∧ g a = y) ∨ y ∈ s
hyt : ¬∃ a, a ∈ t ∧ g a = y
⊢ y ∈ Set.range g → ∃ a, a ∈ t ∧ g a = y
rintro ⟨x, rfl⟩
no goals
case a.intro
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset β
t : Finset γ
ht : Finset.preimage s g (_ : InjOn g (g ⁻¹' ↑s)) ⊆ t
x : γ
hy : (∃ a, a ∈ t ∧ g a = g x) ∨ g x ∈ s
hyt : ¬∃ a, a ∈ t ∧ g a = g x
⊢ ∃ a, a ∈ t ∧ g a = g x
exact ⟨x, ht (Finset.mem_preimage.2 <| hy.resolve_left hyt), rfl⟩
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset γ
t : Finset β
ht : Finset.image g s ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x in u', f (g x) = ∏ b in t, f b
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset γ
⊢ ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x in u', f (g x) = ∏ b in v', f b
refine' ⟨s.image g, fun t ht => _⟩
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset γ
t : Finset β
ht : Finset.image g s ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x in u', f (g x) = ∏ x in Finset.preimage t g (_ : InjOn g (g ⁻¹' ↑t)), f (g x)
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset γ
t : Finset β
ht : Finset.image g s ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x in u', f (g x) = ∏ b in t, f b
simp only [← prod_preimage _ _ (hg.injOn _) _ fun x _ => hf x]
no goals
case a
ι : Type ?u.378253
ι' : Type ?u.378256
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
g : γ → β
hg : Injective g
f : β → α
hf : ∀ (x : β), ¬x ∈ Set.range g → f x = 1
this : DecidableEq β
s : Finset γ
t : Finset β
ht : Finset.image g s ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x in u', f (g x) = ∏ x in Finset.preimage t g (_ : InjOn g (g ⁻¹' ↑t)), f (g x)
exact ⟨_, (image_subset_iff_subset_preimage _).1 ht, rfl⟩