awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
inst_2 : Nonempty ι
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : x ∉ ⋂ (i : ι), s i
⊢ ∃ (x_1 : ι), x ∉ s x_1

Tactic:
simp only [mem_iInter, not_forall] at hx

Premises used: Set.mem_iInter, Classical.not_forall
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
inst_2 : Nonempty ι
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
hx : ∃ (x_1 : ι), x ∉ s x_1
neg : ∀ (j : ι) (hj : x ∉ s j), Eq.{u_3 + 1} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)
⊢ Eq.{u_3 + 1} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)

Tactic:
rcases hx with ⟨j, hj⟩
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
inst_2 : Nonempty ι
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ LE.le.{u_3} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)

Tactic:
simp only [← h1, le_iInf_iff, bot_le, forall_const]

Premises used: le_iInf_iff, forall_const, bot_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
inst_2 : Nonempty ι
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
neg : LE.le.{u_3} (α := M) (⨅ (i : ι), (s i).mulIndicator f x) 1
⊢ Eq.{u_3 + 1} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)

Tactic:
refine le_antisymm (by simp only [← h1, le_iInf_iff, bot_le, forall_const]) ?_

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
ι : Sort u_1
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
inst_2 : Nonempty ι
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
s : ι → Set α
f : α → M
x : α
j : ι
hj : x ∉ s j
⊢ LE.le.{u_3} (α := M) (⨅ (i : ι), (s i).mulIndicator f x) 1

Tactic:
simpa [mulIndicator_of_notMem hj] using (iInf_le (fun i ↦ (s i).mulIndicator f) j) x

Premises used: Set.mulIndicator, Set.mulIndicator_of_notMem, iInf_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
simp :
  (∀ (i : ι), (s i).mulIndicator (f i) ≤ mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i)) ∧
    LE.le (α := (x : α) → M) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i)) (⨆ (i : ι), (s i).mulIndicator (f i))
⊢ Eq (α := (x : α) → M) (⨆ (i : ι), (s i).mulIndicator (f i)) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i))

Tactic:
simp only [le_antisymm_iff, iSup_le_iff]

Premises used: le_antisymm_iff, iSup_le_iff
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
⊢ (∀ (i : ι), (s i).mulIndicator (f i) ≤ mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i)) ∧
    LE.le (α := (x : α) → M) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i)) (⨆ (i : ι), (s i).mulIndicator (f i))

Tactic:
⟨fun i ↦ ?_, fun a ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
refine_1 : ∀ (i : ι), (s i).mulIndicator (f i) ≤ mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i)
refine_2 :
  ∀ (a : α),
    LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
      ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
⊢ (∀ (i : ι), (s i).mulIndicator (f i) ≤ mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i)) ∧
    LE.le (α := (x : α) → M) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i)) (⨆ (i : ι), (s i).mulIndicator (f i))

Tactic:
refine ⟨fun i ↦ ?_, fun a ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
i : ι
h₂ : 1 ≤ f i
⊢ (s i).mulIndicator (f i) ≤ mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i)

Tactic:
grw [← le_iSup f i, ← subset_iUnion s i]

Premises used: le_iSup, Set.subset_iUnion
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
i : ι
i_1 : α
⊢ 1 i_1 ≤ f i i_1

Tactic:
simp [← h1]
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
pos :
  ∀ (ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a),
    LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
      ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
neg :
  ∀ (ha : a ∉ ⋃ (i : ι), s i),
    LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
      ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
    ((⨆ (i : ι), (s i).mulIndicator (f i)) a)

Tactic:
by_cases ha : a ∈ ⋃ i, s i
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a
⊢ ∃ (i : ι), a ∈ s i

Tactic:
simpa using ha
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a
pos :
  ∀ (i : ι) (hi : a ∈ s i),
    LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
      ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
    ((⨆ (i : ι), (s i).mulIndicator (f i)) a)

Tactic:
obtain ⟨i, hi⟩ : ∃ i, a ∈ s i := by simpa using ha
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a
i : ι
hi : a ∈ s i
pos : LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (⨆ (i : ι), f i a) (⨆ (i : ι), (s i).mulIndicator (f i) a)
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
    ((⨆ (i : ι), (s i).mulIndicator (f i)) a)

