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))
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 :
  (∃ (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
⊢ 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

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)
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

Tactic:
⟨k • j + y,
        add_mem (nsmul_mem (mem_closure_of_mem (ht' hj)) _)
          ((closure_mono (t.erase_subset j)) hy), ?_⟩

Premises used: nsmul_mem, AddSubmonoid.mem_closure_of_mem, HAdd.hAdd, And.intro, Exists.intro, AddMemClass.add_mem, HSMul.hSMul, Finset.erase_subset, AddSubmonoid.closure_mono
-- 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)
j : M
hj : j ∈ t'
k : ℕ
hk : k < f j
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (↑(t.erase j) : Set M)) y
h : a + (k • j + y) = a + k • j + y
⊢ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (↑t : Set M)) y_1 ∧ a + y_1 = 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), ?_⟩
-- 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)
j : M
hj : j ∈ t'
k : ℕ
hk : k < f j
y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (↑(t.erase j) : Set M)) y
h h₁ : a + (k • j + y) = a + (k • j + y)
⊢ a + (k • j + y) = a + k • j + y

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- 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)
⊢ IsProperSemilinearSet.{u_1} (M := M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))

Tactic:
.biUnion_finset fun j hj => .biUnion_finset fun k hk =>
      ih _ (Finset.card_lt_card (Finset.erase_ssubset (ht' hj))) _ _ rfl

Premises used: IsProperSemilinearSet.biUnion_finset, HAdd.hAdd, Finset.card_lt_card, Finset.card, HSMul.hSMul, Finset.erase, Finset.erase_ssubset, 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)
⊢ IsProperSemilinearSet.{u_1} (M := M)
    (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ (↑(closure (↑(t.erase j) : Set M)) : Set M))

Tactic:
exact .biUnion_finset fun j hj => .biUnion_finset fun k hk =>
      ih _ (Finset.card_lt_card (Finset.erase_ssubset (ht' hj))) _ _ rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : IsCancelAdd M
hs : IsSemilinearSet s
rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t), IsProperSemilinearSet (⋃₀ S)
⊢ IsProperSemilinearSet 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
inst_1 : IsCancelAdd M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
simp_rw : IsProperSemilinearSet.{u_1} (M := M) (⋃ i ∈ S, i)
⊢ IsProperSemilinearSet (⋃₀ S)

Tactic:
simp_rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsProperSemilinearSet.{u_1} (M := M) (⋃ i ∈ S, i)

Tactic:
IsProperSemilinearSet.biUnion hS fun s hs => (hS' s hs).isProperSemilinearSet

Premises used: IsProperSemilinearSet.biUnion, IsLinearSet.isProperSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : IsCancelAdd M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsProperSemilinearSet.{u_1} (M := M) (⋃ i ∈ S, i)

Tactic:
exact IsProperSemilinearSet.biUnion hS fun s hs => (hS' s hs).isProperSemilinearSet

Premises used: IsProperSemilinearSet.biUnion, IsLinearSet.isProperSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
mp : IsSemilinearSet s → ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
mpr : (∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s) → IsSemilinearSet s
⊢ IsSemilinearSet s ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
hs : IsSemilinearSet s
⊢ IsProperSemilinearSet s

Tactic:
apply IsSemilinearSet.isProperSemilinearSet at hs

Premises used: IsSemilinearSet.isProperSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
hs : IsProperSemilinearSet s
⊢ ∃ (S : Finset (Set ℕ)), (∀ t ∈ S, IsProperLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set ℕ))

Tactic:
rw [isProperSemilinearSet_iff] at hs

Premises used: isProperSemilinearSet_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
hs : ∃ (S : Finset (Set ℕ)), (∀ t ∈ S, IsProperLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set ℕ))
mp :
  ∀ (S : Finset (Set ℕ)) (hS : ∀ t ∈ S, IsProperLinearSet t),
    ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + p ∈ ⋃₀ (↑S : Set (Set ℕ))
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s

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

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
t : Set ℕ
ht : t ∈ S
⊢ IsProperLinearSet t

Tactic:
apply hS at ht
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
t : Set ℕ
ht : IsProperLinearSet t
⊢ ∃ (a : ℕ) (t_1 : Finset ℕ), LinearIndepOn ℕ id (↑t_1 : Set ℕ) ∧ t = a +ᵥ (↑(closure (↑t_1 : Set ℕ)) : Set ℕ)

Tactic:
rw [isProperLinearSet_iff] at ht

Premises used: isProperLinearSet_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
t : Set ℕ
ht : ∃ (a : ℕ) (t_1 : Finset ℕ), LinearIndepOn ℕ id (↑t_1 : Set ℕ) ∧ t = a +ᵥ (↑(closure (↑t_1 : Set ℕ)) : Set ℕ)
rcases :
  ∀ (a : ℕ) (t : Finset ℕ) (ht : LinearIndepOn ℕ id (↑t : Set ℕ)),
    ∃ (k : ℕ),
      ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ)
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t

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

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id (↑t : Set ℕ)
⊢ t.card ≤ 1

Tactic:
simpa [CommSemiring.rank_self] using ht.cardinal_le_rank

Premises used: CommSemiring.rank_self, LinearIndependent.cardinal_le_rank
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id (↑t : Set ℕ)
⊢ t.card ≤ 1

Tactic:
have hcard : t.card ≤ 1 := by simpa [CommSemiring.rank_self] using ht.cardinal_le_rank
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id (↑t : Set ℕ)
hcard : t.card ≤ 1
⊢ ∃ (x : ℕ), t = ∅ ∨ t = {x}

Tactic:
simp_rw [Finset.card_le_one_iff_subset_singleton, Finset.subset_singleton_iff] at hcard

Premises used: Finset.card_le_one_iff_subset_singleton, Finset.subset_singleton_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id (↑t : Set ℕ)
hcard : ∃ (x : ℕ), t = ∅ ∨ t = {x}
inl :
  ∀ (b : ℕ) (ht : LinearIndepOn ℕ id (↑∅ : Set ℕ)),
    ∃ (k : ℕ),
      ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ)
inr :
  ∀ (b : ℕ) (ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)),
    ∃ (k : ℕ),
      ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ)
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ)

