awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact prod_le_prod' Hle

Premises used: Finset.prod_le_prod'
-- 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 : IsOrderedCancelMonoid M
hs : s.Nonempty
Hle : LE.le.{u_4} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
contrapose! : ∀ (Hlt : ∀ (i : ι) (_ : i ∈ s), g i < f i), LT.lt.{u_4} (α := M) (∏ i ∈ s, g i) (∏ i ∈ s, f i)
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
contrapose! Hle with Hlt
-- 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 : IsOrderedCancelMonoid M
hs : s.Nonempty
Hlt : ∀ (i : ι) (_ : i ∈ s), g i < f i
⊢ LT.lt.{u_4} (α := M) (∏ i ∈ s, g i) (∏ i ∈ s, f i)

Tactic:
prod_lt_prod_of_nonempty' hs Hlt

Premises used: Finset.prod_lt_prod_of_nonempty'
-- 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 : IsOrderedCancelMonoid M
hs : s.Nonempty
Hlt : ∀ (i : ι) (_ : i ∈ s), g i < f i
⊢ LT.lt.{u_4} (α := M) (∏ i ∈ s, g i) (∏ i ∈ s, f i)

Tactic:
exact prod_lt_prod_of_nonempty' hs Hlt

Premises used: Finset.prod_lt_prod_of_nonempty'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
s : Finset ι
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h₁ : Eq.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1
h₂ : ∃ i ∈ s, f i ≠ 1
contrapose! : ∀ (h₁ : ∀ (i : ι) (_ : i ∈ s), f i ≤ 1), Ne.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1
⊢ ∃ i ∈ s, 1 < f i

Tactic:
contrapose! h₁
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
s : Finset ι
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h₂ : ∃ i ∈ s, f i ≠ 1
h₁ : ∀ (i : ι) (_ : i ∈ s), f i ≤ 1
⊢ ∃ i ∈ s, f i ≠ 1

Tactic:
h₂
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
s : Finset ι
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h₂ : ∃ i ∈ s, f i ≠ 1
h₁ : ∀ (i : ι) (_ : i ∈ s), f i ≤ 1
obtain : ∀ (i : ι) (m : i ∈ s) (i_ne : f i ≠ 1), Ne.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1
⊢ Ne.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1

Tactic:
obtain ⟨i, m, i_ne⟩ : ∃ i ∈ s, f i ≠ 1 := h₂
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
s : Finset ι
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h₁ : ∀ (i : ι) (_ : i ∈ s), f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
h : LT.lt.{u_4} (α := M) (∏ i ∈ s, f i) 1
⊢ Ne.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1

Tactic:
apply ne_of_lt

Premises used: ne_of_lt
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
s : Finset ι
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h₁ : ∀ (i : ι) (_ : i ∈ s), f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ s, 1)

Tactic:
prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩

Premises used: Finset.prod_lt_prod', LE.le.lt_of_ne, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : LinearOrder M
s : Finset ι
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h₁ : ∀ (i : ι) (_ : i ∈ s), f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ Eq.{u_4 + 1} (α := M) (∏ j ∈ s, 1) 1

Tactic:
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 : LinearOrder M
s : Finset ι
inst_2 : IsOrderedCancelMonoid M
f : ι → M
h₁ : ∀ (i : ι) (_ : i ∈ s), f i ≤ 1
i : ι
m : i ∈ s
i_ne : f i ≠ 1
⊢ LT.lt.{u_4} (α := M) (∏ i ∈ s, f i) 1

Tactic:
calc
    ∏ j ∈ s, f j < ∏ j ∈ s, 1 := prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
    _ = 1 := prod_const_one

Premises used: Finset.prod_lt_prod', LE.le.lt_of_ne, Finset.prod_const_one, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t : Finset ι
⊢ f (t.sup s) ≤ ∑ i ∈ t, f (s i)

Tactic:
t.induction_on zero.le fun i t it h ↦ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t : Finset ι
refine :
  ∀ (i : ι) (t : Finset ι) (it : i ∉ t) (h : f (t.sup s) ≤ ∑ i ∈ t, f (s i)),
    f ((insert i t).sup s) ≤ ∑ i ∈ insert i t, f (s i)
⊢ f (t.sup s) ≤ ∑ i ∈ t, f (s i)