Tactic:
rw [mulIndicator_of_mem ha, iSup_apply, iSup_apply]

Premises used: Set.mulIndicator_of_mem, iSup_apply
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a
i : ι
hi : a ∈ s i
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (⨆ (i : ι), f i a) (⨆ (i : ι), (s i).mulIndicator (f i) a)

Tactic:
iSup_le fun j ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a
i : ι
hi : a ∈ s i
pos : ∀ (j : ι), f j a ≤ ⨆ (i : ι), (s i).mulIndicator (f i) a
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (⨆ (i : ι), f i a) (⨆ (i : ι), (s i).mulIndicator (f i) a)

Tactic:
refine iSup_le fun j ↦ ?_

Premises used: iSup_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a
i : ι
hi : a ∈ s i
j : ι
pos : ∀ (k : ι) (hik : i ≤ k) (hjk : j ≤ k), f j a ≤ ⨆ (i : ι), (s i).mulIndicator (f i) a
⊢ f j a ≤ ⨆ (i : ι), (s i).mulIndicator (f i) a

Tactic:
obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j

Premises used: exists_ge_ge
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a
i : ι
hi : a ∈ s i
j k : ι
hik : i ≤ k
hjk : j ≤ k
⊢ f j a ≤ ⨆ (i : ι), (s i).mulIndicator (f i) a

Tactic:
le_iSup_of_le k <| (hf hjk _).trans_eq ?_

Premises used: LE.le.trans_eq, le_iSup_of_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a
i : ι
hi : a ∈ s i
j k : ι
hik : i ≤ k
hjk : j ≤ k
pos : f k a = (s k).mulIndicator (f k) a
⊢ f j a ≤ ⨆ (i : ι), (s i).mulIndicator (f i) a

Tactic:
refine le_iSup_of_le k <| (hf hjk _).trans_eq ?_

Premises used: LE.le.trans_eq, le_iSup_of_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : Membership.mem (γ := Set α) (⋃ (i : ι), s i) a
i : ι
hi : a ∈ s i
j k : ι
hik : i ≤ k
hjk : j ≤ k
pos pos₁ : f k a = f k a
⊢ f k a = (s k).mulIndicator (f k) a

Tactic:
rw [mulIndicator_of_mem (hs hik hi)]

Premises used: Set.mulIndicator_of_mem
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ (i : ι), s i
neg : LE.le.{u_3} (α := (fun (x : α) ↦ M) a) ⊥ ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
    ((⨆ (i : ι), (s i).mulIndicator (f i)) a)

Tactic:
rw [mulIndicator_of_notMem ha, ← h1]

Premises used: Set.mulIndicator_of_notMem
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ (i : ι), s i
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) ⊥ ((⨆ (i : ι), (s i).mulIndicator (f i)) a)

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CompleteLattice M
inst_1 : One M
ι : Type u_4
inst_2 : Preorder ι
inst_3 : IsDirectedOrder ι
f : ι → α → M
s : ι → Set α
h1 : Eq.{u_3 + 1} (α := M) ⊥ 1
hf : Monotone f
hs : Monotone s
a : α
ha : a ∉ ⋃ (i : ι), s i
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) ⊥ ((⨆ (i : ι), (s i).mulIndicator (f i)) a)

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
inst_1 : PartialOrder M
inst_2 : CanonicallyOrderedMul M
s : Set α
f : α → M
⊢ s.mulIndicator f ≤ f

Tactic:
mulIndicator_le_self' fun _ _ ↦ one_le

Premises used: Set.mulIndicator_le_self', one_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
inst_1 : PartialOrder M
inst_2 : CanonicallyOrderedMul M
a : α
s : Set α
f g : α → M
hfg : a ∈ s → f a ≤ g a
⊢ s.mulIndicator f a ≤ g a

Tactic:
mulIndicator_apply_le' hfg fun _ ↦ one_le

