no goals
ι : Type ?u.355390
ι' : Type ?u.355393
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ map (fun s => ∏ b in s, f b) atTop ≤ map (fun s => ∏ x in s, g x) atTop
classical
  refine' ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => _
  let ⟨v, hv⟩ := h_eq b
  refine ⟨v, trivial, ?_⟩
  simpa [image_subset_iff] using hv
ι : Type ?u.355390
ι' : Type ?u.355393
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
b : Finset γ
x✝ : True
⊢ ∃ i, True ∧ (fun s => ∏ b in s, f b) '' Ici i ⊆ (fun s => ∏ x in s, g x) '' Ici b
ι : Type ?u.355390
ι' : Type ?u.355393
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ map (fun s => ∏ b in s, f b) atTop ≤ map (fun s => ∏ x in s, g x) atTop
refine' ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => _
ι : Type ?u.355390
ι' : Type ?u.355393
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
b : Finset γ
x✝ : True
v : Finset β
hv : ∀ (v' : Finset β), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ ∃ i, True ∧ (fun s => ∏ b in s, f b) '' Ici i ⊆ (fun s => ∏ x in s, g x) '' Ici b
ι : Type ?u.355390
ι' : Type ?u.355393
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
b : Finset γ
x✝ : True
⊢ ∃ i, True ∧ (fun s => ∏ b in s, f b) '' Ici i ⊆ (fun s => ∏ x in s, g x) '' Ici b
let ⟨v, hv⟩ := h_eq b
ι : Type ?u.355390
ι' : Type ?u.355393
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
b : Finset γ
x✝ : True
v : Finset β
hv : ∀ (v' : Finset β), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ (fun s => ∏ b in s, f b) '' Ici v ⊆ (fun s => ∏ x in s, g x) '' Ici b
ι : Type ?u.355390
ι' : Type ?u.355393
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
b : Finset γ
x✝ : True
v : Finset β
hv : ∀ (v' : Finset β), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ ∃ i, True ∧ (fun s => ∏ b in s, f b) '' Ici i ⊆ (fun s => ∏ x in s, g x) '' Ici b
refine ⟨v, trivial, ?_⟩
no goals
ι : Type ?u.355390
ι' : Type ?u.355393
α : Type u_1
β : Type u_3
γ : Type u_2
inst✝ : CommMonoid α
f : β → α
g : γ → α
h_eq : ∀ (u : Finset γ), ∃ v, ∀ (v' : Finset β), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
b : Finset γ
x✝ : True
v : Finset β
hv : ∀ (v' : Finset β), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x in u', g x = ∏ b in v', f b
⊢ (fun s => ∏ b in s, f b) '' Ici v ⊆ (fun s => ∏ x in s, g x) '' Ici b
simpa [image_subset_iff] using hv