Tactic:
refine t.induction_on zero.le fun i t it h ↦ ?_
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t_1 : Finset ι
i : ι
t : Finset ι
it : i ∉ t
h : f (t.sup s) ≤ ∑ i ∈ t, f (s i)
⊢ f (s i) + f (t.sup s) ≤ f (s i) + ∑ i ∈ t, f (s i)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t_1 : Finset ι
i : ι
t : Finset ι
it : i ∉ t
h : f (t.sup s) ≤ ∑ i ∈ t, f (s i)
⊢ f ((insert i t).sup s) ≤ ∑ i ∈ insert i t, f (s i)

Tactic:
simpa only [sup_insert, Finset.sum_insert it] using ih.trans (by gcongr)

Premises used: Finset.sup_insert, LE.le.trans, Finset.sum_insert
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : SemilatticeSup α
inst_1 : OrderBot α
inst_2 : AddCommMonoid β
inst_3 : Preorder β
inst_4 : AddLeftMono β
f : α → β
zero : f ⊥ = 0
ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t
s : ι → α
t : Finset ι
refine :
  ∀ (i : ι) (t : Finset ι) (it : i ∉ t) (h : f (t.sup s) ≤ ∑ i ∈ t, f (s i)),
    f ((insert i t).sup s) ≤ ∑ i ∈ insert i t, f (s i)
⊢ f (t.sup s) ≤ ∑ i ∈ t, f (s i)

Tactic:
classical
  refine t.induction_on zero.le fun i t it h ↦ ?_
  simpa only [sup_insert, Finset.sum_insert it] using ih.trans (by gcongr)

Premises used: Finset.sup_insert, LE.le.trans
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid β
inst_1 : Preorder β
inst_2 : AddLeftMono β
f : Set α → β
zero : f ∅ = 0
ih : ∀ {s t : Set α}, f (s ∪ t) ≤ f s + f t
s : ι → Set α
t : Finset ι
⊢ ∀ {s t : Set α}, f (s ⊔ t) ≤ f s + f t

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1 ↔ ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1

Tactic:
⟨fun h x y hsx hsy hfx hfy ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
refine_1 :
  ∀ (h : LE.le (α := ℕ) (∑ x ∈ s, f x) 1) (x y : α) (hsx : x ∈ s) (hsy : y ∈ s) (hfx : f x ≠ 0) (hfy : f y ≠ 0),
    x = y ∧ f x = 1
refine_2 : ∀ (h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1), LE.le (α := ℕ) (∑ x ∈ s, f x) 1
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1 ↔ ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1

Tactic:
refine ⟨fun h x y hsx hsy hfx hfy ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
h : LE.le (α := ℕ) (∑ x ∈ s, f x) 1
x y : α
hsx : x ∈ s
hsy : y ∈ s
hfx : f x ≠ 0
hfy : f y ≠ 0
⊢ {x, y} ⊆ s

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
h : LE.le (α := ℕ) (∑ x ∈ s, f x) 1
x y : α
hsx : x ∈ s
hsy : y ∈ s
hfx : f x ≠ 0
hfy : f y ≠ 0
⊢ LE.le (α := ℕ) ((fun (s : Finset α) ↦ (∑ x ∈ s, f x : ℕ)) {x, y}) 1

Tactic:
replace h := (sum_mono_set f (show {x, y} ⊆ s by grind)).trans h
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
x y : α
hsx : x ∈ s
hsy : y ∈ s
hfx : f x ≠ 0
hfy : f y ≠ 0
h : LE.le (α := ℕ) ((fun (s : Finset α) ↦ (∑ x ∈ s, f x : ℕ)) {x, y}) 1
⊢ x = y ∧ f x = 1

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
pos : ∀ (hx : ∃ x ∈ s, f x ≠ 0), LE.le (α := ℕ) (∑ x ∈ s, f x) 1
neg : ∀ (hx : ∀ (x : α) (_ : x ∈ s), f x = 0), LE.le (α := ℕ) (∑ x ∈ s, f x) 1
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1

Tactic:
by_cases! hx : ∃ x ∈ s, f x ≠ 0
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
hx : ∃ x ∈ s, f x ≠ 0
pos : ∀ (x : α) (hsx : x ∈ s) (hfx : f x ≠ 0), LE.le (α := ℕ) (∑ x ∈ s, f x) 1
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1

Tactic:
obtain ⟨x, hsx, hfx⟩ := hx
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
x : α
hsx : x ∈ s
hfx : f x ≠ 0
⊢ ∀ y ∈ s \ {x}, f y = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
x : α
hsx : x ∈ s
hfx : f x ≠ 0
⊢ ∀ y ∈ s \ {x}, f y = 0