Premises used: Set.mulIndicator_apply_le', one_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : Monoid M
inst_1 : PartialOrder M
inst_2 : CanonicallyOrderedMul M
s : Set α
f g : α → M
hfg : ∀ a ∈ s, f a ≤ g a
⊢ s.mulIndicator f ≤ g

Tactic:
mulIndicator_le' hfg fun _ _ ↦ one_le

Premises used: Set.mulIndicator_le', one_le
-- Module: Mathlib.Algebra.Order.Group.Indicator
Goal:
α : Type u_2
M : Type u_3
inst : CommGroup M
inst_1 : Lattice M
s t : Set α
f : α → M
x : α
⊢ |(s ∆ t).mulIndicator f x|ₘ = |s.mulIndicator f x / t.mulIndicator f x|ₘ

Tactic:
apply_mulIndicator_symmDiff mabs_inv s t f x

Premises used: Set.apply_mulIndicator_symmDiff, mabs_inv
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
set :
  let r := Ioc (c - (↑(#s) : ℤ)) c;
  LE.le (α := ℤ) (∑ x ∈ s, x) (∑ x ∈ r, x)
⊢ LE.le (α := ℤ) (∑ x ∈ s, x) (∑ x ∈ Ioc (c - (↑(#s) : ℤ)) c, x)

Tactic:
set r := Ioc (c - #s) c

Premises used: HSub.hSub, Nat.cast, Finset.card, Finset.Ioc
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
rw : HAdd.hAdd (α := ℤ) (∑ x ∈ s ∩ r, x) (∑ x ∈ s \ r, x) ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ))
⊢ ∑ x ∈ s, x ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ))

Tactic:
rw [← sum_inter_add_sum_diff s r _]

Premises used: Finset.sum_inter_add_sum_diff
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
bc : ∑ x ∈ s \ r, x ≤ #(s \ r) • (c - (↑(#s) : ℤ))
⊢ HAdd.hAdd (α := ℤ) (∑ x ∈ s ∩ r, x) (∑ x ∈ s \ r, x) ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ))

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
bc : ∀ x ∈ s \ r, x ≤ c - (↑(#s) : ℤ)
⊢ ∑ x ∈ s \ r, x ≤ #(s \ r) • (c - (↑(#s) : ℤ))

Tactic:
apply sum_le_card_nsmul

Premises used: Finset.sum_le_card_nsmul
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ ∀ x ∈ s \ r, x ≤ c - (↑(#s) : ℤ)

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
rw : #s = #r
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ))

Tactic:
rw [inter_comm, card_sdiff_comm]

Premises used: Finset.inter_comm, Finset.card_sdiff_comm
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
rw : #s = (c - (c - (↑(#s) : ℤ))).toNat
rw₁ : #s = Int.toNat (↑(#s) : ℤ)
rw₂ rw₃ : #s = #s
⊢ #s = #r

Tactic:
rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_natCast]

Premises used: Int.toNat_natCast, Int.card_Ioc, sub_sub_cancel
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
rw : ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ)) ≤ HAdd.hAdd (α := ℤ) (∑ x ∈ r ∩ s, x) (∑ x ∈ r \ s, x)
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ)) ≤ ∑ x ∈ r, x

Tactic:
rw [← sum_inter_add_sum_diff r s _]

Premises used: Finset.sum_inter_add_sum_diff
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
bc : #(r \ s) • (c - (↑(#s) : ℤ)) ≤ ∑ x ∈ r \ s, x
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ)) ≤ HAdd.hAdd (α := ℤ) (∑ x ∈ r ∩ s, x) (∑ x ∈ r \ s, x)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ #(r \ s) • (c - (↑(#s) : ℤ)) ≤ ∑ x ∈ r \ s, x

Tactic:
card_nsmul_le_sum _ _ _ fun x mx ↦ ?_

