awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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
⊢ Eq.{u_3 + 1} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)
have neg : ∀ (j : ι) (hj : x ∉ s j), Eq.{u_3 + 1} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)
Tactic: rcases hx with ⟨j, hj⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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
⊢ Eq.{u_3 + 1} (α := M) 1 (⨅ (i : ι), (s i).mulIndicator f x)
have neg : LE.le.{u_3} (α := M) (⨅ (i : ι), (s i).mulIndicator f x) 1
Tactic: refine le_antisymm (by simp only [← h1, le_iInf_iff, bot_le, forall_const]) ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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
⊢ Eq (α := (x : α) → M) (⨆ (i : ι), (s i).mulIndicator (f i)) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i))
have 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))
Tactic: simp only [le_antisymm_iff, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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))
have refine_1 : ∀ (i : ι), (s i).mulIndicator (f i) ≤ mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i)
Tactic: refine ⟨fun i ↦ ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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)
⊢ (∀ (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))
have 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)
Tactic: refine ⟨fun i ↦ ?_, fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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)
have h₂ : 1 ≤ f i
Tactic: grw [← le_iSup f i, ← subset_iUnion s i]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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 : α
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
    ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
have 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)
Tactic: by_cases ha : a ∈ ⋃ i, s i
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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)
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
    ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
have 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)
Tactic: by_cases ha : a ∈ ⋃ i, s i
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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
⊢ LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
    ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
have 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)
Tactic: obtain ⟨i, hi⟩ : ∃ i, a ∈ s i := by simpa using ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
    ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
have pos : LE.le.{u_3} (α := (fun (x : α) ↦ M) a) (⨆ (i : ι), f i a) (⨆ (i : ι), (s i).mulIndicator (f i) a)
Tactic: rw [mulIndicator_of_mem ha, iSup_apply, iSup_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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)
have pos : ∀ (j : ι), f j a ≤ ⨆ (i : ι), (s i).mulIndicator (f i) a
Tactic: refine iSup_le fun j ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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 : ι
⊢ f j a ≤ ⨆ (i : ι), (s i).mulIndicator (f i) a
have pos : ∀ (k : ι) (hik : i ≤ k) (hjk : j ≤ k), f j a ≤ ⨆ (i : ι), (s i).mulIndicator (f i) a
Tactic: obtain ⟨k, hik, hjk⟩ := exists_ge_ge i j
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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
have pos : f k a = (s k).mulIndicator (f k) a
Tactic: refine le_iSup_of_le k <| (hf hjk _).trans_eq ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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 k a = (s k).mulIndicator (f k) a
have pos : f k a = f k a
Tactic: rw [mulIndicator_of_mem (hs hik hi)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Indicator (goal)
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) (mulIndicator (⋃ (i : ι), s i) (⨆ (i : ι), f i) a)
    ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