Tactic:
have hs : ∀ y ∈ s \ {x}, f y = 0 := by grind
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
x : α
hsx : x ∈ s
hfx : f x ≠ 0
hs : ∀ y ∈ s \ {x}, f y = 0
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1

Tactic:
simp [← sum_sdiff (singleton_subset_iff.2 hsx), sum_congr rfl hs, (h x x hsx hsx hfx hfx).2]

Premises used: Iff.mpr, Finset.singleton_subset_iff, And.right, Finset.sum_congr, rfl, Finset.sum_sdiff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
hx : ∀ (x : α) (_ : x ∈ s), f x = 0
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1

Tactic:
simp [sum_congr rfl hx]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
s : Finset α
f : α → ℕ
refine_1 :
  ∀ (h : LE.le (α := ℕ) (∑ x ∈ s, f x) 1) (x y : α) (hsx : x ∈ s) (hsy : y ∈ s) (hfx : f x ≠ 0) (hfy : f y ≠ 0),
    x = y ∧ f x = 1
refine_2 refine_2₁ :
  ∀ (h : ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1), LE.le (α := ℕ) (∑ x ∈ s, f x) 1
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1 ↔ ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1

Tactic:
classical
  refine ⟨fun h x y hsx hsy hfx hfy ↦ ?_, fun h ↦ ?_⟩
  · replace h := (sum_mono_set f (show {x, y} ⊆ s by grind)).trans h
    grind
  · by_cases! hx : ∃ x ∈ s, f x ≠ 0
    · obtain ⟨x, hsx, hfx⟩ := hx
      have hs : ∀ y ∈ s \ {x}, f y = 0 := by grind
      simp [← sum_sdiff (singleton_subset_iff.2 hsx), sum_congr rfl hs, (h x x hsx hsx hfx hfx).2]
    · simp [sum_congr rfl hx]
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Preorder M
inst_3 : MulLeftMono M
⊢ Monotone (β := M) fun (f : ι → M) ↦ ∏ i : ι, f i

Tactic:
fun _ _ hfg ↦
  Finset.prod_le_prod' fun x _ ↦ hfg x

Premises used: Finset.prod_le_prod', Monotone
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Preorder M
inst_3 : MulLeftMono M
f : ι → M
hf : 1 ≤ f
⊢ LE.le.{u_4} (α := M) 1 (∏ i : ι, f i)

Tactic:
Finset.one_le_prod' fun _ _ ↦ hf _

Premises used: Finset.one_le_prod'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : Preorder M
inst_3 : MulLeftMono M
f : ι → M
hf : f ≤ 1
⊢ LE.le.{u_4} (α := M) (∏ i : ι, f i) 1

Tactic:
Finset.prod_le_one' fun _ _ ↦ hf _

Premises used: Finset.prod_le_one'
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : MulLeftMono M
f : ι → M
hf : 1 ≤ f
⊢ (∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → f i = 1) ↔ f = 1

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_9
M : Type u_10
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : MulLeftMono M
f : ι → M
hf : f ≤ 1
⊢ (∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → f i = 1) ↔ f = 1

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelMonoid M
⊢ StrictMono (β := M) fun (f : ι → M) ↦ ∏ x : ι, f x

Tactic:
fun _ _ hfg ↦
  let ⟨hle, i, hlt⟩ := Pi.lt_def.mp hfg
  Finset.prod_lt_prod' (fun i _ ↦ hle i) ⟨i, Finset.mem_univ i, hlt⟩

Premises used: Finset.mem_univ, StrictMono, Finset.univ, Pi.lt_def, Finset.prod_lt_prod', Finset.prod, _private.0.Fintype.prod_strictMono'.match_1, And.intro, LT.lt, Exists.intro, Iff.mp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelMonoid M
f : ι → M
hf : 1 < f
⊢ ∃ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i ∧ 1 < f i

Tactic:
simpa using (Pi.lt_def.1 hf).2

Premises used: Pi.lt_def, And.right, Iff.mp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelMonoid M
f : ι → M
hf : f < 1
⊢ ∃ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i ∧ f i < 1

Tactic:
simpa using (Pi.lt_def.1 hf).2

Premises used: Pi.lt_def, And.right, Iff.mp
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelMonoid M
f : ι → M
hf : 1 ≤ f
inl : ∀ (hf : LE.le (α := ι → M) 1 1), LT.lt.{u_4} (α := M) 1 (∏ i : ι, 1 i) ↔ LT.lt (α := ι → M) 1 1
inr : ∀ (hf : 1 < f), LT.lt.{u_4} (α := M) 1 (∏ i : ι, f i) ↔ 1 < f
⊢ LT.lt.{u_4} (α := M) 1 (∏ i : ι, f i) ↔ 1 < f

