awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
x : ι → ℕ
h :
  ¬(hs.fract (s := s) x = hs.base (s := s) ∧
        ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
          0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)) ↔
    hs.fract (s := s) x ≠ hs.base (s := s) ∨
      (hs.fract (s := s) x = hs.base (s := s) ∧
          ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), hs.floor (s := s) x i < 0) ∨
        hs.fract (s := s) x = hs.base (s := s) ∧
          ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧ 0 < hs.floor (s := s) x i
⊢ x ∈ sᶜ ↔ x ∈ hs.setOfFractNe (s := s) ∪ (hs.setOfFloorNeg (s := s) ∪ hs.setOfFloorPos (s := s))

Tactic:
simp only [mem_compl_iff, hs.mem_iff_fract_eq_and_floor_nonneg, IsProperLinearSet.setOfFractNe,
    IsProperLinearSet.setOfFloorNeg, IsProperLinearSet.setOfFloorPos, mem_union, mem_setOf_eq]

Premises used: Set.mem_union, _private.0.IsProperLinearSet.setOfFloorNeg, _private.0.IsProperLinearSet.setOfFloorPos, _private.0.IsProperLinearSet.setOfFractNe, Set.mem_setOf_eq, _private.0.IsProperLinearSet.mem_iff_fract_eq_and_floor_nonneg, Set.mem_compl_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsProperLinearSet s
x : ι → ℕ
⊢ ¬(hs.fract (s := s) x = hs.base (s := s) ∧
        ∀ (i : (↑(hs.basisSet (s := s)) : Type u_3)),
          0 ≤ hs.floor (s := s) x i ∧ ((↑i : ι → ℕ) ∉ hs.periods (s := s) → hs.floor (s := s) x i = 0)) ↔
    hs.fract (s := s) x ≠ hs.base (s := s) ∨
      (hs.fract (s := s) x = hs.base (s := s) ∧
          ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), hs.floor (s := s) x i < 0) ∨
        hs.fract (s := s) x = hs.base (s := s) ∧
          ∃ (i : (↑(hs.basisSet (s := s)) : Type u_3)), (↑i : ι → ℕ) ∉ hs.periods (s := s) ∧ 0 < hs.floor (s := s) x i

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSemilinearSet s
rcases :
  ∀ (S : Set (Set (ι → ℕ))) (hS : S.Finite) (hS' : ∀ t ∈ S, IsProperLinearSet t) (hs : IsSemilinearSet (⋃₀ S)),
    IsSemilinearSet (⋃₀ S)ᶜ
⊢ IsSemilinearSet sᶜ

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

Premises used: IsSemilinearSet.isProperSemilinearSet, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
simp_rw : IsSemilinearSet.{u_3} (M := ι → ℕ) (⋂ i ∈ S, iᶜ)
⊢ IsSemilinearSet (⋃₀ S)ᶜ

Tactic:
simp_rw [sUnion_eq_biUnion, compl_iUnion]

Premises used: Set.sUnion_eq_biUnion, Set.compl_iUnion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) (⋂ i ∈ S, iᶜ)

Tactic:
.biInter hS fun s hs => isSemilinearSet_compl_of_isProperLinearSet (hS' s hs)

Premises used: IsSemilinearSet.biInter, _private.0.Nat.isSemilinearSet_compl_of_isProperLinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) (⋂ i ∈ S, iᶜ)

Tactic:
exact .biInter hS fun s hs => isSemilinearSet_compl_of_isProperLinearSet (hS' s hs)
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
⊢ IsSemilinearSet (s₁ \ s₂)

Tactic:
isSemilinearSet_inter hs₁ (isSemilinearSet_compl hs₂)

Premises used: Set.Mem, Set.diff, setOf, _private.0.Nat.isSemilinearSet_inter, _private.0.Nat.isSemilinearSet_compl, Not
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
rcases :
  ∀ (P : AddSubmonoid M) (s₁' s₂' : Set ↥P) (hP : P.FG) (hs₁' : IsSemilinearSet s₁')
    (hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')) (hs₂' : IsSemilinearSet s₂')
    (hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')),
    IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁' \ Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
⊢ IsSemilinearSet (s₁ \ s₂)

Tactic:
rcases hs₁.exists_fg_eq_subtypeVal₂ hs₂ with ⟨P, s₁', s₂', hP, hs₁', rfl, hs₂', rfl⟩

Premises used: IsSemilinearSet.exists_fg_eq_subtypeVal₂, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
rw : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' (s₁' \ s₂'))
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁' \ Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')

Tactic:
rw [← image_diff Subtype.val_injective]

Premises used: Subtype.val_injective, Set.image_diff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
apply : IsSemilinearSet (s₁' \ s₂')
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' (s₁' \ s₂'))

Tactic:
apply image (f := P.subtype)

Premises used: AddSubmonoid.subtype, IsSemilinearSet.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : ∃ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P), Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
rcases :
  ∀ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P) (hf : Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤),
    IsSemilinearSet (s₁' \ s₂')
