awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : IsCancelAdd M
hs : IsLinearSet s
rw rw₁ rw₂ : ∀ (hs : ∃ (a : M) (t : Finset M), s = a +ᵥ (↑(closure (↑t : Set M)) : Set M)), IsProperSemilinearSet s
rw₃ : ∀ (a : M) (t : Finset M), IsProperSemilinearSet (a +ᵥ (↑(closure (↑t : Set M)) : Set M))
⊢ IsProperSemilinearSet s
have 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))
Tactic: classical
  rw [isLinearSet_iff] at hs
  rcases hs with ⟨a, t, rfl⟩
  induction hn : t.card using Nat.strong_induction_on generalizing a t with | _ n ih
  subst hn
  by_cases hindep : LinearIndepOn ℕ id (t : Set M)
  · exact IsProperLinearSet.isProperSemilinearSet ⟨a, t, by simpa⟩
  rw [not_linearIndepOn_finset_iffₒₛ] at hindep
  rcases hindep with ⟨t', ht', f, heq, i, hi, hfi⟩
  simp only [Function.id_def] at heq
  convert_to IsProperSemilinearSet (⋃ j ∈ t', ⋃ k ∈ Finset.range (f j),
    (a + k • j) +ᵥ (closure (t.erase j : Set M) : Set M))
  · ext x
    simp only [mem_vadd_set, SetLike.mem_coe]
    constructor
    · rintro ⟨y, hy, rfl⟩
      rw [mem_closure_finset] at hy
      rcases hy with ⟨g, -, rfl⟩
      induction hn : g i using Nat.strong_induction_on generalizing g with | _ n ih'
      subst hn
      by_cases! hfg : ∀ j ∈ t', f j ≤ g j
      · convert!
        ih' (g i - f i) (Nat.sub_lt_self hfi (hfg i hi))
          (fun j => if j ∈ t' then g j - f j else g j + f j) (by simp [hi]) using 1
        conv_lhs => rw [← Finset.union_sdiff_of_subset ht']
        simp_rw [vadd_eq_add, add_left_cancel_iff, Finset.sum_union Finset.sdiff_disjoint.symm,
          ite_smul, Finset.sum_ite, Finset.filter_mem_eq_inter, Finset.inter_eq_right.2 ht',
          Finset.filter_notMem_eq_sdiff, add_smul, Finset.sum_add_distrib, ← heq, ← add_assoc,
          add_right_comm, ← Finset.sum_add_distrib]
        congr! 2 with j hj
        rw [← add_smul, tsub_add_cancel_of_le (hfg j hj)]
      · rcases hfg with ⟨j, hj, hgj⟩
        simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
        refine ⟨j, hj, g j, hgj, ∑ k ∈ t.erase j, g k • k,
          sum_mem fun x hx => (nsmul_mem (mem_closure_of_mem hx) _), ?_⟩
        rw [← Finset.sum_erase_add _ _ (ht' hj), ← add_assoc, add_right_comm]
    · simp only [mem_iUnion, Finset.mem_range, mem_vadd_set, SetLike.mem_coe, vadd_eq_add]
      rintro ⟨j, hj, k, hk, y, hy, rfl⟩
      refine ⟨k • j + y,
        add_mem (nsmul_mem (mem_closure_of_mem (ht' hj)) _)
          ((closure_mono (t.erase_subset j)) hy), ?_⟩
      rw [add_assoc]
  · exact .biUnion_finset fun j hj => .biUnion_finset fun k hk =>
      ih _ (Finset.card_lt_card (Finset.erase_ssubset (ht' hj))) _ _ rfl
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
inst_1 : IsCancelAdd M
hs : IsSemilinearSet s
⊢ IsProperSemilinearSet s
have rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t), IsProperSemilinearSet (⋃₀ S)
Tactic: rcases hs with ⟨S, hS, hS', rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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 (⋃₀ S)
have simp_rw : IsProperSemilinearSet.{u_1} (M := M) (⋃ i ∈ S, i)
Tactic: simp_rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
⊢ IsSemilinearSet s ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
have mp : IsSemilinearSet s → ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
mp : IsSemilinearSet s → ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
⊢ IsSemilinearSet s ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
have mpr : (∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s) → IsSemilinearSet s
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
s : Set ℕ
hs : IsSemilinearSet s
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
have hs₁ : IsProperSemilinearSet s
Tactic: apply IsSemilinearSet.isProperSemilinearSet at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
s : Set ℕ
hs : IsProperSemilinearSet s
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
have hs₁ : ∃ (S : Finset (Set ℕ)), (∀ t ∈ S, IsProperLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set ℕ))
Tactic: rw [isProperSemilinearSet_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
hs : ∃ (S : Finset (Set ℕ)), (∀ t ∈ S, IsProperLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set ℕ))
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
have mp : ∀ (S : Finset (Set ℕ)) (hS : ∀ t ∈ S, IsProperLinearSet t),
  ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + p ∈ ⋃₀ (↑S : Set (Set ℕ))
Tactic: rcases hs with ⟨S, hS, rfl⟩
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
t : Set ℕ
ht : t ∈ S
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t
have ht₁ : IsProperLinearSet t
Tactic: apply hS at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
t : Set ℕ
ht : IsProperLinearSet t
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t
have ht₁ : ∃ (a : ℕ) (t_1 : Finset ℕ), LinearIndepOn ℕ id (↑t_1 : Set ℕ) ∧ t = a +ᵥ (↑(closure (↑t_1 : Set ℕ)) : Set ℕ)
Tactic: rw [isProperLinearSet_iff] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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 ℕ)
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t
have 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 ℕ)
Tactic: rcases ht with ⟨a, t, ht, rfl⟩
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
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 ℕ)
have hcard : t.card ≤ 1
Tactic: have hcard : t.card ≤ 1 := by simpa [CommSemiring.rank_self] using ht.cardinal_le_rank
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id (↑t : Set ℕ)
hcard : t.card ≤ 1
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ)
have hcard₁ : ∃ (x : ℕ), t = ∅ ∨ t = {x}
Tactic: simp_rw [Finset.card_le_one_iff_subset_singleton, Finset.subset_singleton_iff] at hcard
Cleared hypotheses: hcard
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a : ℕ
t : Finset ℕ
ht : LinearIndepOn ℕ id (↑t : Set ℕ)
hcard : ∃ (x : ℕ), t = ∅ ∨ t = {x}
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ)
have inl : ∀ (b : ℕ) (ht : LinearIndepOn ℕ id (↑∅ : Set ℕ)),
  ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ)
Tactic: rcases hcard with ⟨b, (rfl | rfl)⟩
Cleared hypotheses: t, ht, hcard
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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 ℕ)
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑t : Set ℕ)) : Set ℕ)
have 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 ℕ)
Tactic: rcases hcard with ⟨b, (rfl | rfl)⟩
Cleared hypotheses: t, ht, hcard
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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 ℕ)
have inl : ∀ (x : ℕ) (hx : x ≥ a + 1), x ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ) ↔ x + 1 ∈ a +ᵥ (↑(closure (↑∅ : Set ℕ)) : Set ℕ)
Tactic: refine ⟨a + 1, 1, zero_lt_one, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ)
have hb : b ≠ 0
Tactic: have hb : b ≠ 0 := by simpa [ne_comm] using ht.zero_notMem_image
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : b ≠ 0
⊢ ∃ (k : ℕ),
    ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ) ↔ x + p ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ)
