awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
hy : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0
⊢ a + x + 0 = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = a + x + 0

Tactic:
exact Or.inr ⟨x, hx, by simp⟩

Premises used: Or.inr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y
hy_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + y)
⊢ a + x + (a + y) = 0 ∨
    ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + (a + y)

Tactic:
Or.inr ⟨_, add_mem (mem_closure_of_mem (mem_insert _ _)) (add_mem hx hy), ?_⟩

Premises used: AddSubmonoid.mem_closure_of_mem, And.intro, Exists.intro, AddMemClass.add_mem, Set.mem_insert, Or.inr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y
hy_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + y)
h : a + (a + (x + y)) = a + x + (a + y)
⊢ a + x + (a + y) = 0 ∨
    ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + (a + y)

Tactic:
refine Or.inr ⟨_, add_mem (mem_closure_of_mem (mem_insert _ _)) (add_mem hx hy), ?_⟩

Premises used: Or.inr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y
hy_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + y)
h : a + a + x + y = a + x + a + y
⊢ a + (a + (x + y)) = a + x + (a + y)

Tactic:
simp_rw [← add_assoc, add_right_comm a a x]

Premises used: add_assoc, add_right_comm
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x
h :
  ∀ (x : M) (hx : x ∈ a +ᵥ (↑(closure t) : Set M)),
    x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
h₁ : Eq.{u_1 + 1} (α := M) 0 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = 0
h₂ :
  ∀ (x y : M),
    Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x →
      Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) y →
        ∀ (ih₁ : x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x)
          (ih₂ : y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = y),
          x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = x + y
⊢ x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x

Tactic:
induction hx using closure_induction with
    | mem x hx =>
      rcases hx with ⟨x, hx, rfl⟩
      exact Or.inr ⟨x, closure_mono (subset_insert _ _) hx, rfl⟩
    | zero => exact Or.inl rfl
    | add x y _ _ ih₁ ih₂ =>
      rcases ih₁ with rfl | ⟨x, hx, rfl⟩
      · simpa
      · rcases ih₂ with rfl | ⟨y, hy, rfl⟩
        · exact Or.inr ⟨x, hx, by simp⟩
        · refine Or.inr ⟨_, add_mem (mem_closure_of_mem (mem_insert _ _)) (add_mem hx hy), ?_⟩
          simp_rw [← add_assoc, add_right_comm a a x]

Premises used: add_assoc, add_right_comm, Or.inl, AddSubmonoid.zero, IsLinearSet.add, Or.inr, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
⊢ ∃ (y : M), (∃ (n : ℕ), n • a = y) ∧ ∃ (z : M), Membership.mem (γ := AddSubmonoid M) (closure t) z ∧ y + z = x

Tactic:
simp_rw [insert_eq, closure_union, mem_sup, mem_closure_singleton] at hx

Premises used: Set.insert_eq, AddSubmonoid.closure_union, AddSubmonoid.mem_sup, AddSubmonoid.mem_closure_singleton
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
hx : ∃ (y : M), (∃ (n : ℕ), n • a = y) ∧ ∃ (z : M), Membership.mem (γ := AddSubmonoid M) (closure t) z ∧ y + z = x
h :
  ∀ (n : ℕ) (x : M) (hx : Membership.mem (γ := AddSubmonoid M) (closure t) x),
    Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + (n • a + x))
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)

Tactic:
rcases hx with ⟨_, ⟨n, rfl⟩, ⟨x, hx, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
n : ℕ
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure t) x
h : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (n • a + (a + x))
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + (n • a + x))

Tactic:
rw [add_left_comm]

Premises used: add_left_comm
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
n : ℕ
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure t) x
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (n • a + (a + x))

Tactic:
add_mem (nsmul_mem (mem_closure_of_mem ?_) _)
        (mem_closure_of_mem (vadd_mem_vadd_set hx))

Premises used: Set.vadd_mem_vadd_set, nsmul_mem, AddSubmonoid.mem_closure_of_mem, AddMemClass.add_mem
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
n : ℕ
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure t) x
h : a ∈ a +ᵥ (↑(closure t) : Set M)
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (n • a + (a + x))

Tactic:
refine add_mem (nsmul_mem (mem_closure_of_mem ?_) _)
        (mem_closure_of_mem (vadd_mem_vadd_set hx))

Premises used: Set.vadd_mem_vadd_set, nsmul_mem, AddSubmonoid.mem_closure_of_mem, AddMemClass.add_mem
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
n : ℕ
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure t) x
h : a + 0 ∈ a +ᵥ (↑(closure t) : Set M)
⊢ a ∈ a +ᵥ (↑(closure t) : Set M)