Tactic:
rcases hcard with ⟨b, (rfl | rfl)⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑∅ : Set ℕ)
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ)

Tactic:
⟨a + 1, 1, zero_lt_one, fun x hx => ?_⟩

Premises used: zero_lt_one, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑∅ : Set ℕ)
inl :
  ∀ (x : ℕ) (hx : x ≥ a + 1),
    x ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ) ↔ x + 1 ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ)
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ)

Tactic:
refine ⟨a + 1, 1, zero_lt_one, fun x hx => ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑∅ : Set ℕ)
x : ℕ
hx : x ≥ a + 1
⊢ x ≠ a

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑∅ : Set ℕ)
x : ℕ
hx : x ≥ a + 1
⊢ x + 1 ≠ a

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
⊢ b ≠ 0

Tactic:
simpa [ne_comm] using ht.zero_notMem_image

Premises used: LinearIndepOn.zero_notMem_image, ne_comm
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
⊢ b ≠ 0

Tactic:
have hb : b ≠ 0 := by simpa [ne_comm] using ht.zero_notMem_image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : b ≠ 0
⊢ 0 < b

Tactic:
rw [Nat.ne_zero_iff_zero_lt] at hb

Premises used: Nat.ne_zero_iff_zero_lt
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ)

Tactic:
⟨a, b, hb, fun x hx => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
inr :
  ∀ (x : ℕ) (hx : x ≥ a),
    x ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ) ↔ x + b ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ)
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ)

Tactic:
refine ⟨a, b, hb, fun x hx => ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : x ≥ a
inr : (∃ (a_1 : ℕ), a + a_1 * b = x) ↔ ∃ (a_1 : ℕ), a + a_1 * b = x + b
⊢ x ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ) ↔ x + b ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ)

Tactic:
simp only [Finset.coe_singleton, mem_vadd_set, SetLike.mem_coe,
          AddSubmonoid.mem_closure_singleton, smul_eq_mul, vadd_eq_add, exists_exists_eq_and]