have hb₁ : 0 < b
Tactic: rw [Nat.ne_zero_iff_zero_lt] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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 ℕ)
have inr : ∀ (x : ℕ) (hx : x ≥ a), x ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ) ↔ x + b ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ)
Tactic: refine ⟨a, b, hb, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : x ≥ a
⊢ x ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ) ↔ x + b ∈ a +ᵥ (↑(closure (↑{b} : Set ℕ)) : Set ℕ)
have inr : (∃ (a_1 : ℕ), a + a_1 * b = x) ↔ ∃ (a_1 : ℕ), a + a_1 * b = x + b
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]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id (↑{b} : Set ℕ)
hb : 0 < b
x : ℕ
hx : x ≥ a
⊢ (∃ (a_1 : ℕ), a + a_1 * b = x) ↔ ∃ (a_1 : ℕ), a + a_1 * b = x + b
have inr : (∃ (a_1 : ℕ), a + a_1 * b = x) → ∃ (a_2 : ℕ), a + a_2 * b = x + b
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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
⊢ (∃ (a_1 : ℕ), a + a_1 * b = x) ↔ ∃ (a_1 : ℕ), a + a_1 * b = x + b
have inr₁ : (∃ (a_1 : ℕ), a + a_1 * b = x + b) → ∃ (a_2 : ℕ), a + a_2 * b = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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
⊢ ∃ (a_1 : ℕ), a + a_1 * b = x
have inr : ∀ (heq : a + 0 * b = x + b), ∃ (a_1 : ℕ), a + a_1 * b = x
Tactic: cases y with
          | zero => exact ⟨0, by grind⟩
          | succ y => exact ⟨y, by grind⟩
Cleared hypotheses: y, heq
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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
⊢ ∃ (a_1 : ℕ), a + a_1 * b = x
have inr₁ : ∀ (y : ℕ) (heq : a + (y + 1) * b = x + b), ∃ (a_1 : ℕ), a + a_1 * b = x
Tactic: cases y with
          | zero => exact ⟨0, by grind⟩
          | succ y => exact ⟨y, by grind⟩