⊢ IsSemilinearSet (s₁' \ s₂')

Tactic:
rcases hP with ⟨n, f, hf⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
rw :
  IsSemilinearSet (M := ↥P)
    (Set.image (α := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ↥P)
      ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' \ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂'))
⊢ IsSemilinearSet (s₁' \ s₂')

Tactic:
rw [← image_preimage_eq (s₁' \ s₂') hf, preimage_diff]

Premises used: Set.image_preimage_eq, SDiff.sdiff, Set.preimage_diff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
hs : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' \ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
⊢ IsSemilinearSet (M := ↥P)
    (Set.image (α := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ↥P)
      ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' \ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂'))

Tactic:
apply image

Premises used: IsSemilinearSet.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
hs : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁')
hs₃ : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
⊢ IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' \ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')

Tactic:
apply Nat.isSemilinearSet_diff

Premises used: _private.0.Nat.isSemilinearSet_diff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : AddMonoid.FG M
hs : IsSemilinearSet s
rw : IsSemilinearSet (univ \ s)
⊢ IsSemilinearSet sᶜ

Tactic:
rw [compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : AddMonoid.FG M
hs : IsSemilinearSet s
⊢ IsSemilinearSet (univ \ s)

Tactic:
diff .univ hs

Premises used: IsSemilinearSet.diff, IsSemilinearSet.univ
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : AddMonoid.FG M
hs : IsSemilinearSet s
⊢ IsSemilinearSet (univ \ s)

Tactic:
exact diff .univ hs

Premises used: IsSemilinearSet.diff, IsSemilinearSet.univ
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
⊢ IsLinearSet s ↔ ∃ (a : M) (t : Finset M), s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)

Tactic:
simp [IsLinearSet, Finset.exists]

Premises used: IsLinearSet, Finset.exists
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
⊢ Set.Finite.{u_1} (α := M) ∅ ∧ {a} = a +ᵥ (↑(closure ∅) : Set M)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Finset M
⊢ (↑s : Set M).Finite ∧ (↑(closure (↑s : Set M)) : Set M) = HVAdd.hVAdd (α := M) 0 (↑(closure (↑s : Set M)) : Set M)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : s.Finite
⊢ (↑(closure s) : Set M) = HVAdd.hVAdd (α := M) 0 (↑(closure s) : Set M)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
h : ∃ (P : AddSubmonoid M), P.FG ∧ s = a +ᵥ (↑P : Set M)
P : AddSubmonoid M
t : Finset M
hP : closure (↑t : Set M) = P
hs rwa rwa₁ rwa₂ rwa₃ : s = a +ᵥ (↑P : Set M)
⊢ s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)

Tactic:
rwa [hP]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
hP : P.FG
rw : ∃ (a : M) (P_1 : AddSubmonoid M), P_1.FG ∧ (↑P : Set M) = a +ᵥ (↑P_1 : Set M)
⊢ IsLinearSet (↑P : Set M)

Tactic:
rw [isLinearSet_iff_exists_fg_eq_vadd]

Premises used: isLinearSet_iff_exists_fg_eq_vadd
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
hP : P.FG
⊢ (↑P : Set M) = HVAdd.hVAdd (α := M) 0 (↑P : Set M)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
hP : P.FG
⊢ ∃ (a : M) (P_1 : AddSubmonoid M), P_1.FG ∧ (↑P : Set M) = a +ᵥ (↑P_1 : Set M)

Tactic:
exact ⟨0, P, hP, by simp⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
⊢ IsLinearSet.{u_1} (M := M) univ

Tactic:
of_fg AddMonoid.FG.fg_top

