ι : Type ?u.800477
β : Type u
α : Type v
γ✝ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝³ : CommMonoid β
γ : Type u_1
inst✝² : DecidableEq α
inst✝¹ : OrderedCommMonoid γ
inst✝ : CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m in erase s d, f m < ∏ m in insert d (erase s d), f m
ι : Type ?u.800477
β : Type u
α : Type v
γ✝ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝³ : CommMonoid β
γ : Type u_1
inst✝² : DecidableEq α
inst✝¹ : OrderedCommMonoid γ
inst✝ : CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m in erase s d, f m < ∏ m in s, f m
conv in ∏ m in s, f m => rw [← Finset.insert_erase hd]
ι : Type ?u.800477
β : Type u
α : Type v
γ✝ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝³ : CommMonoid β
γ : Type u_1
inst✝² : DecidableEq α
inst✝¹ : OrderedCommMonoid γ
inst✝ : CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m in erase s d, f m < f d * ∏ x in erase s d, f x
ι : Type ?u.800477
β : Type u
α : Type v
γ✝ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝³ : CommMonoid β
γ : Type u_1
inst✝² : DecidableEq α
inst✝¹ : OrderedCommMonoid γ
inst✝ : CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m in erase s d, f m < ∏ m in insert d (erase s d), f m
rw [Finset.prod_insert (Finset.not_mem_erase d s)]
no goals
ι : Type ?u.800477
β : Type u
α : Type v
γ✝ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝³ : CommMonoid β
γ : Type u_1
inst✝² : DecidableEq α
inst✝¹ : OrderedCommMonoid γ
inst✝ : CovariantClass γ γ (fun x x_1 => x * x_1) fun x x_1 => x < x_1
s : Finset α
d : α
hd : d ∈ s
f : α → γ
hdf : 1 < f d
⊢ ∏ m in erase s d, f m < f d * ∏ x in erase s d, f x
exact lt_mul_of_one_lt_left' _ hdf