-- Mathlib/Order/Filter/AtTopBot/BigOperators.lean
theorem Filter.map_atTop_finset_prod_le_of_prod_eq {f : α → M} {g : β → M}
    (h_eq : ∀ u : Finset β,
      ∃ v : Finset α, ∀ v', v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b) :
    (atTop.map fun s : Finset α => ∏ b ∈ s, f b) ≤
      atTop.map fun s : Finset β => ∏ x ∈ s, g x

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
b : Finset β
x✝ : True
⊢ ∃ i, True ∧ (fun s => ∏ b ∈ s, f b) '' Set.Ici i ⊆ (fun s => ∏ x ∈ s, g x) '' Set.Ici b

Tactic:
let ⟨v, hv⟩ := h_eq b

Result:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
b : Finset β
x✝ : True
v : Finset α
hv : ∀ (v' : Finset α), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
⊢ ∃ i, True ∧ (fun s => ∏ b ∈ s, f b) '' Set.Ici i ⊆ (fun s => ∏ x ∈ s, g x) '' Set.Ici b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
b : Finset β
x✝ : True
v : Finset α
hv : ∀ (v' : Finset α), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
⊢ (fun s => ∏ b ∈ s, f b) '' Set.Ici v ⊆ (fun s => ∏ x ∈ s, g x) '' Set.Ici b

Tactic:
simpa [Finset.image_subset_iff] using hv

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
b : Finset β
x✝ : True
v : Finset α
hv : ∀ (v' : Finset α), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
⊢ ∃ i, True ∧ (fun s => ∏ b ∈ s, f b) '' Set.Ici i ⊆ (fun s => ∏ x ∈ s, g x) '' Set.Ici b

Tactic:
refine ⟨v, trivial, ?_⟩

Result:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
b : Finset β
x✝ : True
v : Finset α
hv : ∀ (v' : Finset α), v ⊆ v' → ∃ u', b ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
⊢ (fun s => ∏ b ∈ s, f b) '' Set.Ici v ⊆ (fun s => ∏ x ∈ s, g x) '' Set.Ici b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
⊢ map (fun s => ∏ b ∈ s, f b) atTop ≤ map (fun s => ∏ x ∈ s, g x) atTop

Tactic:
refine ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => ?_

Result:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
b : Finset β
x✝ : True
⊢ ∃ i, True ∧ (fun s => ∏ b ∈ s, f b) '' Set.Ici i ⊆ (fun s => ∏ x ∈ s, g x) '' Set.Ici b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
f : α → M
g : β → M
h_eq : ∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', g x = ∏ b ∈ v', f b
⊢ map (fun s => ∏ b ∈ s, f b) atTop ≤ map (fun s => ∏ x ∈ s, g x) atTop

Tactic:
classical
  refine ((atTop_basis.map _).le_basis_iff (atTop_basis.map _)).2 fun b _ => ?_
  let ⟨v, hv⟩ := h_eq b
  refine ⟨v, trivial, ?_⟩
  simpa [Finset.image_subset_iff] using hv

Result:
no goals