awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
have 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
Tactic: refine ⟨fun h x y hsx hsy hfx hfy ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1 ↔ ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
have 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
Tactic: refine ⟨fun h x y hsx hsy hfx hfy ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (hypothesis)
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 ∧ f x = 1
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1
have pos : ∀ (hx : ∃ x ∈ s, f x ≠ 0), LE.le (α := ℕ) (∑ x ∈ s, f x) 1
Tactic: by_cases! hx : ∃ x ∈ s, f x ≠ 0
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1
have neg : ∀ (hx : ∀ (x : α) (_ : x ∈ s), f x = 0), LE.le (α := ℕ) (∑ x ∈ s, f x) 1
Tactic: by_cases! hx : ∃ x ∈ s, f x ≠ 0
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1
have pos : ∀ (x : α) (hsx : x ∈ s) (hfx : f x ≠ 0), LE.le (α := ℕ) (∑ x ∈ s, f x) 1
Tactic: obtain ⟨x, hsx, hfx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (hypothesis)
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
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1
have hs : ∀ y ∈ s \ {x}, f y = 0
Tactic: have hs : ∀ y ∈ s \ {x}, f y = 0 := by grind
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LE.le (α := ℕ) (∑ x ∈ s, f x) 1 ↔ ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LT.lt.{u_4} (α := M) 1 (∏ i : ι, f i) ↔ 1 < f
have inl : ∀ (hf : LE.le (α := ι → M) 1 1), LT.lt.{u_4} (α := M) 1 (∏ i : ι, 1 i) ↔ LT.lt (α := ι → M) 1 1
Tactic: obtain rfl | hf := hf.eq_or_lt
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LT.lt.{u_4} (α := M) 1 (∏ i : ι, f i) ↔ 1 < f
have inr : ∀ (hf : 1 < f), LT.lt.{u_4} (α := M) 1 (∏ i : ι, f i) ↔ 1 < f
Tactic: obtain rfl | hf := hf.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LT.lt.{u_4} (α := M) (∏ i : ι, f i) 1 ↔ f < 1
have inl : ∀ (hf : LE.le (α := ι → M) 1 1), LT.lt.{u_4} (α := M) (∏ i : ι, 1 i) 1 ↔ LT.lt (α := ι → M) 1 1
Tactic: obtain rfl | hf := hf.eq_or_lt
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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
⊢ LT.lt.{u_4} (α := M) (∏ i : ι, f i) 1 ↔ f < 1
have inr : ∀ (hf : f < 1), LT.lt.{u_4} (α := M) (∏ i : ι, f i) 1 ↔ f < 1
Tactic: obtain rfl | hf := hf.eq_or_lt
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
⊢ (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)
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (hypothesis)
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)
⊢ 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
have this : ∀ (x : β) (H : x ∈ i), x ≠ z
Tactic: have := fun x (H : x ∈ i) => ne_of_mem_of_not_mem H hz
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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 ↔
    (∀ a ∈ i, ¬a = z → Disjoint (f z) (f a)) ∧ (∀ x ∈ i, ¬x = z → Disjoint (f x) (f z)) ∧ i.sum f = i.sup f
have 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
Tactic: simp +contextual only [this, not_false_iff, true_imp_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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 ↔
    (∀ a ∈ i, Disjoint (f z) (f a)) ∧ (∀ x ∈ i, Disjoint (f x) (f z)) ∧ i.sum f = i.sup f
have cons : f z + ∑ x ∈ i, f x = f z ∪ i.sup f ↔ Disjoint (f z) (i.sum f) ∧ i.sum f = i.sup f
Tactic: simp_rw [← disjoint_finsetSum_left, ← disjoint_finsetSum_right, disjoint_comm, ← and_assoc,
      and_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq α
i : Finset β
f : β → Multiset α
⊢ i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
have empty : Finset.sum ∅ f = Finset.sup ∅ f ↔
  ∀ (x : β),
    Membership.mem (γ := Finset β) ∅ x → ∀ (y : β), Membership.mem (γ := Finset β) ∅ y → 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))
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
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)
⊢ i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
have 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)
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))
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
x : Multiset α
⊢ ((Finset.range (x.card + 1)).sup fun (k : ℕ) ↦ powersetCard k x) = x.powerset
have 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)
Tactic: convert! bind_powerset_len x using 1
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
m : Multiset α
⊢ m.card ≤ m.toFinset.card + 1 ↔ ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
have rw : (∀ (x y : α), x ∈ m.toFinset → y ∈ m.toFinset → count x m - 1 ≠ 0 → count y m - 1 ≠ 0 → x = y ∧ count x m - 1 = 1) ↔
  ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