Premises used: Finset.card_nsmul_le_sum
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
bc : ∀ (x : ℤ) (mx : x ∈ r \ s), c - (↑(#s) : ℤ) ≤ x
⊢ #(r \ s) • (c - (↑(#s) : ℤ)) ≤ ∑ x ∈ r \ s, x

Tactic:
refine card_nsmul_le_sum _ _ _ fun x mx ↦ ?_

Premises used: Finset.card_nsmul_le_sum
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
x : ℤ
mx : x ∈ r \ s
⊢ (c - (↑(#s) : ℤ) < x ∧ x ≤ c) ∧ x ∉ s

Tactic:
rw [mem_sdiff, mem_Ioc] at mx

Premises used: Finset.mem_sdiff, Finset.mem_Ioc
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
x : ℤ
mx : (c - (↑(#s) : ℤ) < x ∧ x ≤ c) ∧ x ∉ s
⊢ c - (↑(#s) : ℤ) ≤ x

Tactic:
mx.1.1.le

Premises used: LT.lt.le, And.left
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
x : ℤ
mx : (c - (↑(#s) : ℤ) < x ∧ x ≤ c) ∧ x ∉ s
⊢ c - (↑(#s) : ℤ) ≤ x

Tactic:
exact mx.1.1.le

Premises used: LT.lt.le, And.left
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
_ : ∑ x ∈ s, x ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ))
_₁ : ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ))
_₂ : ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ)) ≤ ∑ x ∈ r, x
⊢ LE.le (α := ℤ) (∑ x ∈ s, x) (∑ x ∈ r, x)

Tactic:
calc
    _ ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - #s) := by
      rw [← sum_inter_add_sum_diff s r _]
      gcongr
      apply sum_le_card_nsmul
      grind
    _ = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_natCast]
    _ ≤ _ := by
      rw [← sum_inter_add_sum_diff r s _]
      gcongr
      refine card_nsmul_le_sum _ _ _ fun x mx ↦ ?_
      rw [mem_sdiff, mem_Ioc] at mx; exact mx.1.1.le

Premises used: HSub.hSub, Nat.cast, SDiff.sdiff, Finset.card
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ LE.le (α := ℤ) (∑ x ∈ s, x) (∑ x ∈ Ioc (c - (↑(#s) : ℤ)) c, x)

Tactic:
sum_le_sum_Ioc hs

Premises used: Finset.sum_le_sum_Ioc
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
h : Eq (α := ℤ) (∑ n ∈ range #s, (c - (↑n : ℤ))) (∑ x ∈ Ioc (c - (↑(#s) : ℤ)) c, x)
⊢ LE.le (α := ℤ) (∑ x ∈ s, x) (∑ n ∈ range #s, (c - (↑n : ℤ)))

Tactic:
convert! sum_le_sum_Ioc hs

Premises used: Finset.sum_le_sum_Ioc
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c - (↑n : ℤ))) (∑ x ∈ Ioc (c - (↑(#s) : ℤ)) c, x)

Tactic:
sum_nbij (c - ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)

Premises used: Finset.sum_nbij, HSub.hSub, Nat.cast, rfl
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
h : ∀ a ∈ range #s, (fun (x : ℕ) ↦ c - (↑x : ℤ)) a ∈ Ioc (c - (↑(#s) : ℤ)) c
h₁ : Set.InjOn (β := ℤ) (fun (x : ℕ) ↦ c - (↑x : ℤ)) (↑(range #s) : Set ℕ)
h₂ : Set.SurjOn (fun (x : ℕ) ↦ c - (↑x : ℤ)) (↑(range #s) : Set ℕ) (↑(Ioc (c - (↑(#s) : ℤ)) c) : Set ℤ)
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c - (↑n : ℤ))) (∑ x ∈ Ioc (c - (↑(#s) : ℤ)) c, x)

Tactic:
refine sum_nbij (c - ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)

Premises used: Finset.sum_nbij, HSub.hSub, rfl
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
h : c - (↑(#s) : ℤ) < (fun (x : ℕ) ↦ c - (↑x : ℤ)) x ∧ (fun (x : ℕ) ↦ c - (↑x : ℤ)) x ≤ c
⊢ (fun (x : ℕ) ↦ c - (↑x : ℤ)) x ∈ Ioc (c - (↑(#s) : ℤ)) c

Tactic:
rw [mem_Ioc]

Premises used: Finset.mem_Ioc
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ x < #s

Tactic:
rw [mem_range] at mx

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x < #s
⊢ c - (↑(#s) : ℤ) < c - (↑x : ℤ) ∧ c - (↑x : ℤ) ≤ c

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ (↑(range #s) : Set ℕ)
y : ℕ
my : y ∈ (↑(range #s) : Set ℕ)
h : ∀ (h : c - (↑x : ℤ) = c - (↑y : ℤ)), x = y
⊢ Eq (α := ℤ) ((fun (x : ℕ) ↦ c - (↑x : ℤ)) x) ((fun (x : ℕ) ↦ c - (↑x : ℤ)) y) → x = y

Tactic:
(h : c - x = c - y)
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ (↑(range #s) : Set ℕ)
y : ℕ
my : y ∈ (↑(range #s) : Set ℕ)
h : c - (↑x : ℤ) = c - (↑y : ℤ)
⊢ x = y

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ (↑(Ioc (c - (↑(#s) : ℤ)) c) : Set ℤ)
h : ∃ x_1 < #s, c - (↑x_1 : ℤ) = x
⊢ Membership.mem (γ := Set ℤ) ((fun (x : ℕ) ↦ c - (↑x : ℤ)) '' (↑(range #s) : Set ℕ)) x

Tactic:
simp_rw [coe_range, Set.mem_image, Set.mem_Iio]

Premises used: Set.mem_Iio, Finset.coe_range, Set.mem_image
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ (↑(Ioc (c - (↑(#s) : ℤ)) c) : Set ℤ)
⊢ c - (↑(#s) : ℤ) < x ∧ x ≤ c

Tactic:
rw [mem_coe, mem_Ioc] at mx

Premises used: Finset.mem_Ioc, Finset.mem_coe
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : c - (↑(#s) : ℤ) < x ∧ x ≤ c
h : (c - x).toNat < #s ∧ c - (↑(c - x).toNat : ℤ) = x
⊢ ∃ x_1 < #s, c - (↑x_1 : ℤ) = x

Tactic:
use (c - x).toNat

Premises used: HSub.hSub, Int.toNat
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : c - (↑(#s) : ℤ) < x ∧ x ≤ c
⊢ (c - x).toNat < #s ∧ c - (↑(c - x).toNat : ℤ) = x

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
set :
  let r := Ico c (c + (↑(#s) : ℤ));
  LE.le (α := ℤ) (∑ x ∈ r, x) (∑ x ∈ s, x)
⊢ LE.le (α := ℤ) (∑ x ∈ Ico c (c + (↑(#s) : ℤ)), x) (∑ x ∈ s, x)

Tactic:
set r := Ico c (c + #s)

Premises used: Finset.Ico, Nat.cast, HAdd.hAdd, Finset.card
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
grw : ∀ (x : ℤ) (mx : x ∈ r \ s), x ≤ c + (↑(#s) : ℤ)
⊢ ∑ x ∈ r, x ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ))

Tactic:
grw [← sum_inter_add_sum_diff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]

Premises used: Finset.sum_inter_add_sum_diff, Finset.sum_le_card_nsmul
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
x : ℤ
mx : x ∈ r \ s
⊢ (c ≤ x ∧ x < c + (↑(#s) : ℤ)) ∧ x ∉ s

Tactic:
rw [mem_sdiff, mem_Ico] at mx

Premises used: Finset.mem_sdiff, Finset.mem_Ico
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
x : ℤ
mx : (c ≤ x ∧ x < c + (↑(#s) : ℤ)) ∧ x ∉ s
⊢ x ≤ c + (↑(#s) : ℤ)

Tactic:
mx.1.2.le

Premises used: LT.lt.le, And.right, And.left
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
x : ℤ
mx : (c ≤ x ∧ x < c + (↑(#s) : ℤ)) ∧ x ∉ s
⊢ x ≤ c + (↑(#s) : ℤ)

Tactic:
exact mx.1.2.le

Premises used: LT.lt.le, And.right, And.left
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
rw : #r = #s
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ)) = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + (↑(#s) : ℤ))

Tactic:
rw [inter_comm, card_sdiff_comm]

Premises used: Finset.inter_comm, Finset.card_sdiff_comm