awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hf : Injective f
hs : (↑s : Set ι).PairwiseDisjoint f
grw : #(s.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + 1
grw₁ grw₂ : #(s.biUnion f) + 1 ≤ #(s.biUnion f) + 1
⊢ #s ≤ #(s.biUnion f) + 1

Tactic:
grw [card_le_card_biUnion_add_card_fiber hs,
    card_le_one.2 fun _ hi _ hj ↦ hf <| (mem_filter.1 hi).2.trans (mem_filter.1 hj).2.symm]

Premises used: Iff.mpr, Finset.card_le_one, Finset.card_le_card_biUnion_add_card_fiber
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s : Finset ι
i : ι
hi : i ∈ s
⊢ f i ≤ ∏ j ∈ s, f j

Tactic:
have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
  single_le_prod' (fun _ _ ↦ one_le) hi

Premises used: CanonicallyOrderedMul.toIsOrderedMonoid, Finset.single_le_prod', one_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : s ⊆ t
⊢ LE.le.{u_4} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, f x)

Tactic:
have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
  prod_le_prod_of_subset_of_one_le' h fun _ _ _ ↦ one_le

Premises used: CanonicallyOrderedMul.toIsOrderedMonoid, Finset.prod_le_prod_of_subset_of_one_le', one_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
⊢ Monotone.{u_1, u_4} (β := M) fun (s : Finset ι) ↦ ∏ x ∈ s, f x

Tactic:
fun _ _ hs ↦
  have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
  prod_le_prod_of_subset' hs

Premises used: CanonicallyOrderedMul.toIsOrderedMonoid, Monotone, Finset.prod_le_prod_of_subset'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
⊢ IsOrderedMonoid M

Tactic:
have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
rw : Disjoint ({x ∈ s | f x = 1}) ({x ∈ s | f x ≠ 1})
⊢ ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s with f x = 1, f x) (∏ x ∈ s with f x ≠ 1, f x)

Tactic:
rw [← prod_union, filter_union_filter_not_eq]

Premises used: Finset.prod_union, Finset.filter_union_filter_not_eq
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ Disjoint ({x ∈ s | f x = 1}) ({x ∈ s | f x ≠ 1})

Tactic:
disjoint_filter.2 fun _ _ h n_h ↦ n_h h

Premises used: Iff.mpr, Finset.disjoint_filter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ Disjoint ({x ∈ s | f x = 1}) ({x ∈ s | f x ≠ 1})

Tactic:
exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h

Premises used: Iff.mpr, Finset.disjoint_filter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
simp : ∀ i ∈ s, f i = 1 → f i ≤ 1
⊢ ∀ i ∈ {x ∈ s | f x = 1}, f i ≤ 1

Tactic:
simp only [mem_filter, and_imp]

Premises used: and_imp, Finset.mem_filter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∀ i ∈ s, f i = 1 → f i ≤ 1

Tactic:
fun _ _ ↦ le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ ∀ i ∈ s, f i = 1 → f i ≤ 1

Tactic:
exact fun _ _ ↦ le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
⊢ {x ∈ s | f x ≠ 1} ⊆ t

Tactic:
simpa only [subset_iff, mem_filter, and_imp]

Premises used: and_imp, Finset.subset_iff, Finset.mem_filter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
x : ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s with f x = 1, f x) (∏ x ∈ s with f x ≠ 1, f x)
⊢ LE.le.{u_4} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, f x)

Tactic:
calc
    ∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x := by
      rw [← prod_union, filter_union_filter_not_eq]
      exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
    _ ≤ ∏ x ∈ t, f x :=
      mul_le_of_le_one_of_le
        (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
        (prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp])

Premises used: mul_le_of_le_one_of_le, Finset.prod_le_prod_of_subset', Finset.prod_le_one', Finset.prod, OfNat.ofNat, Finset.filter, Eq
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s t : Finset ι
h : ∀ x ∈ s, f x ≠ 1 → x ∈ t
this : IsOrderedMonoid M
classical : ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s with f x = 1, f x) (∏ x ∈ s with f x ≠ 1, f x)
⊢ LE.le.{u_4} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, f x)