Tactic: rw [← m.toFinset_sum_count_eq, m.toFinset.card_eq_sum_ones, ← tsub_le_iff_left,
    ← Finset.sum_tsub_distrib _ (by simp [one_le_count_iff_mem]), Finset.sum_le_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.Finset (goal)
Goal:
α : Type u_2
inst : DecidableEq α
m : Multiset α
⊢ (∀ (x y : α), x ∈ m.toFinset → y ∈ m.toFinset → count x m - 1 ≠ 0 → count y m - 1 ≠ 0 → x = y ∧ count x m - 1 = 1) ↔
    ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
have simp : (∀ (x y : α), x ∈ m → y ∈ m → 1 < count x m → 1 < count y m → x = y ∧ count x m = HAdd.hAdd (α := ℕ) 0 2) ↔
  ∀ (x y : α), 1 < count x m → 1 < count y m → x = y ∧ count x m = 2
Tactic: simp only [← pos_iff_ne_zero, Nat.sub_pos_iff_lt, mem_toFinset, Nat.pred_eq_succ_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
h : Forall₂ (fun (x1 x2 : M) ↦ x1 ≤ x2) l₁ l₂
⊢ l₁.prod ≤ l₂.prod
have nil : LE.le.{u_3} (α := M) (prod []) (prod [])
Tactic: induction h with
  | nil => rfl
  | cons hab ih ih' => simpa only [prod_cons] using mul_le_mul' hab ih'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
h : Forall₂ (fun (x1 x2 : M) ↦ x1 ≤ x2) l₁ l₂
nil : LE.le.{u_3} (α := M) (prod []) (prod [])
⊢ l₁.prod ≤ l₂.prod
have cons : ∀ {a b : M} {l₁ l₂ : List M} (hab : a ≤ b) (ih : Forall₂ (fun (x1 x2 : M) ↦ x1 ≤ x2) l₁ l₂) (ih' : l₁.prod ≤ l₂.prod),
  (a :: l₁).prod ≤ (b :: l₂).prod
Tactic: induction h with
  | nil => rfl
  | cons hab ih ih' => simpa only [prod_cons] using mul_le_mul' hab ih'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ l₁_1 l₂_1 : List M
a : M
h : l₁_1 <+ l₂_1
ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂_1 → 1 ≤ a), l₁_1.prod ≤ l₂_1.prod
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂_1 → 1 ≤ a_1
⊢ l₁_1.prod ≤ (a :: l₂_1).prod
have cons : ∀ (h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂_1 → 1 ≤ x), l₁_1.prod ≤ a * l₂_1.prod
Tactic: simp only [prod_cons, forall_mem_cons] at h₁ ⊢
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ l₁_1 l₂_1 : List M
a : M
h : l₁_1 <+ l₂_1
ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂_1 → 1 ≤ a), l₁_1.prod ≤ l₂_1.prod
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂_1 → 1 ≤ a_1
⊢ (a :: l₁_1).prod ≤ (a :: l₂_1).prod
have cons_cons : ∀ (h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂_1 → 1 ≤ x), a * l₁_1.prod ≤ a * l₂_1.prod
Tactic: simp only [prod_cons, forall_mem_cons] at h₁ ⊢
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ l₁_1 l₂_1 : List M
a : M
h : l₁_1 <+ l₂_1
ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂_1 → 1 ≤ a), l₁_1.prod ≤ l₂_1.prod
h₁ : 1 ≤ a ∧ ∀ (x : M), x ∈ l₂_1 → 1 ≤ x
⊢ a * l₁_1.prod ≤ a * l₂_1.prod
have cons_cons : a * l₂_1.prod ≤ a * l₂_1.prod
Tactic: grw [ih' h₁.2]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
h : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
⊢ l₁.prod ≤ l₂.prod
have slnil : ∀ (h₁ : ∀ (a : M), Membership.mem (γ := List M) [] a → 1 ≤ a), LE.le.{u_3} (α := M) (prod []) (prod [])
Tactic: induction h with
  | slnil => rfl
  | cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
  | cons_cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    grw [ih' h₁.2]
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
h : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
slnil : ∀ (h₁ : ∀ (a : M), Membership.mem (γ := List M) [] a → 1 ≤ a), LE.le.{u_3} (α := M) (prod []) (prod [])
⊢ l₁.prod ≤ l₂.prod
have cons : ∀ {l₁ l₂ : List M} (a : M),
  l₁ <+ l₂ →
    ∀ (ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a), l₁.prod ≤ l₂.prod) (h₁ : ∀ (a_2 : M), a_2 ∈ a :: l₂ → 1 ≤ a_2),
      l₁.prod ≤ (a :: l₂).prod
Tactic: induction h with
  | slnil => rfl
  | cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
  | cons_cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    grw [ih' h₁.2]
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l₁ l₂ : List M
h : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
slnil : ∀ (h₁ : ∀ (a : M), Membership.mem (γ := List M) [] a → 1 ≤ a), LE.le.{u_3} (α := M) (prod []) (prod [])
cons :
  ∀ {l₁ l₂ : List M} (a : M),
    l₁ <+ l₂ →
      ∀ (ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a), l₁.prod ≤ l₂.prod) (h₁ : ∀ (a_2 : M), a_2 ∈ a :: l₂ → 1 ≤ a_2),
        l₁.prod ≤ (a :: l₂).prod
⊢ l₁.prod ≤ l₂.prod
have cons_cons : ∀ {l₁ l₂ : List M} (a : M),
  l₁ <+ l₂ →
    ∀ (ih' : ∀ (h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a), l₁.prod ≤ l₂.prod) (h₁ : ∀ (a_2 : M), a_2 ∈ a :: l₂ → 1 ≤ a_2),
      (a :: l₁).prod ≤ (a :: l₂).prod
Tactic: induction h with
  | slnil => rfl
  | cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
  | cons_cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    grw [ih' h₁.2]
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₁ : ∀ (i_1 : ι), i_1 ∈ i :: l → f i_1 ≤ g i_1
h₂ : ∃ (i_1 : ι), i_1 ∈ i :: l ∧ f i_1 < g i_1
⊢ (map f (i :: l)).prod < (map g (i :: l)).prod
have cons : ∀ (h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x), f i * (map f l).prod < g i * (map g l).prod
Tactic: simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₂ : ∃ (i_1 : ι), i_1 ∈ i :: l ∧ f i_1 < g i_1
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
⊢ f i * (map f l).prod < g i * (map g l).prod
have h₃ : f i < g i ∨ ∃ (a : ι), a ∈ l ∧ f a < g a
Tactic: simp only [mem_cons, exists_eq_or_imp] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h₂ : f i < g i ∨ ∃ (a : ι), a ∈ l ∧ f a < g a
⊢ f i * (map f l).prod < g i * (map g l).prod
have cons : f i < g i → f i * (map f l).prod < g i * (map g l).prod
Tactic: cases h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
f g : ι → M
i : ι
l : List ι
ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod
h₁ : f i ≤ g i ∧ ∀ (x : ι), x ∈ l → f x ≤ g x
h₂ : f i < g i ∨ ∃ (a : ι), a ∈ l ∧ f a < g a
cons : f i < g i → f i * (map f l).prod < g i * (map g l).prod
⊢ f i * (map f l).prod < g i * (map g l).prod
have cons₁ : (∃ (a : ι), a ∈ l ∧ f a < g a) → f i * (map f l).prod < g i * (map g l).prod
Tactic: cases h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
l : List ι
f g : ι → M
h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i
h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i
⊢ (map f l).prod < (map g l).prod
have nil : ∀ (h₁ : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ≤ g i)
  (h₂ : ∃ (i : ι), Membership.mem (γ := List ι) [] i ∧ f i < g i), (map f []).prod < (map g []).prod
Tactic: induction l with
  | nil => simp at h₂
  | cons i l ihl =>
    simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢
    simp only [mem_cons, exists_eq_or_imp] at h₂
    cases h₂
    · exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
    · exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›
Cleared hypotheses: l, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : Preorder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
l : List ι
f g : ι → M
h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i
h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i
nil :
  ∀ (h₁ : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ≤ g i)
    (h₂ : ∃ (i : ι), Membership.mem (γ := List ι) [] i ∧ f i < g i), (map f []).prod < (map g []).prod
⊢ (map f l).prod < (map g l).prod
have cons : ∀ (i : ι) (l : List ι)
  (ihl : ∀ (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i), (map f l).prod < (map g l).prod)
  (h₁ : ∀ (i_1 : ι), i_1 ∈ i :: l → f i_1 ≤ g i_1) (h₂ : ∃ (i_1 : ι), i_1 ∈ i :: l ∧ f i_1 < g i_1),
  (map f (i :: l)).prod < (map g (i :: l)).prod
Tactic: induction l with
  | nil => simp at h₂
  | cons i l ihl =>
    simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢
    simp only [mem_cons, exists_eq_or_imp] at h₂
    cases h₂
    · exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
    · exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›
Cleared hypotheses: l, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulRightMono M
inst_3 : MulLeftMono M
l : List ι
f g : ι → M
h : (map f l).prod < (map g l).prod
⊢ ∃ (i : ι), i ∈ l ∧ f i < g i
have contrapose! : ∀ (h : ∀ (i : ι) (_ : i ∈ l), g i ≤ f i), (map g l).prod ≤ (map f l).prod
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Group.List (goal)
Goal:
ι : Type u_1
M : Type u_3
inst : Monoid M
inst_1 : LinearOrder M
inst_2 : MulLeftStrictMono M
inst_3 : MulLeftMono M
inst_4 : MulRightStrictMono M
inst_5 : MulRightMono M
l : List ι
hl : l ≠ []
f g : ι → M
h : (map f l).prod ≤ (map g l).prod
⊢ ∃ (x : ι), x ∈ l ∧ f x ≤ g x
have contrapose! : ∀ (h : ∀ (x : ι) (_ : x ∈ l), g x < f x), (map g l).prod < (map f l).prod
Tactic: contrapose! h
Cleared hypotheses: h