-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive]
lemma prod_image_le_of_one_le
    {g : ι → ι'} {f : ι' → N} (hf : ∀ u ∈ s.image g, 1 ≤ f u) :
    ∏ u ∈ s.image g, f u ≤ ∏ u ∈ s, f (g u)

Proof state:
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
⊢ f a ≤ f a ^ #(filter (fun a_1 => g a_1 = a) s)

Tactic:
obtain ⟨i, hi, hig⟩ := Finset.mem_image.mp hag

Result:
case intro.intro
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ f a ≤ f a ^ #(filter (fun a_1 => g a_1 = a) s)

Proof state:
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
⊢ ∏ u ∈ image g s, f u ≤ ∏ u ∈ s, f (g u)

Tactic:
rw [prod_comp f g]

Result:
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
⊢ ∏ u ∈ image g s, f u ≤ ∏ b ∈ image g s, f b ^ #(filter (fun a => g a = b) s)

Proof state:
case intro.intro
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ (filter (fun a_1 => g a_1 = a) s).Nonempty

Tactic:
exact ⟨i, mem_filter.mpr ⟨hi, hig⟩⟩

Result:
no goals

Proof state:
case intro.intro
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ f a ≤ f a ^ #(filter (fun a_1 => g a_1 = a) s)

Tactic:
apply le_self_pow (hf a hag)

Result:
case intro.intro
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ #(filter (fun a_1 => g a_1 = a) s) ≠ 0

Proof state:
case intro.intro
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ #(filter (fun a_1 => g a_1 = a) s) ≠ 0

Tactic:
rw [← Nat.pos_iff_ne_zero, card_pos]

Result:
case intro.intro
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
i : ι
hi : i ∈ s
hig : g i = a
⊢ (filter (fun a_1 => g a_1 = a) s).Nonempty

Proof state:
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
⊢ ∏ u ∈ image g s, f u ≤ ∏ b ∈ image g s, f b ^ #(filter (fun a => g a = b) s)

Tactic:
refine prod_le_prod' fun a hag ↦ ?_

Result:
ι : Type u_1
N : Type u_5
inst✝¹ : OrderedCommMonoid N
s : Finset ι
ι' : Type u_9
inst✝ : DecidableEq ι'
g : ι → ι'
f : ι' → N
hf : ∀ u ∈ image g s, 1 ≤ f u
a : ι'
hag : a ∈ image g s
⊢ f a ≤ f a ^ #(filter (fun a_1 => g a_1 = a) s)