Premises used: Finset.coe_singleton, Set.mem_vadd_set, exists_exists_eq_and, SetLike.mem_coe, vadd_eq_add, smul_eq_mul, AddSubmonoid.mem_closure_singleton
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : x ≥ a
inr : (∃ (a_1 : ℕ), a + a_1 * b = x) → ∃ (a_2 : ℕ), a + a_2 * b = x + b
inr₁ : (∃ (a_1 : ℕ), a + a_1 * b = x + b) → ∃ (a_2 : ℕ), a + a_2 * b = x
⊢ (∃ (a_1 : ℕ), a + a_1 * b = x) ↔ ∃ (a_1 : ℕ), a + a_1 * b = x + b

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : a + x * b ≥ a
⊢ a + (x + 1) * b = a + x * b + b

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : a + x * b ≥ a
⊢ ∃ (a_1 : ℕ), a + a_1 * b = a + x * b + b

Tactic:
exact ⟨x + 1, by grind⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : x ≥ a
heq : a + 0 * b = x + b
⊢ a + 0 * b = x

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : x ≥ a
heq : a + 0 * b = x + b
⊢ ∃ (a_1 : ℕ), a + a_1 * b = x

Tactic:
exact ⟨0, by grind⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : x ≥ a
y : ℕ
heq : a + (y + 1) * b = x + b
⊢ a + y * b = x

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : x ≥ a
y : ℕ
heq : a + (y + 1) * b = x + b
⊢ ∃ (a_1 : ℕ), a + a_1 * b = x

Tactic:
exact ⟨y, by grind⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : x ≥ a
y : ℕ
heq : a + y * b = x + b
inr : ∀ (heq : a + 0 * b = x + b), ∃ (a_1 : ℕ), a + a_1 * b = x
inr₁ : ∀ (y : ℕ) (heq : a + (y + 1) * b = x + b), ∃ (a_1 : ℕ), a + a_1 * b = x
⊢ ∃ (a_1 : ℕ), a + a_1 * b = x

Tactic:
cases y with
          | zero => exact ⟨0, by grind⟩
          | succ y => exact ⟨y, by grind⟩

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
⊢ ∀ t ∈ S, ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t

Tactic:
replace hS : ∀ t ∈ S, ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t := by
      intro t ht
      apply hS at ht
      rw [isProperLinearSet_iff] at ht
      rcases ht with ⟨a, t, ht, rfl⟩
      have hcard : t.card ≤ 1 := by simpa [CommSemiring.rank_self] using ht.cardinal_le_rank
      simp_rw [Finset.card_le_one_iff_subset_singleton, Finset.subset_singleton_iff] at hcard
      rcases hcard with ⟨b, (rfl | rfl)⟩
      · refine ⟨a + 1, 1, zero_lt_one, fun x hx => ?_⟩
        simp [(by grind : x ≠ a), (by grind : x + 1 ≠ a)]
      · have hb : b ≠ 0 := by simpa [ne_comm] using ht.zero_notMem_image
        rw [Nat.ne_zero_iff_zero_lt] at hb
        refine ⟨a, b, hb, fun x hx => ?_⟩
        simp only [Finset.coe_singleton, mem_vadd_set, SetLike.mem_coe,
          AddSubmonoid.mem_closure_singleton, smul_eq_mul, vadd_eq_add, exists_exists_eq_and]
        constructor
        · rintro ⟨x, rfl⟩
          exact ⟨x + 1, by grind⟩
        · rintro ⟨y, heq⟩
          cases y with
          | zero => exact ⟨0, by grind⟩
          | succ y => exact ⟨y, by grind⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t
mp :
  ∀ (k p : (t : Set ℕ) → ℕ) (hS : ∀ t ∈ S, p t > 0) (hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t),
    ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + p ∈ ⋃₀ (↑S : Set (Set ℕ))
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + p ∈ ⋃₀ (↑S : Set (Set ℕ))