Tactic:
nth_rw 2 [← add_zero a]

Premises used: add_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
n : ℕ
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure t) x
⊢ a + 0 ∈ a +ᵥ (↑(closure t) : Set M)

Tactic:
vadd_mem_vadd_set (zero_mem _)

Premises used: Set.vadd_mem_vadd_set, Set.Mem, ZeroMemClass.zero_mem
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
n : ℕ
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure t) x
⊢ a + 0 ∈ a +ᵥ (↑(closure t) : Set M)

Tactic:
exact vadd_mem_vadd_set (zero_mem _)

Premises used: Set.vadd_mem_vadd_set, ZeroMemClass.zero_mem
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : IsSemilinearSet s
rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t), IsSemilinearSet (↑(closure (⋃₀ S)) : Set M)
⊢ IsSemilinearSet (↑(closure s) : Set M)

Tactic:
rcases hs with ⟨S, hS, hS', rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS' : ∀ (t : Set M), Membership.mem (γ := Set (Set M)) ∅ t → IsLinearSet t
⊢ IsSemilinearSet (↑(closure (⋃₀ ∅)) : Set M)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
a : Set M
s : Set (Set M)
h : a ∉ s
hs : s.Finite
ih : ∀ (hS' : ∀ t ∈ s, IsLinearSet t), IsSemilinearSet (↑(closure (⋃₀ s)) : Set M)
hS' : ∀ t ∈ insert a s, IsLinearSet t
⊢ IsLinearSet a ∧ ∀ a ∈ s, IsLinearSet a

Tactic:
simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'

Premises used: forall_eq_or_imp, Set.mem_insert_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
a : Set M
s : Set (Set M)
h : a ∉ s
hs : s.Finite
ih : ∀ (hS' : ∀ t ∈ s, IsLinearSet t), IsSemilinearSet (↑(closure (⋃₀ s)) : Set M)
hS' : IsLinearSet a ∧ ∀ a ∈ s, IsLinearSet a
⊢ IsSemilinearSet (↑(closure (⋃₀ insert a s)) : Set M)

Tactic:
simpa [closure_union, coe_sup] using hS'.1.closure.add (ih hS'.2)

Premises used: AddSubmonoid.closure_union, IsLinearSet.closure, AddSubmonoid.coe_sup, And.right, And.left, IsSemilinearSet.add
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
empty :
  ∀ (hS' : ∀ (t : Set M), Membership.mem (γ := Set (Set M)) ∅ t → IsLinearSet t),
    IsSemilinearSet (↑(closure (⋃₀ ∅)) : Set M)
insert :
  ∀ {a : Set M} {s : Set (Set M)},
    a ∉ s →
      s.Finite →
        ∀ (ih : ∀ (hS' : ∀ t ∈ s, IsLinearSet t), IsSemilinearSet (↑(closure (⋃₀ s)) : Set M))
          (hS' : ∀ t ∈ Insert.insert a s, IsLinearSet t), IsSemilinearSet (↑(closure (⋃₀ Insert.insert a s)) : Set M)
⊢ IsSemilinearSet (↑(closure (⋃₀ S)) : Set M)

Tactic:
induction S, hS using Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa [closure_union, coe_sup] using hS'.1.closure.add (ih hS'.2)

Premises used: AddSubmonoid.closure_union, Insert.insert, forall_eq_or_imp, AddSubmonoid.coe_sup, Set.mem_insert_iff, IsSemilinearSet.empty
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
h : ∃ (t : Set M), t.Finite ∧ LinearIndepOn ℕ id t ∧ s = a +ᵥ (↑(closure t) : Set M)
t : Set M
ht : t.Finite
hs : LinearIndepOn ℕ id t ∧ s = a +ᵥ (↑(closure t) : Set M)
⊢ LinearIndepOn ℕ id (↑(ht.toFinset (s := t)) : Set M) ∧ s = a +ᵥ (↑(closure (↑(ht.toFinset (s := t)) : Set M)) : Set M)

Tactic:
simpa
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : IsProperLinearSet s
rcases : ∀ (a : M) (t : Set M) (ht : t.Finite), LinearIndepOn ℕ id t → IsLinearSet (a +ᵥ (↑(closure t) : Set M))
⊢ IsLinearSet s

Tactic:
rcases hs with ⟨a, t, ht, _, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
left : LinearIndepOn ℕ id t
⊢ IsLinearSet (a +ᵥ (↑(closure t) : Set M))

Tactic:
⟨a, t, ht, rfl⟩

Premises used: IsLinearSet, And.intro, Exists.intro, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
left : LinearIndepOn ℕ id t
⊢ IsLinearSet (a +ᵥ (↑(closure t) : Set M))

Tactic:
exact ⟨a, t, ht, rfl⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
⊢ Set.Finite.{u_1} (α := M) ∅ ∧ LinearIndepOn.{u_1, 0, u_1} (ι := M) ℕ id ∅ ∧ {a} = a +ᵥ (↑(closure ∅) : Set M)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
⊢ IsProperSemilinearSet s ↔ ∃ (S : Finset (Set M)), (∀ t ∈ S, IsProperLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set M))

Tactic:
Set.exists_finite_iff_finset

Premises used: IsProperSemilinearSet, Set.exists_finite_iff_finset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : IsProperSemilinearSet s
rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsProperLinearSet t), IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet s

Tactic:
rcases hs with ⟨S, hS, hS', rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
⊢ IsSemilinearSet (⋃₀ S)

Tactic:
⟨S, hS, fun s hs => (hS' s hs).isLinearSet, rfl⟩

Premises used: IsProperLinearSet.isLinearSet, IsSemilinearSet, And.intro, Exists.intro, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
⊢ IsSemilinearSet (⋃₀ S)

Tactic:
exact ⟨S, hS, fun s hs => (hS' s hs).isLinearSet, rfl⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : IsProperLinearSet s
⊢ Set.Finite (α := Set M) {s} ∧
    (∀ (t : Set M), Membership.mem (γ := Set (Set M)) {s} t → IsProperLinearSet t) ∧ s = ⋃₀ {s}

Tactic:
simpa
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
⊢ Set.Finite.{u_1} (α := Set M) ∅ ∧
    (∀ (t : Set M), Membership.mem (γ := Set (Set M)) ∅ t → IsProperLinearSet t) ∧ Eq.{u_1 + 1} (α := Set M) ∅ (⋃₀ ∅)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsProperSemilinearSet s₁
hs₂ : IsProperSemilinearSet s₂
rcases :
  ∀ (S₁ : Set (Set M)) (hS₁ : S₁.Finite) (hS₁' : ∀ t ∈ S₁, IsProperLinearSet t), IsProperSemilinearSet (⋃₀ S₁ ∪ s₂)
⊢ IsProperSemilinearSet (s₁ ∪ s₂)

Tactic:
rcases hs₁ with ⟨S₁, hS₁, hS₁', rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s₂ : Set M
hs₂ : IsProperSemilinearSet s₂
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
rcases :
  ∀ (S₂ : Set (Set M)) (hS₂ : S₂.Finite) (hS₂' : ∀ t ∈ S₂, IsProperLinearSet t), IsProperSemilinearSet (⋃₀ S₁ ∪ ⋃₀ S₂)
⊢ IsProperSemilinearSet (⋃₀ S₁ ∪ s₂)

Tactic:
rcases hs₂ with ⟨S₂, hS₂, hS₂', rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
rw : IsProperSemilinearSet (⋃₀ (S₁ ∪ S₂))
⊢ IsProperSemilinearSet (⋃₀ S₁ ∪ ⋃₀ S₂)

Tactic:
rw [← sUnion_union]

Premises used: Set.sUnion_union
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
⊢ IsProperSemilinearSet (⋃₀ (S₁ ∪ S₂))

Tactic:
⟨S₁ ∪ S₂, hS₁.union hS₂, fun s hs => ?_, rfl⟩

Premises used: Set.Finite.union, IsProperSemilinearSet, And.intro, Exists.intro, Union.union, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
refine : ∀ (s : Set M) (hs : s ∈ S₁ ∪ S₂), IsProperLinearSet s
⊢ IsProperSemilinearSet (⋃₀ (S₁ ∪ S₂))

Tactic:
refine ⟨S₁ ∪ S₂, hS₁.union hS₂, fun s hs => ?_, rfl⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
s : Set M
hs : s ∈ S₁ ∪ S₂
⊢ s ∈ S₁ ∨ s ∈ S₂

Tactic:
rw [mem_union] at hs

Premises used: Set.mem_union
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
s : Set M
hs : s ∈ S₁ ∨ s ∈ S₂
⊢ IsProperLinearSet s

Tactic:
hs.elim (hS₁' s) (hS₂' s)

Premises used: Or.elim
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsProperLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsProperLinearSet t
s : Set M
hs : s ∈ S₁ ∨ s ∈ S₂
⊢ IsProperLinearSet s

Tactic:
exact hs.elim (hS₁' s) (hS₂' s)

Premises used: Or.elim
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS' : ∀ (s : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsProperSemilinearSet s
⊢ IsProperSemilinearSet.{u_1} (M := M) (⋃₀ ∅)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
a : Set M
s : Set (Set M)
h : a ∉ s
hs : s.Finite
ih : ∀ (hS' : ∀ s_1 ∈ s, IsProperSemilinearSet s_1), IsProperSemilinearSet (⋃₀ s)
hS' : ∀ s_1 ∈ insert a s, IsProperSemilinearSet s_1
⊢ IsProperSemilinearSet a ∧ ∀ a ∈ s, IsProperSemilinearSet a

Tactic:
simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'

Premises used: forall_eq_or_imp, Set.mem_insert_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
a : Set M
s : Set (Set M)
h : a ∉ s
hs : s.Finite
ih : ∀ (hS' : ∀ s_1 ∈ s, IsProperSemilinearSet s_1), IsProperSemilinearSet (⋃₀ s)
hS' : IsProperSemilinearSet a ∧ ∀ a ∈ s, IsProperSemilinearSet a
⊢ IsProperSemilinearSet (⋃₀ insert a s)

Tactic:
simpa using hS'.1.union (ih hS'.2)

Premises used: IsProperSemilinearSet.union, And.right, And.left
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ s ∈ S, IsProperSemilinearSet s
empty :
  ∀ (hS' : ∀ (s : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsProperSemilinearSet s),
    IsProperSemilinearSet.{u_1} (M := M) (⋃₀ ∅)
insert :
  ∀ {a : Set M} {s : Set (Set M)},
    a ∉ s →
      s.Finite →
        ∀ (ih : ∀ (hS' : ∀ s_1 ∈ s, IsProperSemilinearSet s_1), IsProperSemilinearSet (⋃₀ s))
          (hS' : ∀ s_1 ∈ Insert.insert a s, IsProperSemilinearSet s_1), IsProperSemilinearSet (⋃₀ Insert.insert a s)
⊢ IsProperSemilinearSet (⋃₀ S)

Tactic:
induction S, hS using Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa using hS'.1.union (ih hS'.2)

Premises used: IsProperSemilinearSet.empty, Insert.insert, forall_eq_or_imp, Set.mem_insert_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
rw : IsProperSemilinearSet (⋃₀ (t '' s))
⊢ IsProperSemilinearSet.{u_1} (M := M) (⋃ i ∈ s, t i)

Tactic:
rw [← sUnion_image]

Premises used: Set.sUnion_image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
apply : ∀ s_1 ∈ t '' s, IsProperSemilinearSet s_1
⊢ IsProperSemilinearSet (⋃₀ (t '' s))

Tactic:
apply sUnion (hs.image t)

Premises used: IsProperSemilinearSet.sUnion, Set.Finite.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
⊢ ∀ s_1 ∈ t '' s, IsProperSemilinearSet s_1

Tactic:
simpa
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
s : Finset ι
t : ι → Set M
ht : ∀ i ∈ s, IsProperSemilinearSet (t i)
⊢ IsProperSemilinearSet.{u_1} (M := M) (⋃ i ∈ s, t i)

Tactic:
biUnion s.finite_toSet ht

Premises used: IsProperSemilinearSet.biUnion, Finset.finite_toSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : IsCancelAdd M
hs : IsLinearSet s
⊢ ∃ (a : M) (t : Finset M), s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)

Tactic:
rw [isLinearSet_iff] at hs

Premises used: isLinearSet_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : IsCancelAdd M
hs : ∃ (a : M) (t : Finset M), s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)
rcases : ∀ (a : M) (t : Finset M), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
⊢ IsProperSemilinearSet s

Tactic:
rcases hs with ⟨a, t, 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
h :
  ∀ (n : ℕ)
    (ih :
      ∀ m < n,
        ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M)))
    (a : M) (t : Finset M) (hn : t.card = n), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))

Tactic:
induction hn : t.card using Nat.strong_induction_on generalizing a t with | _ n ih

Premises used: Finset.card
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
n : ℕ
ih : ∀ m < n, ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
a : M
t : Finset M
hn : t.card = n
⊢ ∀ m < t.card,
    ∀ (a : M) (t : Finset M) (hn : t.card = m), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))

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))
pos : ∀ (hindep : LinearIndepOn ℕ id (↑t : Set M)), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
neg : ∀ (hindep : ¬LinearIndepOn ℕ id (↑t : Set M)), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
⊢ IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))

Tactic:
by_cases hindep : LinearIndepOn ℕ id (t : Set M)

Premises used: id, SetLike.coe, Nat, LinearIndepOn
-- 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 : Set M).Finite ∧
    LinearIndepOn ℕ id (↑t : Set M) ∧ a +ᵥ (↑(closure (↑t : Set M)) : Set M) = a +ᵥ (↑(closure (↑t : Set M)) : Set M)

Tactic:
simpa