Tactic:
obtain rfl | hf := hf.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelMonoid M
hf : LE.le (α := ι → M) 1 1
⊢ LT.lt.{u_4} (α := M) 1 (∏ i : ι, 1 i) ↔ LT.lt (α := ι → M) 1 1

Tactic:
simp [*, one_lt_prod]

Premises used: Fintype.one_lt_prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelMonoid M
f : ι → M
hf_1 : 1 ≤ f
hf : 1 < f
⊢ LT.lt.{u_4} (α := M) 1 (∏ i : ι, f i) ↔ 1 < f

Tactic:
simp [*, one_lt_prod]

Premises used: Fintype.one_lt_prod
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelMonoid M
f : ι → M
hf : f ≤ 1
inl : ∀ (hf : LE.le (α := ι → M) 1 1), LT.lt.{u_4} (α := M) (∏ i : ι, 1 i) 1 ↔ LT.lt (α := ι → M) 1 1
inr : ∀ (hf : f < 1), LT.lt.{u_4} (α := M) (∏ i : ι, f i) 1 ↔ f < 1
⊢ LT.lt.{u_4} (α := M) (∏ i : ι, f i) 1 ↔ f < 1

Tactic:
obtain rfl | hf := hf.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelMonoid M
hf : LE.le (α := ι → M) 1 1
⊢ LT.lt.{u_4} (α := M) (∏ i : ι, 1 i) 1 ↔ LT.lt (α := ι → M) 1 1

Tactic:
simp [*, prod_lt_one]

Premises used: Fintype.prod_lt_one
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
ι : Type u_1
M : Type u_4
inst : Fintype ι
inst_1 : CommMonoid M
inst_2 : PartialOrder M
inst_3 : IsOrderedCancelMonoid M
f : ι → M
hf_1 : f ≤ 1
hf : f < 1
⊢ LT.lt.{u_4} (α := M) (∏ i : ι, f i) 1 ↔ f < 1

Tactic:
simp [*, prod_lt_one]

Premises used: Fintype.prod_lt_one
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : β → Multiset α
⊢ Finset.sum ∅ f = Finset.sup ∅ f ↔
    ∀ (x : β),
      Membership.mem (γ := Finset β) ∅ x → ∀ (y : β), Membership.mem (γ := Finset β) ∅ y → x ≠ y → Disjoint (f x) (f y)

Tactic:
simp only [Finset.notMem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty,
      Finset.sup_empty, bot_eq_zero]

Premises used: Finset.sup_empty, Multiset.bot_eq_zero, imp_true_iff, Finset.notMem_empty, Finset.sum_empty, IsEmpty.forall_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
cons :
  f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f
⊢ (Finset.cons z i hz).sum f = (Finset.cons z i hz).sup f ↔
    ∀ x ∈ Finset.cons z i hz, ∀ y ∈ Finset.cons z i hz, x ≠ y → Disjoint (f x) (f y)

Tactic:
simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union,
      forall_eq_or_imp, Ne, not_true_eq_false, IsEmpty.forall_iff, true_and,
      imp_and, forall_and, ← hr, @eq_comm _ z]

Premises used: Multiset.sup_eq_union, imp_and, Finset.sum_cons, not_true_eq_false, Ne, forall_eq_or_imp, eq_comm, Finset.sup_cons, Finset.mem_cons, true_and, IsEmpty.forall_iff, forall_and
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
⊢ ∀ (x : β) (H : x ∈ i), x ≠ z

Tactic:
have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ (x : β) (H : x ∈ i), x ≠ z
cons :
  f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, Disjoint (f z) (f a)) ∧ (∀ x ∈ i, Disjoint (f x) (f z)) ∧ i.sum f = i.sup f
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Tactic:
simp +contextual only [this, not_false_iff, true_imp_iff]

Premises used: true_imp_iff, not_false_iff
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ (x : β) (H : x ∈ i), x ≠ z
cons : f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ Disjoint (f z) (i.sum f) ∧ i.sum f = i.sup f
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔
    (∀ a ∈ i, Disjoint (f z) (f a)) ∧ (∀ x ∈ i, Disjoint (f x) (f z)) ∧ i.sum f = i.sup f

Tactic:
simp_rw [← disjoint_finsetSum_left, ← disjoint_finsetSum_right, disjoint_comm, ← and_assoc,
      and_self_iff]