Premises used: Set.univ, setOf, AddMonoid.FG.fg_top, IsLinearSet.of_fg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
hs : IsLinearSet s
rcases : ∀ (b : M) (t : Set M) (ht : t.Finite), IsLinearSet (a +ᵥ b +ᵥ (↑(closure t) : Set M))
⊢ IsLinearSet (a +ᵥ s)

Tactic:
rcases hs with ⟨b, t, ht, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a b : M
t : Set M
ht : t.Finite
rw rw₁ : (a + b) +ᵥ (↑(closure t) : Set M) = (a + b) +ᵥ (↑(closure t) : Set M)
⊢ a +ᵥ b +ᵥ (↑(closure t) : Set M) = (a + b) +ᵥ (↑(closure t) : Set M)

Tactic:
rw [vadd_vadd]

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

Tactic:
exact ⟨a + b, t, ht, by rw [vadd_vadd]⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
rcases : ∀ (a : M) (t₁ : Set M) (ht₁ : t₁.Finite), IsLinearSet ((a +ᵥ (↑(closure t₁) : Set M)) + s₂)
⊢ IsLinearSet (s₁ + 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
s₂ : Set M
hs₂ : IsLinearSet s₂
a : M
t₁ : Set M
ht₁ : t₁.Finite
rcases :
  ∀ (b : M) (t₂ : Set M) (ht₂ : t₂.Finite),
    IsLinearSet ((a +ᵥ (↑(closure t₁) : Set M)) + (b +ᵥ (↑(closure t₂) : Set M)))
⊢ IsLinearSet ((a +ᵥ (↑(closure t₁) : Set M)) + s₂)

Tactic:
rcases hs₂ with ⟨b, 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
b : M
t₂ : Set M
ht₂ : t₂.Finite
⊢ (a +ᵥ (↑(closure t₁) : Set M)) + (b +ᵥ (↑(closure t₂) : Set M)) = (a + b) +ᵥ (↑(closure (t₁ ∪ t₂)) : Set M)

Tactic:
simp [vadd_add_vadd, closure_union, coe_sup]

Premises used: vadd_add_vadd, AddSubmonoid.closure_union, AddSubmonoid.coe_sup
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t₁ : Set M
ht₁ : t₁.Finite
b : M
t₂ : Set M
ht₂ : t₂.Finite
⊢ IsLinearSet ((a +ᵥ (↑(closure t₁) : Set M)) + (b +ᵥ (↑(closure t₂) : Set M)))

Tactic:
exact ⟨a + b, t₁ ∪ t₂, ht₁.union ht₂, by simp [vadd_add_vadd, closure_union, coe_sup]⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
s : Set M
hs : IsLinearSet s
f : F
rcases :
  ∀ (a : M) (t : Set M) (ht : t.Finite),
    IsLinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' (a +ᵥ (↑(closure t) : Set M)))
⊢ IsLinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)

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

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
a : M
t : Set M
ht : t.Finite
⊢ IsLinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' (a +ᵥ (↑(closure t) : Set M)))

Tactic:
⟨f a, f '' t, ht.image f, ?_⟩

Premises used: Set.Finite.image, IsLinearSet, And.intro, Exists.intro, Set.image, DFunLike.coe
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
a : M
t : Set M
ht : t.Finite
refine :
  (⇑f : (a : M) → N) '' (a +ᵥ (↑(closure t) : Set M)) =
    HVAdd.hVAdd (α := N) ((f : (a : M) → N) a : N) (↑(closure ((⇑f : (a : M) → N) '' t)) : Set N)
⊢ IsLinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' (a +ᵥ (↑(closure t) : Set M)))

Tactic:
refine ⟨f a, f '' t, ht.image f, ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
a : M
t : Set M
ht : t.Finite
⊢ (⇑f : (a : M) → N) '' (a +ᵥ (↑(closure t) : Set M)) =
    HVAdd.hVAdd (α := N) ((f : (a : M) → N) a : N) (↑(closure ((⇑f : (a : M) → N) '' t)) : Set N)

Tactic:
simp [image_vadd_distrib, ← AddMonoidHom.map_mclosure]

Premises used: AddMonoidHom.map_mclosure, Set.image_vadd_distrib
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
⊢ IsSemilinearSet s ↔ ∃ (S : Finset (Set M)), (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set M))

Tactic:
Set.exists_finite_iff_finset