Cleared hypotheses: y, heq
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + p ∈ ⋃₀ (↑S : Set (Set ℕ))
have hS₁ : ∀ 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⟩
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
S : Finset (Set ℕ)
hS : ∀ t ∈ S, ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ t ↔ x + p ∈ t
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + p ∈ ⋃₀ (↑S : Set (Set ℕ))
have 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 ℕ))
Tactic: choose! k p hS hS' using hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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 ℕ))
have mp : S.lcm p > 0
Tactic: refine ⟨S.sup k, S.lcm p, ?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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
⊢ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + p ∈ ⋃₀ (↑S : Set (Set ℕ))
have mp₁ : ∀ (x : ℕ) (hx : x ≥ S.sup k), x ∈ ⋃₀ (↑S : Set (Set ℕ)) ↔ x + S.lcm p ∈ ⋃₀ (↑S : Set (Set ℕ))
Tactic: refine ⟨S.sup k, S.lcm p, ?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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
have mp : ∀ (t : Set ℕ) (ht : t ∈ S), x ∈ t ↔ x + S.lcm p ∈ t
Tactic: refine exists_congr fun t => and_congr_right fun ht => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
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 + S.lcm p ∈ t
have hpt : p t ∣ S.lcm p
Tactic: have hpt : p t ∣ S.lcm p := Finset.dvd_lcm ht
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
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
⊢ x ∈ t ↔ x + S.lcm p ∈ t
have hpt₁ : ∃ (c : ℕ), S.lcm p = c * p t
Tactic: rw [dvd_iff_exists_eq_mul_left] at hpt
Cleared hypotheses: hpt
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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
⊢ x ∈ t ↔ x + S.lcm p ∈ t
have mp : ∀ (m : ℕ) (hpt : S.lcm p = m * p t), x ∈ t ↔ x + S.lcm p ∈ t
Tactic: rcases hpt with ⟨m, hpt⟩
Cleared hypotheses: hpt
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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
⊢ x ∈ t ↔ x + S.lcm p ∈ t
have mp : x ∈ t ↔ x + m * p t ∈ t
Tactic: rw [hpt]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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 : ℕ
⊢ x ∈ t ↔ x + m * p t ∈ t
have mp : x ∈ t ↔ x + 0 * p t ∈ t
Tactic: induction m with grind [Finset.sup_le_iff]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
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
⊢ x ∈ t ↔ x + m * p t ∈ t
have mp₁ : ∀ (n : ℕ), (x ∈ t ↔ x + n * p t ∈ t) → (x ∈ t ↔ x + (n + 1) * p t ∈ t)
Tactic: induction m with grind [Finset.sup_le_iff]
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
⊢ IsSemilinearSet s
have h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
Tactic: have h₁ : {x ∈ s | x < k}.Finite := (Set.finite_lt_nat k).subset (sep_subset_setOf _ _)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (hypothesis)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
⊢ IsSemilinearSet s
have h₂ : 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 _ _)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
⊢ IsSemilinearSet s
have h : s = {x : ℕ | x ∈ s ∧ x < k} ∪ ({x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p} + (↑(closure (↑{p} : Set ℕ)) : Set ℕ))
Tactic: convert! (IsSemilinearSet.of_finite h₁).union (.add (.of_finite h₂) (.closure_finset { p }))
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
⊢ s = {x : ℕ | x ∈ s ∧ x < k} ∪ ({x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p} + (↑(closure (↑{p} : Set ℕ)) : Set ℕ))
have h : ∀ (x : ℕ),
  x ∈ s ↔ x ∈ {x : ℕ | x ∈ s ∧ x < k} ∪ ({x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p} + (↑(closure (↑{p} : Set ℕ)) : Set ℕ))
Tactic: ext x
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
⊢ x ∈ s ↔ x ∈ {x : ℕ | x ∈ s ∧ x < k} ∪ ({x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p} + (↑(closure (↑{p} : Set ℕ)) : Set ℕ))
have h : x ∈ s ↔ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
Tactic: simp only [sep_and, Finset.coe_singleton, mem_union, mem_setOf_eq, mem_add, mem_inter_iff,
      SetLike.mem_coe, AddSubmonoid.mem_closure_singleton, smul_eq_mul, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
⊢ x ∈ s ↔ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
have h : x ∈ s → x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
h : x ∈ s → x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
⊢ x ∈ s ↔ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
have h₃ : (x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x) → x ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
have pos : ∀ (hx' : x < k), x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
Tactic: by_cases hx' : x < k
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs (goal)
Goal:
s : Set ℕ
k p : ℕ
hp : p > 0
hs : ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
h₁ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ x < k}
h₂ : Set.Finite (α := ℕ) {x : ℕ | x ∈ s ∧ k ≤ x ∧ x < k + p}
x : ℕ
hx : x ∈ s
pos :
  ∀ (hx' : x < k),
    x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
⊢ x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
have neg : ∀ (hx' : ¬x < k),
  x ∈ s ∧ x < k ∨ ∃ (x_1 : ℕ), ((x_1 ∈ s ∧ k ≤ x_1) ∧ x_1 ∈ s ∧ x_1 < k + p) ∧ ∃ (a : ℕ), x_1 + a * p = x
Tactic: by_cases hx' : x < k