awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
pos :
  ∀ (hfg : ∀ j ∈ t', f j ≤ g j),
    Membership.mem (γ := Set M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
      (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
have neg : ∀ (hfg : ∃ j ∈ t', g j < f j),
  Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
Tactic: by_cases! hfg : ∀ j ∈ t', f j ≤ g j
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
have h : HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a) =
  HVAdd.hVAdd (β := M) a (∑ a ∈ t, (if a ∈ t' then g a - f a else g a + f a) • a)
Tactic: convert!
        ih' (g i - f i) (Nat.sub_lt_self hfi (hfg i hi))
          (fun j => if j ∈ t' then g j - f j else g j + f j) (by simp [hi]) using 1
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
hfg : ∀ j ∈ t', f j ≤ g j
| HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a)
have rw : HVAdd.hVAdd (β := M) a (∑ a ∈ t' ∪ t \ t', g a • a)
Tactic: rw [← Finset.union_sdiff_of_subset ht']
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a) =
    HVAdd.hVAdd (β := M) a (∑ a ∈ t, (if a ∈ t' then g a - f a else g a + f a) • a)
have h : HVAdd.hVAdd (β := M) a (∑ a ∈ t' ∪ t \ t', g a • a) =
  HVAdd.hVAdd (β := M) a (∑ a ∈ t, (if a ∈ t' then g a - f a else g a + f a) • a)
Tactic: conv_lhs => rw [← Finset.union_sdiff_of_subset ht']
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ HVAdd.hVAdd (β := M) a (∑ a ∈ t' ∪ t \ t', g a • a) =
    HVAdd.hVAdd (β := M) a (∑ a ∈ t, (if a ∈ t' then g a - f a else g a + f a) • a)
have h : HAdd.hAdd (α := M) (∑ a ∈ t', g a • a) (∑ a ∈ t \ t', g a • a) =
  HAdd.hAdd (α := M) (∑ x ∈ t', ((g x - f x) • x + f x • x)) (∑ x ∈ t \ t', g x • x)
Tactic: simp_rw [vadd_eq_add, add_left_cancel_iff, Finset.sum_union Finset.sdiff_disjoint.symm,
          ite_smul, Finset.sum_ite, Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht',
          Finset.filter_notMem_eq_sdiff, add_smul, Finset.sum_add_distrib, ← heq, ← add_assoc,
          add_right_comm, ← Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ HAdd.hAdd (α := M) (∑ a ∈ t', g a • a) (∑ a ∈ t \ t', g a • a) =
    HAdd.hAdd (α := M) (∑ x ∈ t', ((g x - f x) • x + f x • x)) (∑ x ∈ t \ t', g x • x)
have h : ∀ (j : M) (hj : j ∈ t'), g j • j = (g j - f j) • j + f j • j
Tactic: congr! 2 with j hj
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
hfg : ∀ j ∈ t', f j ≤ g j
j : M
hj : j ∈ t'
⊢ g j • j = (g j - f j) • j + f j • j
have h : g j • j = (g j - f j + f j) • j
Tactic: rw [← add_smul, tsub_add_cancel_of_le (hfg j hj)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
hfg : ∀ j ∈ t', f j ≤ g j
j : M
hj : j ∈ t'
h : g j • j = (g j - f j + f j) • j
⊢ g j • j = (g j - f j) • j + f j • j
have h₁ : g j • j = g j • j
Tactic: rw [← add_smul, tsub_add_cancel_of_le (hfg j hj)]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
hfg : ∃ j ∈ t', g j < f j
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
have neg : ∀ (j : M) (hj : j ∈ t') (hgj : g j < f j),
  Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
Tactic: rcases hfg with ⟨j, hj, hgj⟩
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
j : M
hj : j ∈ t'
hgj : g j < f j
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
    (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
have neg : ∃ (i : M) (_ : i ∈ t') (i_1 : ℕ) (_ : i_1 < f i) (y : M),
  Membership.mem (γ := AddSubmonoid M) (closure (↑(t.erase i) : Set M)) y ∧ a + i_1 • i + y = a + ∑ a ∈ t, g a • a
Tactic: simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
j : M
hj : j ∈ t'
hgj : g j < f j
⊢ ∃ (i : M) (_ : i ∈ t') (i_1 : ℕ) (_ : i_1 < f i) (y : M),
    Membership.mem (γ := AddSubmonoid M) (closure (↑(t.erase i) : Set M)) y ∧ a + i_1 • i + y = a + ∑ a ∈ t, g a • a
have neg : a + g j • j + ∑ k ∈ t.erase j, g k • k = a + ∑ a ∈ t, g a • a
Tactic: refine ⟨j, hj, g j, hgj, ∑ k ∈ t.erase j, g k • k,
          sum_mem fun x hx => (nsmul_mem (mem_closure_of_mem hx) _), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
j : M
hj : j ∈ t'
hgj : g j < f j
⊢ a + g j • j + ∑ k ∈ t.erase j, g k • k = a + ∑ a ∈ t, g a • a
have neg : a + g j • j + ∑ k ∈ t.erase j, g k • k = a + (∑ x ∈ t.erase j, g x • x + g j • j)
Tactic: rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
j : M
hj : j ∈ t'
hgj : g j < f j
neg : a + g j • j + ∑ k ∈ t.erase j, g k • k = a + (∑ x ∈ t.erase j, g x • x + g j • j)
⊢ a + g j • j + ∑ k ∈ t.erase j, g k • k = a + ∑ a ∈ t, g a • a
have neg₁ : a + g j • j + ∑ k ∈ t.erase j, g k • k = a + ∑ x ∈ t.erase j, g x • x + g j • j
Tactic: rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ) (hn : g i = m),
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
        (HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a))
j : M
hj : j ∈ t'
hgj : g j < f j
neg : a + g j • j + ∑ k ∈ t.erase j, g k • k = a + (∑ x ∈ t.erase j, g x • x + g j • j)
neg₁ : a + g j • j + ∑ k ∈ t.erase j, g k • k = a + ∑ x ∈ t.erase j, g x • x + g j • j
⊢ a + g j • j + ∑ k ∈ t.erase j, g k • k = a + ∑ a ∈ t, g a • a
have neg₂ : a + ∑ k ∈ t.erase j, g k • k + g j • j = a + ∑ x ∈ t.erase j, g x • x + g j • j
Tactic: rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
x : M
⊢ Membership.mem (γ := Set M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x →
    ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y ∧ a +ᵥ y = x
have h : (∃ (i : M) (_ : i ∈ t') (i_1 : ℕ) (_ : i_1 < f i) (y : M),
    Membership.mem (γ := AddSubmonoid M) (closure (↑(t.erase i) : Set M)) y ∧ a + i_1 • i + y = x) →
  ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y ∧ a + y = x
Tactic: simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
j : M
hj : j ∈ t'
k : ℕ
hk : k < f j
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (↑(t.erase j) : Set M)) y
⊢ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y_1 ∧ a + y_1 = a + k • j + y
have h : a + (k • j + y) = a + k • j + y
Tactic: refine ⟨k • j + y,
        add_mem (nsmul_mem (mem_closure_of_mem (ht' hj)) _)
          ((closure_mono (t.erase_subset j)) hy), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
a : M
t : Finset M
ih :
  ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)
j : M
hj : j ∈ t'
k : ℕ
hk : k < f j
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (↑(t.erase j) : Set M)) y
⊢ a + (k • j + y) = a + k • j + y
have h : a + (k • j + y) = a + (k • j + y)
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : IsCancelAdd M
hs : IsLinearSet s
⊢ IsProperSemilinearSet s
have rw : ∀ (hs : ∃ (a : M) (t : Finset M), s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)), IsProperSemilinearSet s
Tactic: classical
  rw [isLinearSet_iff] at hs
  rcases hs with ⟨a, t, rfl⟩
  induction hn : t.card using Nat.strong_induction_on generalizing a t with | _ n ih
  subst hn
  by_cases hindep : LinearIndepOn ℕ id (t : Set M)
  · exact IsProperLinearSet.isProperSemilinearSet ⟨a, t, by simpa⟩
  rw [not_linearIndepOn_finset_iffₒₛ] at hindep
  rcases hindep with ⟨t', ht', f, heq, i, hi, hfi⟩
  simp only [Function.id_def] at heq
  convert_to IsProperSemilinearSet (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j),
    (a + k • j) +ᵥ (closure (t.erase j : Set M) : Set M))
  · ext x
    simp only [mem_vadd_set, SetLike.mem_coe]
    constructor
    · rintro ⟨y, hy, rfl⟩
      rw [mem_closure_finset] at hy
      rcases hy with ⟨g, -, rfl⟩
      induction hn : g i using Nat.strong_induction_on generalizing g with | _ n ih'
      subst hn
      by_cases! hfg : ∀ j ∈ t', f j ≤ g j
      · convert!
        ih' (g i - f i) (Nat.sub_lt_self hfi (hfg i hi))
          (fun j => if j ∈ t' then g j - f j else g j + f j) (by simp [hi]) using 1
        conv_lhs => rw [← Finset.union_sdiff_of_subset ht']
        simp_rw [vadd_eq_add, add_left_cancel_iff, Finset.sum_union Finset.sdiff_disjoint.symm,
          ite_smul, Finset.sum_ite, Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht',
          Finset.filter_notMem_eq_sdiff, add_smul, Finset.sum_add_distrib, ← heq, ← add_assoc,
          add_right_comm, ← Finset.sum_add_distrib]
        congr! 2 with j hj
        rw [← add_smul, tsub_add_cancel_of_le (hfg j hj)]
      · rcases hfg with ⟨j, hj, hgj⟩
        simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
        refine ⟨j, hj, g j, hgj, ∑ k ∈ t.erase j, g k • k,
          sum_mem fun x hx => (nsmul_mem (mem_closure_of_mem hx) _), ?_⟩
        rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]
    · simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
      rintro ⟨j, hj, k, hk, y, hy, rfl⟩
      refine ⟨k • j + y,
        add_mem (nsmul_mem (mem_closure_of_mem (ht' hj)) _)
          ((closure_mono (t.erase_subset j)) hy), ?_⟩
      rw [add_assoc]
  · exact .biUnion_finset fun j hj => .biUnion_finset fun k hk =>
      ih _ (Finset.card_lt_card (Finset.erase_ssubset (ht' hj))) _ _ rfl
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : IsCancelAdd M
hs : IsLinearSet s
rw rw₁ rw₂ : ∀ (hs : ∃ (a : M) (t : Finset M), s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)), IsProperSemilinearSet s
⊢ IsProperSemilinearSet s
have rw₃ : ∀ (a : M) (t : Finset M), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
Tactic: classical
  rw [isLinearSet_iff] at hs
  rcases hs with ⟨a, t, rfl⟩
  induction hn : t.card using Nat.strong_induction_on generalizing a t with | _ n ih
  subst hn
  by_cases hindep : LinearIndepOn ℕ id (t : Set M)
  · exact IsProperLinearSet.isProperSemilinearSet ⟨a, t, by simpa⟩
  rw [not_linearIndepOn_finset_iffₒₛ] at hindep
  rcases hindep with ⟨t', ht', f, heq, i, hi, hfi⟩
  simp only [Function.id_def] at heq
  convert_to IsProperSemilinearSet (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j),
    (a + k • j) +ᵥ (closure (t.erase j : Set M) : Set M))
  · ext x
    simp only [mem_vadd_set, SetLike.mem_coe]
    constructor
    · rintro ⟨y, hy, rfl⟩
      rw [mem_closure_finset] at hy
      rcases hy with ⟨g, -, rfl⟩
      induction hn : g i using Nat.strong_induction_on generalizing g with | _ n ih'
      subst hn
      by_cases! hfg : ∀ j ∈ t', f j ≤ g j
      · convert!
        ih' (g i - f i) (Nat.sub_lt_self hfi (hfg i hi))
          (fun j => if j ∈ t' then g j - f j else g j + f j) (by simp [hi]) using 1
        conv_lhs => rw [← Finset.union_sdiff_of_subset ht']
        simp_rw [vadd_eq_add, add_left_cancel_iff, Finset.sum_union Finset.sdiff_disjoint.symm,
          ite_smul, Finset.sum_ite, Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht',
          Finset.filter_notMem_eq_sdiff, add_smul, Finset.sum_add_distrib, ← heq, ← add_assoc,
          add_right_comm, ← Finset.sum_add_distrib]
        congr! 2 with j hj
        rw [← add_smul, tsub_add_cancel_of_le (hfg j hj)]
      · rcases hfg with ⟨j, hj, hgj⟩
        simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
        refine ⟨j, hj, g j, hgj, ∑ k ∈ t.erase j, g k • k,
          sum_mem fun x hx => (nsmul_mem (mem_closure_of_mem hx) _), ?_⟩
        rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]
    · simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
      rintro ⟨j, hj, k, hk, y, hy, rfl⟩
      refine ⟨k • j + y,
        add_mem (nsmul_mem (mem_closure_of_mem (ht' hj)) _)
          ((closure_mono (t.erase_subset j)) hy), ?_⟩
      rw [add_assoc]
  · exact .biUnion_finset fun j hj => .biUnion_finset fun k hk =>
      ih _ (Finset.card_lt_card (Finset.erase_ssubset (ht' hj))) _ _ rfl
Cleared hypotheses: s, hs