Premises used: IsSemilinearSet, Set.exists_finite_iff_finset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
h : IsLinearSet s
⊢ Set.Finite (α := Set M) {s} ∧ (∀ (t : Set M), Membership.mem (γ := Set (Set M)) {s} t → IsLinearSet 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 → IsLinearSet t) ∧ Eq.{u_1 + 1} (α := Set M) ∅ (⋃₀ ∅)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
⊢ IsSemilinearSet (M := M) {a}

Tactic:
(IsLinearSet.singleton a).isSemilinearSet

Premises used: IsLinearSet.isSemilinearSet, IsLinearSet.singleton
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Finset M
⊢ IsSemilinearSet (↑(closure (↑s : Set M)) : Set M)

Tactic:
(IsLinearSet.closure_finset s).isSemilinearSet

Premises used: IsLinearSet.closure_finset, IsLinearSet.isSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : s.Finite
⊢ IsSemilinearSet (↑(closure s) : Set M)

Tactic:
(IsLinearSet.closure_of_finite hs).isSemilinearSet

Premises used: IsLinearSet.closure_of_finite, IsLinearSet.isSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
hP : P.FG
⊢ IsSemilinearSet (↑P : Set M)

Tactic:
(IsLinearSet.of_fg hP).isSemilinearSet

Premises used: IsLinearSet.of_fg, IsLinearSet.isSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
⊢ IsSemilinearSet.{u_1} (M := M) univ

Tactic:
IsLinearSet.univ.isSemilinearSet

Premises used: IsLinearSet.univ, IsLinearSet.isSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
rcases : ∀ (S₁ : Set (Set M)) (hS₁ : S₁.Finite) (hS₁' : ∀ t ∈ S₁, IsLinearSet t), IsSemilinearSet (⋃₀ S₁ ∪ s₂)
⊢ IsSemilinearSet (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₂ : IsSemilinearSet s₂
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
rcases : ∀ (S₂ : Set (Set M)) (hS₂ : S₂.Finite) (hS₂' : ∀ t ∈ S₂, IsLinearSet t), IsSemilinearSet (⋃₀ S₁ ∪ ⋃₀ S₂)
⊢ IsSemilinearSet (⋃₀ 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₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
rw : IsSemilinearSet (⋃₀ (S₁ ∪ S₂))
⊢ IsSemilinearSet (⋃₀ 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₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ (S₁ ∪ S₂))

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

Premises used: Set.Finite.union, IsSemilinearSet, 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₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
refine : ∀ (s : Set M) (hs : s ∈ S₁ ∪ S₂), IsLinearSet s
⊢ IsSemilinearSet (⋃₀ (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₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet 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₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
s : Set M
hs : s ∈ S₁ ∨ s ∈ S₂
⊢ IsLinearSet 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₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
s : Set M
hs : s ∈ S₁ ∨ s ∈ S₂
⊢ IsLinearSet 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 → IsSemilinearSet s
⊢ IsSemilinearSet.{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, IsSemilinearSet s_1), IsSemilinearSet (⋃₀ s)
hS' : ∀ s_1 ∈ insert a s, IsSemilinearSet s_1
⊢ IsSemilinearSet a ∧ ∀ a ∈ s, IsSemilinearSet 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, IsSemilinearSet s_1), IsSemilinearSet (⋃₀ s)
hS' : IsSemilinearSet a ∧ ∀ a ∈ s, IsSemilinearSet a
⊢ IsSemilinearSet (⋃₀ insert a s)

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

Premises used: And.right, And.left, IsSemilinearSet.union
-- 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, IsSemilinearSet s
empty :
  ∀ (hS' : ∀ (s : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsSemilinearSet s),
    IsSemilinearSet.{u_1} (M := M) (⋃₀ ∅)
insert :
  ∀ {a : Set M} {s : Set (Set M)},
    a ∉ s →
      s.Finite →
        ∀ (ih : ∀ (hS' : ∀ s_1 ∈ s, IsSemilinearSet s_1), IsSemilinearSet (⋃₀ s))
          (hS' : ∀ s_1 ∈ Insert.insert a s, IsSemilinearSet s_1), IsSemilinearSet (⋃₀ Insert.insert a s)
⊢ IsSemilinearSet (⋃₀ 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: Insert.insert, forall_eq_or_imp, Set.mem_insert_iff, IsSemilinearSet.empty