Tactic:
classical calc
    ∏ x ∈ s, f x = (∏ x ∈ s with f x = 1, f x) * ∏ x ∈ s with f x ≠ 1, f x := by
      rw [← prod_union, filter_union_filter_not_eq]
      exact disjoint_filter.2 fun _ _ h n_h ↦ n_h h
    _ ≤ ∏ x ∈ t, f x :=
      mul_le_of_le_one_of_le
        (prod_le_one' <| by simp only [mem_filter, and_imp]; exact fun _ _ ↦ le_of_eq)
        (prod_le_prod_of_subset' <| by simpa only [subset_iff, mem_filter, and_imp])

Premises used: mul_le_of_le_one_of_le, Finset.prod_le_prod_of_subset', Finset.prod_le_one'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : CanonicallyOrderedMul M
f : ι → M
s : Finset ι
⊢ LT.lt.{u_10} (α := M) 1 (∏ x ∈ s, f x) ↔ ∃ x ∈ s, 1 < f x

Tactic:
have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
  Finset.one_lt_prod_iff_of_one_le <| fun _ _ => one_le

Premises used: CanonicallyOrderedMul.toIsOrderedMonoid, Finset.one_lt_prod_iff_of_one_le, one_le
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f g : ι → M
s : Finset ι
inst_3 : MulLeftStrictMono M
hle : ∀ i ∈ s, f i ≤ g i
hlt : ∃ i ∈ s, f i < g i
⊢ LT.lt.{u_4} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
Multiset.prod_lt_prod' hle hlt

Premises used: Multiset.prod_lt_prod', Finset.prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f g : ι → M
s : Finset ι
inst_3 : MulLeftStrictMono M
hs : s.Nonempty
hlt : ∀ i ∈ s, f i < g i
⊢ s.val ≠ ∅

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
rw : ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x
⊢ LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ insert i s, f j)

Tactic:
rw [prod_insert hs]

Premises used: Finset.prod_insert
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x

Tactic:
lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt

Premises used: lt_mul_of_one_lt_left', Finset.prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x

Tactic:
exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt

Premises used: lt_mul_of_one_lt_left', Finset.prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
h₁ : insert i s ⊆ t
hf : ∀ i_1 ∈ t, i_1 ∉ insert i s → 1 ≤ f i_1
⊢ LE.le.{u_4} (α := M) (∏ j ∈ insert i s, f j) (∏ j ∈ t, f j)

Tactic:
apply prod_le_prod_of_subset_of_one_le'

Premises used: Finset.prod_le_prod_of_subset_of_one_le'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
⊢ insert i s ⊆ t

Tactic:
simp [Finset.insert_subset_iff, h, ht]

Premises used: Finset.insert_subset_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : x ∉ insert i s
⊢ ¬x = i ∧ x ∉ s

Tactic:
simp only [mem_insert, not_or] at h'x

Premises used: Finset.mem_insert, not_or
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x = i ∧ x ∉ s
⊢ 1 ≤ f x

Tactic:
hle x hx h'x.2

Premises used: And.right
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
x : ι
hx : x ∈ t
h'x : ¬x = i ∧ x ∉ s
⊢ 1 ≤ f x

Tactic:
exact hle x hx h'x.2

Premises used: And.right
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
j : LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ insert i s, f j)
j₁ : LE.le.{u_4} (α := M) (∏ j ∈ insert i s, f j) (∏ j ∈ t, f j)
⊢ LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ t, f j)

Tactic:
calc
    ∏ j ∈ s, f j < ∏ j ∈ insert i s, f j := by
      rw [prod_insert hs]
      exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt
    _ ≤ ∏ j ∈ t, f j := by
      apply prod_le_prod_of_subset_of_one_le'
      · simp [Finset.insert_subset_iff, h, ht]
      · intro x hx h'x
        simp only [mem_insert, not_or] at h'x
        exact hle x hx h'x.2

Premises used: Insert.insert
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : MulLeftStrictMono M
h : s ⊆ t
i : ι
ht : i ∈ t
hs : i ∉ s
hlt : 1 < f i
hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j
classical : LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ insert i s, f j)
classical₁ : LE.le.{u_4} (α := M) (∏ j ∈ insert i s, f j) (∏ j ∈ t, f j)
⊢ LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ t, f j)

