awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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))
hindep : LinearIndepOn ℕ id (↑t : Set M)
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))

Tactic:
exact IsProperLinearSet.isProperSemilinearSet ⟨a, t, by simpa⟩

Premises used: IsProperLinearSet.isProperSemilinearSet, SetLike.coe, Exists.intro
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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))
hindep : ¬LinearIndepOn ℕ id (↑t : Set M)
⊢ ∃ t_1 ⊆ t, ∃ (f : M → ℕ), Eq (α := M) (∑ i ∈ t_1, f i • id i) (∑ i ∈ t \ t_1, f i • id i) ∧ ∃ i ∈ t_1, 0 < f i

Tactic:
rw [not_linearIndepOn_finset_iffₒₛ] at hindep

Premises used: not_linearIndepOn_finset_iffₒₛ
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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))
hindep : ∃ t_1 ⊆ t, ∃ (f : M → ℕ), Eq (α := M) (∑ i ∈ t_1, f i • id i) (∑ i ∈ t \ t_1, f i • id i) ∧ ∃ i ∈ t_1, 0 < f i
neg :
  ∀ (t' : Finset M) (ht' : t' ⊆ t) (f : M → ℕ) (heq : Eq (α := M) (∑ i ∈ t', f i • id i) (∑ i ∈ t \ t', f i • id i))
    (i : M) (hi : i ∈ t') (hfi : 0 < f i), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))

Tactic:
rcases hindep with ⟨t', ht', f, heq, i, hi, hfi⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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 → ℕ
heq : Eq (α := M) (∑ i ∈ t', f i • id i) (∑ i ∈ t \ t', f i • id i)
i : M
hi : i ∈ t'
hfi : 0 < f i
⊢ Eq (α := M) (∑ x ∈ t', f x • x) (∑ x ∈ t \ t', f x • x)

Tactic:
simp only [Function.id_def] at heq

Premises used: Function.id_def
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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)
h :
  a +ᵥ (↑(closure (↑t : Set M)) : Set M) =
    ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)
neg :
  IsProperSemilinearSet.{u_1} (M := M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))

Tactic:
convert_to IsProperSemilinearSet (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j),
    (a + k • j) +ᵥ (closure (t.erase j : Set M) : Set M))

Premises used: IsProperSemilinearSet, HVAdd.hVAdd, SetLike.coe, HAdd.hAdd, AddSubmonoid.closure, HSMul.hSMul, Finset.erase, Set.iUnion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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)
h :
  ∀ (x : M),
    x ∈ a +ᵥ (↑(closure (↑t : Set M)) : Set M) ↔
      Membership.mem (γ := Set M)
        (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x
⊢ a +ᵥ (↑(closure (↑t : Set M)) : Set M) =
    ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
h :
  (∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y ∧ a +ᵥ y = x) →
    Membership.mem (γ := Set M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x
h₁ :
  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
⊢ (∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y ∧ a +ᵥ y = x) ↔
    Membership.mem (γ := Set M)
      (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) x

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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)
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y
⊢ ∃ (f : M → ℕ), Function.support f ⊆ (↑t : Set M) ∧ ∑ a ∈ t, f a • a = y

Tactic:
rw [mem_closure_finset] at hy

Premises used: AddSubmonoid.mem_closure_finset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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)
y : M
hy : ∃ (f : M → ℕ), Function.support f ⊆ (↑t : Set M) ∧ ∑ a ∈ t, f a • a = y
h :
  ∀ (g : 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))
⊢ Membership.mem (γ := Set M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M)) (a +ᵥ y)

Tactic:
rcases hy with ⟨g, -, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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 → ℕ
h :
  ∀ (n : ℕ)
    (ih' :
      ∀ m < n,
        ∀ (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)))
    (g : M → ℕ) (hn : g i = n),
    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))

Tactic:
induction hn : g i using Nat.strong_induction_on generalizing g with | _ n ih'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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)
n : ℕ
ih' :
  ∀ m < n,
    ∀ (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))
g : M → ℕ
hn : g i = n
⊢ ∀ 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))

Tactic:
subst hn
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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))
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))
⊢ 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
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
⊢ (fun (j : M) ↦ if j ∈ t' then g j - f j else g j + f j) i = g i - f i

Tactic:
simp [hi]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
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)
⊢ 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:
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

Premises used: HSub.hSub, Membership.mem, Nat.sub_lt_self, HAdd.hAdd, ite
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
rw : HVAdd.hVAdd (β := M) a (∑ a ∈ t' ∪ t \ t', g a • a)
| HVAdd.hVAdd (β := M) a (∑ a ∈ t, g a • a)

Tactic:
rw [← Finset.union_sdiff_of_subset ht']

Premises used: Finset.union_sdiff_of_subset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
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)
⊢ 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:
conv_lhs => rw [← Finset.union_sdiff_of_subset ht']

Premises used: Finset.union_sdiff_of_subset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
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)
⊢ 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:
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]

Premises used: Finset.filter_notMem_eq_sdiff, Iff.mpr, Finset.sum_add_distrib, add_assoc, add_right_comm, Finset.sum_union, add_left_cancel_iff, Disjoint.symm, add_smul, vadd_eq_add, Finset.inter_eq_right, ite_smul, Finset.sdiff_disjoint, Finset.filter_mem_eq_inter, Finset.sum_ite
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
h : ∀ (j : M) (hj : j ∈ t'), g j • j = (g j - f j) • j + f j • 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)

Tactic:
congr! 2 with j hj
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
h₁ h₂ : g j • j = g j • j
⊢ g j • j = (g j - f j) • j + f j • j

Tactic:
rw [← add_smul, tsub_add_cancel_of_le (hfg j hj)]

Premises used: tsub_add_cancel_of_le, add_smul
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
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))
⊢ 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⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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 :
  ∃ (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
⊢ 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:
simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]

Premises used: Set.mem_vadd_set, Set.mem_iUnion, Finset.mem_range, SetLike.mem_coe, vadd_eq_add
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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

Tactic:
⟨j, hj, g j, hgj, ∑ k ∈ t.erase j, g k • k,
          sum_mem fun x hx => (nsmul_mem (mem_closure_of_mem hx) _), ?_⟩

Premises used: nsmul_mem, AddSubmonoid.mem_closure_of_mem, And.intro, Exists.intro, HSMul.hSMul, Finset.erase, Finset.sum, sum_mem
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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 + ∑ a ∈ t, g a • a
⊢ ∃ (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:
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) _), ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
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
neg₂ neg₃ : a + ∑ k ∈ t.erase j, g k • k + g j • j = 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

Tactic:
rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]

Premises used: add_assoc, add_right_comm, Finset.sum_erase_add