Premises used: disjoint_comm, and_assoc, and_self_iff, Multiset.disjoint_finsetSum_right, Multiset.disjoint_finsetSum_left
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ (x : β) (H : x ∈ i), x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ Disjoint (f z) (i.sum f) ∧ i.sum f = i.sup f

Tactic:
add_eq_union_left_of_le (Finset.sup_le fun x hx => le_sum_of_mem (mem_map_of_mem f hx))

Premises used: Multiset.mem_map_of_mem, Finset.sup_le, Multiset.add_eq_union_left_of_le, Multiset.le_sum_of_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
f : β → Multiset α
z : β
i : Finset β
hz : z ∉ i
hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
this : ∀ (x : β) (H : x ∈ i), x ≠ z
⊢ f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ Disjoint (f z) (i.sum f) ∧ i.sum f = i.sup f

Tactic:
exact add_eq_union_left_of_le (Finset.sup_le fun x hx => le_sum_of_mem (mem_map_of_mem f hx))

Premises used: Multiset.mem_map_of_mem, Finset.sup_le, Multiset.add_eq_union_left_of_le, Multiset.le_sum_of_mem
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
i : Finset β
f : β → Multiset α
empty :
  Finset.sum ∅ f = Finset.sup ∅ f ↔
    ∀ (x : β),
      Membership.mem (γ := Finset β) ∅ x → ∀ (y : β), Membership.mem (γ := Finset β) ∅ y → x ≠ y → Disjoint (f x) (f y)
cons :
  ∀ (z : β) (i : Finset β) (hz : z ∉ i) (hr : i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)),
    (Finset.cons z i hz).sum f = (Finset.cons z i hz).sup f ↔
      ∀ x ∈ Finset.cons z i hz, ∀ y ∈ Finset.cons z i hz, x ≠ y → Disjoint (f x) (f y)
⊢ i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)

Tactic:
induction i using Finset.cons_induction_on with
  | empty =>
    simp only [Finset.notMem_empty, IsEmpty.forall_iff, imp_true_iff, Finset.sum_empty,
      Finset.sup_empty, bot_eq_zero]
  | cons z i hz hr =>
    simp_rw [Finset.sum_cons hz, Finset.sup_cons, Finset.mem_cons, Multiset.sup_eq_union,
      forall_eq_or_imp, Ne, not_true_eq_false, IsEmpty.forall_iff, true_and,
      imp_and, forall_and, ← hr, @eq_comm _ z]
    have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz
    simp +contextual only [this, not_false_iff, true_imp_iff]
    simp_rw [← disjoint_finsetSum_left, ← disjoint_finsetSum_right, disjoint_comm, ← and_assoc,
      and_self_iff]
    exact add_eq_union_left_of_le (Finset.sup_le fun x hx => le_sum_of_mem (mem_map_of_mem f hx))

Premises used: Multiset.sup_eq_union, imp_and, disjoint_comm, Finset.sup_empty, not_true_eq_false, Multiset.mem_map_of_mem, Multiset.cons, Ne, forall_eq_or_imp, Multiset.bot_eq_zero, Finset.sup_le, imp_true_iff, Finset.notMem_empty, true_imp_iff, and_assoc, Finset.sup_cons, Finset.sum_empty, and_self_iff, not_false_iff, Finset.mem_cons, Multiset.add_eq_union_left_of_le, Multiset.le_sum_of_mem, Multiset.disjoint_finsetSum_right, true_and, IsEmpty.forall_iff, forall_and, Multiset.disjoint_finsetSum_left
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
x : Multiset α
⊢ ((range (x.card + 1)).bind fun (k : ℕ) ↦ powersetCard k x) = x.powerset

Tactic:
bind_powerset_len x

Premises used: Multiset.bind_powerset_len
-- Module: Mathlib.Algebra.Order.BigOperators.Group.Finset
Goal:
α : Type u_2
inst : DecidableEq α
x : Multiset α
h :
  Eq.{u_2 + 1} (α := Multiset (Multiset α)) ((Finset.range (x.card + 1)).sup fun (k : ℕ) ↦ powersetCard k x)
    ((range (x.card + 1)).bind fun (k : ℕ) ↦ powersetCard k x)
⊢ ((Finset.range (x.card + 1)).sup fun (k : ℕ) ↦ powersetCard k x) = x.powerset

Tactic:
convert! bind_powerset_len x using 1

Premises used: Multiset.bind_powerset_len