Tactic:
classical calc
    ∏ j ∈ s, f j < ∏ j ∈ insert i s, f j := by
      rw [prod_insert hs]
      exact lt_mul_of_one_lt_left' (∏ j ∈ s, f j) hlt
    _ ≤ ∏ j ∈ t, f j := by
      apply prod_le_prod_of_subset_of_one_le'
      · simp [Finset.insert_subset_iff, h, ht]
      · intro x hx h'x
        simp only [mem_insert, not_or] at h'x
        exact hle x hx h'x.2
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst_3 : MulLeftStrictMono M
i j : ι
hij : j ≠ i
hi : i ∈ s
hj : j ∈ s
hlt : 1 < f j
hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k
rw rw₁ : f i = f i
⊢ f i = ∏ k ∈ {i}, f k

Tactic:
rw [prod_singleton]

Premises used: Finset.prod_singleton
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst_3 : MulLeftStrictMono M
h : ∀ i ∈ s, 1 < f i
hs : s.Nonempty
rw rw₁ : LE.le.{u_4} (α := M) 1 1
⊢ LE.le.{u_4} (α := M) 1 (∏ i ∈ s, 1)

Tactic:
rw [prod_const_one]

Premises used: Finset.prod_const_one
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst_3 : MulLeftStrictMono M
h : ∀ i ∈ s, f i < 1
hs : s.Nonempty
rw rw₁ : LE.le.{u_4} (α := M) 1 1
⊢ LE.le.{u_4} (α := M) (∏ i ∈ s, 1) 1

Tactic:
rw [prod_const_one]

Premises used: Finset.prod_const_one
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst_3 : MulLeftStrictMono M
h : ∀ i ∈ s, 1 ≤ f i
hs : ∃ i ∈ s, 1 < f i
⊢ LT.lt.{u_4} (α := M) 1 (∏ i ∈ s, f i)

Tactic:
prod_const_one.symm.trans_lt <| prod_lt_prod' h hs

Premises used: Finset.prod_lt_prod', Finset.prod_const_one, Eq.trans_lt, Eq.symm
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s : Finset ι
inst_3 : MulLeftStrictMono M
h : ∀ i ∈ s, f i ≤ 1
hs : ∃ i ∈ s, f i < 1
⊢ LT.lt.{u_4} (α := M) (∏ i ∈ s, f i) 1

Tactic:
prod_const_one.le.trans_lt' <| prod_lt_prod' h hs

Premises used: Finset.prod_lt_prod', Eq.le, Finset.prod_const_one, LE.le.trans_lt'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ≤ g i
revert : ∀ (h : ∀ i ∈ s, f i ≤ g i), Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i
⊢ Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i

Tactic:
revert h
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
s : Finset ι
f g : ι → M
⊢ ∀ (h : ∀ i ∈ s, f i ≤ g i), Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i

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

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
s : Finset ι
f g : ι → M
refine :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih : ∀ (h : ∀ i ∈ s, f i ≤ g i), Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i)
    (H : ∀ i ∈ insert a s, f i ≤ g i),
    Eq.{u_10 + 1} (α := M) (∏ i ∈ insert a s, f i) (∏ i ∈ insert a s, g i) ↔ ∀ i ∈ insert a s, f i = g i
⊢ ∀ (h : ∀ i ∈ s, f i ≤ g i), Eq.{u_10 + 1} (α := M) (∏ 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.notMem_empty _ h),
      fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
s_1 : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
ih : ∀ (h : ∀ i ∈ s, f i ≤ g i), Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i
H : ∀ i ∈ insert a s, f i ≤ g i
⊢ Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i

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

Premises used: Function.comp, Finset.mem_insert_of_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
s_1 : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
H : ∀ i ∈ insert a s, f i ≤ g i
ih : Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i
rw : f a * ∏ x ∈ s, f x = g a * ∏ x ∈ s, g x ↔ f a = g a ∧ Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
⊢ Eq.{u_10 + 1} (α := M) (∏ 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]

Premises used: Finset.prod_insert, Finset.forall_mem_insert
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
s_1 : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
H : ∀ i ∈ insert a s, f i ≤ g i
ih : Eq.{u_10 + 1} (α := M) (∏ 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 ∧ Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)

Tactic:
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)

