awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s : Set ι).PairwiseDisjoint f
⊢ #s ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
have rw : #({a ∈ s | ¬f a = ∅}) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
Tactic: rw [← Finset.card_filter_add_card_filter_not fun i ↦ f i = ∅, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s : Set ι).PairwiseDisjoint f
⊢ #({a ∈ s | ¬f a = ∅}) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
have grw : #({i ∈ s | f i ≠ ∅}.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
Tactic: grw [card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
    nonempty_of_ne_empty (mem_filter.1 hi).2, filter_subset]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hs : (↑s : Set ι).PairwiseDisjoint f
grw : #({i ∈ s | f i ≠ ∅}.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
⊢ #({a ∈ s | ¬f a = ∅}) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
have grw₁ : #(s.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(s.biUnion f) + #({i ∈ s | f i = ∅})
Tactic: grw [card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
    nonempty_of_ne_empty (mem_filter.1 hi).2, filter_subset]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : DecidableEq α
s : Finset ι
f : ι → Finset α
hf : Injective f
hs : (↑s : Set ι).PairwiseDisjoint f
⊢ #s ≤ #(s.biUnion f) + 1
have grw : #(s.biUnion f) + #({i ∈ s | f i = ∅}) ≤ #(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]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ #s ≤ #(s.biUnion f) + 1
have grw₁ : #(s.biUnion f) + 1 ≤ #(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]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (hypothesis)
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
⊢ LE.le.{u_4} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, f x)
have this : IsOrderedMonoid M
Tactic: have := CanonicallyOrderedMul.toIsOrderedMonoid (α := M)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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 = HMul.hMul (α := M) (∏ x ∈ s with f x = 1, f x) (∏ x ∈ s with f x ≠ 1, f x)
have rw : Disjoint ({x ∈ s | f x = 1}) ({x ∈ s | f x ≠ 1})
Tactic: rw [← prod_union, filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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 ∈ {x ∈ s | f x = 1}, f i ≤ 1
have simp : ∀ i ∈ s, f i = 1 → f i ≤ 1
Tactic: simp only [mem_filter, and_imp]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le.{u_4} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, f x)
have x : ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s with f x = 1, f x) (∏ x ∈ s with f x ≠ 1, 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])
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le.{u_4} (α := M) (∏ x ∈ s, f x) (∏ x ∈ t, f x)
have classical : ∏ x ∈ s, f x = HMul.hMul (α := M) (∏ x ∈ s with f x = 1, f x) (∏ x ∈ s with f x ≠ 1, 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])
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ insert i s, f j)
have rw : ∏ j ∈ s, f j < f i * ∏ x ∈ s, f x
Tactic: rw [prod_insert hs]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le.{u_4} (α := M) (∏ j ∈ insert i s, f j) (∏ j ∈ t, f j)
have h₁ : insert i s ⊆ t
Tactic: apply prod_le_prod_of_subset_of_one_le'
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le.{u_4} (α := M) (∏ j ∈ insert i s, f j) (∏ j ∈ t, f j)
have hf : ∀ i_1 ∈ t, i_1 ∉ insert i s → 1 ≤ f i_1
Tactic: apply prod_le_prod_of_subset_of_one_le'
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (hypothesis)
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
⊢ 1 ≤ f x
have h'x₁ : ¬x = i ∧ x ∉ s
Tactic: simp only [mem_insert, not_or] at h'x
Cleared hypotheses: h'x
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ t, f j)
have j : LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ insert i s, 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
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
⊢ LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ t, f j)
have j₁ : LE.le.{u_4} (α := M) (∏ j ∈ insert i 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
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ t, f j)
have classical : LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ insert i s, 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
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
⊢ LT.lt.{u_4} (α := M) (∏ j ∈ s, f j) (∏ j ∈ t, f j)
have classical₁ : LE.le.{u_4} (α := M) (∏ j ∈ insert i 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
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ f i = ∏ k ∈ {i}, f k
have rw : f i = f i
Tactic: rw [prod_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le.{u_4} (α := M) 1 (∏ i ∈ s, 1)
have rw : LE.le.{u_4} (α := M) 1 1
Tactic: rw [prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le.{u_4} (α := M) (∏ i ∈ s, 1) 1
have rw : LE.le.{u_4} (α := M) 1 1
Tactic: rw [prod_const_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
have 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
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
have 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
Tactic: refine Finset.induction_on s (fun _ ↦ ⟨fun _ _ h ↦ False.elim (Finset.notMem_empty _ h),
      fun _ ↦ rfl⟩) fun a s ha ih H ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (hypothesis)
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 ∈ insert a s, f i) (∏ i ∈ insert a s, g i) ↔ ∀ i ∈ insert a s, f i = g i
have ih₁ : 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
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ 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
have 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)
Tactic: rw [Finset.prod_insert ha, Finset.prod_insert ha, Finset.forall_mem_insert, ← ih]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
have 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
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
have 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
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i
have 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
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ Eq.{u_10 + 1} (α := M) (∏ i ∈ s, f i) (∏ i ∈ s, g i) ↔ ∀ i ∈ s, f i = g i
have 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)
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)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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 ι
⊢ 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)
have rw : Disjoint (t \ s) (s ∩ t)
Tactic: rw [← mul_le_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
    ← prod_union, inter_comm, sdiff_union_inter]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ 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)
have rw : Disjoint (t \ s) (s ∩ t)
Tactic: rw [← mul_lt_mul_iff_right, ← prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter,
    ← prod_union, inter_comm, sdiff_union_inter]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
⊢ ∃ i ∈ s, f i < g i
have contrapose! : ∀ (Hle : ∀ (i : ι) (_ : i ∈ s), g i ≤ f i), LE.le.{u_4} (α := M) (∏ i ∈ s, g i) (∏ i ∈ s, f i)
Tactic: contrapose! Hlt with Hle
Cleared hypotheses: Hlt
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
⊢ ∃ i ∈ s, f i ≤ g i
have contrapose! : ∀ (Hlt : ∀ (i : ι) (_ : i ∈ s), g i < f i), LT.lt.{u_4} (α := M) (∏ i ∈ s, g i) (∏ i ∈ s, f i)
Tactic: contrapose! Hle with Hlt
Cleared hypotheses: Hle
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ ∃ i ∈ s, 1 < f i
have contrapose! : ∀ (h₁ : ∀ (i : ι) (_ : i ∈ s), f i ≤ 1), Ne.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1
Tactic: contrapose! h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ Ne.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1
have obtain : ∀ (i : ι) (m : i ∈ s) (i_ne : 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₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ Ne.{u_4 + 1} (α := M) (∏ i ∈ s, f i) 1
have h : LT.lt.{u_4} (α := M) (∏ i ∈ s, f i) 1
Tactic: apply ne_of_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
have 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)
Tactic: refine t.induction_on zero.le fun i t it h ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
have 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)
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)