-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem prod_eq_prod_iff_of_le {f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) :
    ((∏ i ∈ s, f i) = ∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ≤ g i
⊢ ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i

Tactic:
classical
  revert h
  refine Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h),
    fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_
  specialize ih fun i ↦ H i ∘ Finset.mem_insert_of_mem
  rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]
  exact
    mul_eq_mul_iff_eq_and_eq (H a (s.mem_insert_self a))
      (Finset.prod_le_prod' fun i ↦ H i ∘ Finset.mem_insert_of_mem)

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
H : ∀ i ∈ insert a s, f i ≤ g i
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
⊢ ∏ i ∈ insert a s, f i = ∏ i ∈ insert a s, g i ↔ ∀ i ∈ insert a s, f i = g i

Tactic:
rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]

Result:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
H : ∀ i ∈ insert a s, f i ≤ g i
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
⊢ f a * ∏ x ∈ s, f x = g a * ∏ x ∈ s, g x ↔ f a = g a ∧ ∏ i ∈ s, f i = ∏ i ∈ s, g i

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s : Finset ι
f g : ι → M
⊢ (∀ i ∈ s, f i ≤ g i) → (∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i)

Tactic:
refine Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.not_mem_empty _ h),
  fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_

Result:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, f i ≤ g i) → (∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i)
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ ∏ i ∈ insert a s, f i = ∏ i ∈ insert a s, g i ↔ ∀ i ∈ insert a s, f i = g i

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : (∀ i ∈ s, f i ≤ g i) → (∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i)
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ ∏ i ∈ insert a s, f i = ∏ i ∈ insert a s, g i ↔ ∀ i ∈ insert a s, f i = g i

Tactic:
specialize ih fun i ↦ H i ∘ Finset.mem_insert_of_mem

Result:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
H : ∀ i ∈ insert a s, f i ≤ g i
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
⊢ ∏ i ∈ insert a s, f i = ∏ i ∈ insert a s, g i ↔ ∀ i ∈ insert a s, f i = g i

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ≤ g i
⊢ ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i

Tactic:
revert h

Result:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s : Finset ι
f g : ι → M
⊢ (∀ i ∈ s, f i ≤ g i) → (∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i)

Proof state:
ι : Type u_1
M : Type u_4
inst✝ : OrderedCancelCommMonoid M
s✝ : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
H : ∀ i ∈ insert a s, f i ≤ g i
ih : ∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
⊢ f a * ∏ x ∈ s, f x = g a * ∏ x ∈ s, g x ↔ f a = g a ∧ ∏ i ∈ s, f i = ∏ i ∈ s, g i

Tactic:
exact
  mul_eq_mul_iff_eq_and_eq (H a (s.mem_insert_self a))
    (Finset.prod_le_prod' fun i ↦ H i ∘ Finset.mem_insert_of_mem)

Result:
no goals