Premises used: Finset.prod_le_prod', Finset.mem_insert_self, Function.comp, Finset.mem_insert_of_mem, mul_eq_mul_iff_eq_and_eq
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
s_1 : Finset ι
f g : ι → M
a : ι
s : Finset ι
ha : a ∉ s
H : ∀ i ∈ insert a s, f i ≤ g i
ih : Eq.{u_10 + 1} (α := M) (∏ 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 ∧ Eq.{u_10 + 1} (α := M) (∏ 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)

Premises used: Finset.prod_le_prod', Finset.mem_insert_self, Function.comp, Finset.mem_insert_of_mem, mul_eq_mul_iff_eq_and_eq
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
s : Finset ι
f g : ι → M
h : ∀ i ∈ s, f i ≤ g i
revert : ∀ (h : ∀ i ∈ s, f i ≤ g i), Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i
revert₁ :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
    (ih : ∀ (h : ∀ i ∈ s, f i ≤ g i), Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i)
    (H : ∀ i ∈ insert a s, f i ≤ g i),
    Eq.{u_10 + 1} (α := M) (∏ i ∈ insert a s, f i) (∏ i ∈ insert a s, g i) ↔ ∀ i ∈ insert a s, f i = g i
revert₂ :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (H : ∀ i ∈ insert a s, f i ≤ g i)
    (ih : Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i),
    Eq.{u_10 + 1} (α := M) (∏ i ∈ insert a s, f i) (∏ i ∈ insert a s, g i) ↔ ∀ i ∈ insert a s, f i = g i
revert₃ :
  ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (H : ∀ i ∈ insert a s, f i ≤ g i)
    (ih : Eq.{u_10 + 1} (α := M) (∏ 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 ∧ Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
⊢ Eq.{u_10 + 1} (α := M) (∏ 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.notMem_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)

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : DecidableEq ι
rw : Disjoint (t \ s) (s ∩ t)
⊢ LE.le.{u_4} (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t \ s, f i) ↔ LE.le.{u_4} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, f i)

Tactic:
rw [← mul_le_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
    ← prod_union, inter_comm, sdiff_union_inter]

Premises used: mul_le_mul_iff_right, Finset.inter_comm, Finset.prod_union, Finset.disjoint_sdiff_inter, Finset.sdiff_union_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Preorder M
inst_2 : IsOrderedCancelMonoid M
f : ι → M
s t : Finset ι
inst_3 : DecidableEq ι
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
simpa only [inter_comm] using disjoint_sdiff_inter t s

Premises used: Finset.inter_comm, Finset.disjoint_sdiff_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
inst_3 : DecidableEq ι
s t : Finset ι
f : ι → M
rw : Disjoint (t \ s) (s ∩ t)
⊢ LT.lt.{u_10} (α := M) (∏ i ∈ s \ t, f i) (∏ i ∈ t \ s, f i) ↔ LT.lt.{u_10} (α := M) (∏ i ∈ s, f i) (∏ i ∈ t, f i)

Tactic:
rw [← mul_lt_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
    ← prod_union, inter_comm, sdiff_union_inter]

Premises used: Finset.inter_comm, Finset.prod_union, mul_lt_mul_iff_right, Finset.disjoint_sdiff_inter, Finset.sdiff_union_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : CommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedCancelMonoid M
inst_3 : DecidableEq ι
s t : Finset ι
f : ι → M
⊢ Disjoint (t \ s) (s ∩ t)

Tactic:
simpa only [inter_comm] using disjoint_sdiff_inter t s

Premises used: Finset.inter_comm, Finset.disjoint_sdiff_inter
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
f g : ι → M
s : Finset ι
inst_2 : MulLeftMono M
Hlt : LT.lt.{u_4} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
contrapose! : ∀ (Hle : ∀ (i : ι) (_ : i ∈ s), g i ≤ f i), LE.le.{u_4} (α := M) (∏ i ∈ s, g i) (∏ i ∈ s, f i)
⊢ ∃ i ∈ s, f i < g i

Tactic:
contrapose! Hlt with Hle
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
f g : ι → M
s : Finset ι
inst_2 : MulLeftMono M
Hle : ∀ (i : ι) (_ : i ∈ s), g i ≤ f i
⊢ LE.le.{u_4} (α := M) (∏ i ∈ s, g i) (∏ i ∈ s, f i)

Tactic:
prod_le_prod' Hle

Premises used: Finset.prod_le_prod'