have neg : LE.le.{u_3} (α := (fun (x : α) ↦ M) a) ⊥ ((⨆ (i : ι), (s i).mulIndicator (f i)) a)
Tactic: rw [mulIndicator_of_notMem ha, ← h1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
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) : ℤ))
have rw : HAdd.hAdd (α := ℤ) (∑ x ∈ s ∩ r, x) (∑ x ∈ s \ r, x) ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ))
Tactic: rw [← sum_inter_add_sum_diff s r _]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ HAdd.hAdd (α := ℤ) (∑ x ∈ s ∩ r, x) (∑ x ∈ s \ r, x) ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ))
have bc : ∑ x ∈ s \ r, x ≤ #(s \ r) • (c - (↑(#s) : ℤ))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ ∑ x ∈ s \ r, x ≤ #(s \ r) • (c - (↑(#s) : ℤ))
have bc : ∀ x ∈ s \ r, x ≤ c - (↑(#s) : ℤ)
Tactic: apply sum_le_card_nsmul
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ))
have rw : #s = #r
Tactic: rw [inter_comm, card_sdiff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ #s = #r
have rw : #s = (c - (c - (↑(#s) : ℤ))).toNat
Tactic: rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
rw : #s = (c - (c - (↑(#s) : ℤ))).toNat
⊢ #s = #r
have rw₁ : #s = Int.toNat (↑(#s) : ℤ)
Tactic: rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
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) : ℤ)
⊢ #s = #r
have rw₂ : #s = #s
Tactic: rw [Int.card_Ioc, sub_sub_cancel, Int.toNat_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ)) ≤ ∑ x ∈ r, x
have rw : ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ)) ≤ HAdd.hAdd (α := ℤ) (∑ x ∈ r ∩ s, x) (∑ x ∈ r \ s, x)
Tactic: rw [← sum_inter_add_sum_diff r s _]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ)) ≤ HAdd.hAdd (α := ℤ) (∑ x ∈ r ∩ s, x) (∑ x ∈ r \ s, x)
have bc : #(r \ s) • (c - (↑(#s) : ℤ)) ≤ ∑ x ∈ r \ s, x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ #(r \ s) • (c - (↑(#s) : ℤ)) ≤ ∑ x ∈ r \ s, x
have bc : ∀ (x : ℤ) (mx : x ∈ r \ s), c - (↑(#s) : ℤ) ≤ x
Tactic: refine card_nsmul_le_sum _ _ _ fun x mx ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (hypothesis)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
x : ℤ
mx : x ∈ r \ s
⊢ c - (↑(#s) : ℤ) ≤ x
have mx₁ : (c - (↑(#s) : ℤ) < x ∧ x ≤ c) ∧ x ∉ s
Tactic: rw [mem_sdiff, mem_Ioc] at mx
Cleared hypotheses: mx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - (↑(#s) : ℤ)) c
⊢ LE.le (α := ℤ) (∑ x ∈ s, x) (∑ x ∈ r, x)
have _ : ∑ x ∈ s, x ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ))
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
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
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) : ℤ))
⊢ LE.le (α := ℤ) (∑ x ∈ s, x) (∑ x ∈ r, x)
have _₁ : ∑ x ∈ s ∩ r, x + #(s \ r) • (c - (↑(#s) : ℤ)) = ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ))
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
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
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) : ℤ))
⊢ LE.le (α := ℤ) (∑ x ∈ s, x) (∑ x ∈ r, x)
have _₂ : ∑ x ∈ r ∩ s, x + #(r \ s) • (c - (↑(#s) : ℤ)) ≤ ∑ 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
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ LE.le (α := ℤ) (∑ x ∈ s, x) (∑ n ∈ range #s, (c - (↑n : ℤ)))
have h : Eq (α := ℤ) (∑ n ∈ range #s, (c - (↑n : ℤ))) (∑ x ∈ Ioc (c - (↑(#s) : ℤ)) c, x)
Tactic: convert! sum_le_sum_Ioc hs
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c - (↑n : ℤ))) (∑ x ∈ Ioc (c - (↑(#s) : ℤ)) c, x)
have h : ∀ a ∈ range #s, (fun (x : ℕ) ↦ c - (↑x : ℤ)) a ∈ Ioc (c - (↑(#s) : ℤ)) c
Tactic: refine sum_nbij (c - ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
h : ∀ a ∈ range #s, (fun (x : ℕ) ↦ c - (↑x : ℤ)) a ∈ Ioc (c - (↑(#s) : ℤ)) c
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c - (↑n : ℤ))) (∑ x ∈ Ioc (c - (↑(#s) : ℤ)) c, x)
have h₁ : Set.InjOn (β := ℤ) (fun (x : ℕ) ↦ c - (↑x : ℤ)) (↑(range #s) : Set ℕ)
Tactic: refine sum_nbij (c - ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
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 ℕ)
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c - (↑n : ℤ))) (∑ x ∈ Ioc (c - (↑(#s) : ℤ)) c, x)
have h₂ : Set.SurjOn (fun (x : ℕ) ↦ c - (↑x : ℤ)) (↑(range #s) : Set ℕ) (↑(Ioc (c - (↑(#s) : ℤ)) c) : Set ℤ)
Tactic: refine sum_nbij (c - ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ (fun (x : ℕ) ↦ c - (↑x : ℤ)) x ∈ Ioc (c - (↑(#s) : ℤ)) c
have h : c - (↑(#s) : ℤ) < (fun (x : ℕ) ↦ c - (↑x : ℤ)) x ∧ (fun (x : ℕ) ↦ c - (↑x : ℤ)) x ≤ c
Tactic: rw [mem_Ioc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (hypothesis)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℕ
mx : x ∈ range #s
⊢ c - (↑(#s) : ℤ) < c - (↑x : ℤ) ∧ c - (↑x : ℤ) ≤ c
have mx₁ : x < #s
Tactic: rw [mem_range] at mx
Cleared hypotheses: mx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ (↑(Ioc (c - (↑(#s) : ℤ)) c) : Set ℤ)
⊢ Membership.mem (γ := Set ℤ) ((fun (x : ℕ) ↦ c - (↑x : ℤ)) '' (↑(range #s) : Set ℕ)) x
have h : ∃ x_1 < #s, c - (↑x_1 : ℤ) = x
Tactic: simp_rw [coe_range, Set.mem_image, Set.mem_Iio]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (hypothesis)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : x ∈ (↑(Ioc (c - (↑(#s) : ℤ)) c) : Set ℤ)
⊢ ∃ x_1 < #s, c - (↑x_1 : ℤ) = x
have mx₁ : c - (↑(#s) : ℤ) < x ∧ x ≤ c
Tactic: rw [mem_coe, mem_Ioc] at mx
Cleared hypotheses: mx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
x : ℤ
mx : c - (↑(#s) : ℤ) < x ∧ x ≤ c
⊢ ∃ x_1 < #s, c - (↑x_1 : ℤ) = x
have h : (c - x).toNat < #s ∧ c - (↑(c - x).toNat : ℤ) = x
Tactic: use (c - x).toNat
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
⊢ ∑ x ∈ r, x ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ))
have grw : ∀ (x : ℤ) (mx : x ∈ r \ s), x ≤ c + (↑(#s) : ℤ)
Tactic: grw [← sum_inter_add_sum_diff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (hypothesis)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
x : ℤ
mx : x ∈ r \ s
⊢ x ≤ c + (↑(#s) : ℤ)
have mx₁ : (c ≤ x ∧ x < c + (↑(#s) : ℤ)) ∧ x ∉ s
Tactic: rw [mem_sdiff, mem_Ico] at mx
Cleared hypotheses: mx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ)) = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + (↑(#s) : ℤ))
have rw : #r = #s
Tactic: rw [inter_comm, card_sdiff_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
⊢ #r = #s
have rw : (c + (↑(#s) : ℤ) - c).toNat = #s
Tactic: rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
rw : (c + (↑(#s) : ℤ) - c).toNat = #s
⊢ #r = #s
have rw₁ : Int.toNat (↑(#s) : ℤ) = #s
Tactic: rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
rw : (c + (↑(#s) : ℤ) - c).toNat = #s
rw₁ : Int.toNat (↑(#s) : ℤ) = #s
⊢ #r = #s
have rw₂ : #s = #s
Tactic: rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c + (↑(#s) : ℤ)) ≤ ∑ x ∈ s, x
have grw : ∀ (x : ℤ) (mx : x ∈ s \ r), c + (↑(#s) : ℤ) ≤ x
Tactic: grw [← sum_inter_add_sum_diff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
⊢ LE.le (α := ℤ) (∑ x ∈ r, x) (∑ x ∈ s, x)
have _ : ∑ x ∈ r, x ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ))
Tactic: calc
    _ ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + #s) := by
      grw [← sum_inter_add_sum_diff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]
      rw [mem_sdiff, mem_Ico] at mx; exact mx.1.2.le
    _ = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
    _ ≤ _ := by
      grw [← sum_inter_add_sum_diff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]
      grind
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
_ : ∑ x ∈ r, x ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ))
⊢ LE.le (α := ℤ) (∑ x ∈ r, x) (∑ x ∈ s, x)
have _₁ : ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ)) = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + (↑(#s) : ℤ))
Tactic: calc
    _ ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + #s) := by
      grw [← sum_inter_add_sum_diff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]
      rw [mem_sdiff, mem_Ico] at mx; exact mx.1.2.le
    _ = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
    _ ≤ _ := by
      grw [← sum_inter_add_sum_diff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]
      grind
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
_ : ∑ x ∈ r, x ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ))
_₁ : ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ)) = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + (↑(#s) : ℤ))
⊢ LE.le (α := ℤ) (∑ x ∈ r, x) (∑ x ∈ s, x)
have _₂ : ∑ x ∈ s ∩ r, x + #(s \ r) • (c + (↑(#s) : ℤ)) ≤ ∑ x ∈ s, x
Tactic: calc
    _ ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + #s) := by
      grw [← sum_inter_add_sum_diff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]
      rw [mem_sdiff, mem_Ico] at mx; exact mx.1.2.le
    _ = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
    _ ≤ _ := by
      grw [← sum_inter_add_sum_diff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]
      grind
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ LE.le (α := ℤ) (∑ n ∈ range #s, (c + (↑n : ℤ))) (∑ x ∈ s, x)
have h : Eq (α := ℤ) (∑ n ∈ range #s, (c + (↑n : ℤ))) (∑ x ∈ Ico c (c + (↑(#s) : ℤ)), x)
Tactic: convert! sum_Ico_le_sum hs
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c + (↑n : ℤ))) (∑ x ∈ Ico c (c + (↑(#s) : ℤ)), x)
have h : ∀ a ∈ range #s, (fun (x : ℕ) ↦ c + (↑x : ℤ)) a ∈ Ico c (c + (↑(#s) : ℤ))
Tactic: refine sum_nbij (c + ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
h : ∀ a ∈ range #s, (fun (x : ℕ) ↦ c + (↑x : ℤ)) a ∈ Ico c (c + (↑(#s) : ℤ))
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c + (↑n : ℤ))) (∑ x ∈ Ico c (c + (↑(#s) : ℤ)), x)
have h₁ : Set.InjOn (β := ℤ) (fun (x : ℕ) ↦ c + (↑x : ℤ)) (↑(range #s) : Set ℕ)
Tactic: refine sum_nbij (c + ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)