Tactic:
choose! k p hS hS' using hS
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + p ∈ ⋃₀ (↑S : Set (Set ℕ))

Tactic:
⟨S.sup k, S.lcm p, ?_, fun x hx => ?_⟩

Premises used: And.intro, Exists.intro, Finset.sup, Finset.lcm
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
mp : S.lcm p > 0
mp₁ : ∀ (x : ℕ) (hx : x ≥ S.sup k), x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + S.lcm p ∈ ⋃₀ (↑S : Set (Set ℕ))
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + p ∈ ⋃₀ (↑S : Set (Set ℕ))

Tactic:
refine ⟨S.sup k, S.lcm p, ?_, fun x hx => ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
⊢ S.lcm p > 0

Tactic:
grind [Finset.lcm_eq_zero_iff]

Premises used: Finset.lcm_eq_zero_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
⊢ (∃ t ∈ S, x ∈ t) ↔ ∃ t ∈ S, x + S.lcm p ∈ t

Tactic:
exists_congr fun t => and_congr_right fun ht => ?_

Premises used: and_congr_right, exists_congr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
mp : ∀ (t : Set ℕ) (ht : t ∈ S), x ∈ t ↔ x + S.lcm p ∈ t
⊢ (∃ t ∈ S, x ∈ t) ↔ ∃ t ∈ S, x + S.lcm p ∈ t

Tactic:
refine exists_congr fun t => and_congr_right fun ht => ?_

Premises used: and_congr_right, exists_congr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
⊢ p t ∣ S.lcm p

Tactic:
have hpt : p t ∣ S.lcm p := Finset.dvd_lcm ht
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
hpt : p t ∣ S.lcm p
⊢ ∃ (c : ℕ), S.lcm p = c * p t

Tactic:
rw [dvd_iff_exists_eq_mul_left] at hpt

Premises used: dvd_iff_exists_eq_mul_left
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
hpt : ∃ (c : ℕ), S.lcm p = c * p t
mp : ∀ (m : ℕ) (hpt : S.lcm p = m * p t), x ∈ t ↔ x + S.lcm p ∈ t
⊢ x ∈ t ↔ x + S.lcm p ∈ t

Tactic:
rcases hpt with ⟨m, hpt⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
m : ℕ
hpt : S.lcm p = m * p t
mp : x ∈ t ↔ x + m * p t ∈ t
⊢ x ∈ t ↔ x + S.lcm p ∈ t

Tactic:
rw [hpt]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
⊢ x ∈ t ↔ x + 0 * p t ∈ t

Tactic:
grind [Finset.sup_le_iff]

Premises used: Finset.sup_le_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
n : ℕ
h : x ∈ t ↔ x + n * p t ∈ t
⊢ x ∈ t ↔ x + (n + 1) * p t ∈ t

Tactic:
grind [Finset.sup_le_iff]

Premises used: Finset.sup_le_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
S : Finset (Set ℕ)
k p : (t : Set ℕ) → ℕ
hS : ∀ t ∈ S, p t > 0
hS' : ∀ t ∈ S, ∀ x ≥ k t, x ∈ t ↔ x + p t ∈ t
x : ℕ
hx : x ≥ S.sup k
t : Set ℕ
ht : t ∈ S
m : ℕ
mp : x ∈ t ↔ x + 0 * p t ∈ t
mp₁ : ∀ (n : ℕ), (x ∈ t ↔ x + n * p t ∈ t) → (x ∈ t ↔ x + (n + 1) * p t ∈ t)
⊢ x ∈ t ↔ x + m * p t ∈ t

Tactic:
induction m with grind [Finset.sup_le_iff]

Premises used: Finset.sup_le_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
⊢ Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}

Tactic:
have h₁ : {x ∈ s | x < k}.Finite := (Set.finite_lt_nat k).subset (sep_subset_setOf _ _)
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
⊢ Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}

Tactic:
have h₂ : {x ∈ s | k ≤ x ∧ x < k + p}.Finite :=
      (Set.finite_Ico k (k + p)).subset (sep_subset_setOf _ _)