awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
hxu : a + x + u ∈ s
a₁ : w ∈ f (a + x + u)
⊢ w ∈ (↑(f (a + x + u)) : Set M)
have a₂ : a + x + u + w ∈ s
Tactic: rwa [SetLike.mem_coe, hf _ hxu, add_assoc, add_comm u w]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
hxu : a + x + u ∈ s
a₁ : w ∈ f (a + x + u)
a₂ : a + x + u + w ∈ s
⊢ w ∈ (↑(f (a + x + u)) : Set M)
have a₃ : a + x + (u + w) ∈ s
Tactic: rwa [SetLike.mem_coe, hf _ hxu, add_assoc, add_comm u w]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
hxu : a + x + u ∈ s
⊢ w + u ∈ f a
have hw₂ : w ∈ g (a + x + u)
Tactic: have hw₂ : w ∈ g (a + x + u) := by
      apply AddSemigroupIdeal.subset_closure
      refine Set.mem_diff_of_mem ?_ hw₁
      rwa [SetLike.mem_coe, hf _ hxu, add_assoc, add_comm u w]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
hxu : a + x + u ∈ s
hw₂ : w ∈ g (a + x + u)
⊢ w + u ∈ f a
have hw₃ : w ∈ g a
Tactic: apply ha.2 hxu (hg _ ha.1 _ hxu (le_add_right le_self_add)) at hw₂
Cleared hypotheses: hw₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
hxu : a + x + u ∈ s
hw₂ : w ∈ g a
⊢ w + u ∈ f a
have hw₃ : ∃ (y : M) (z : M), (z ∈ f a ∧ z ≠ 0) ∧ y + z = w
Tactic: simp only [g, AddSemigroupIdeal.mem_closure'', Set.mem_diff, SetLike.mem_coe,
      Set.notMem_singleton_iff] at hw₂
Cleared hypotheses: hw₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : ¬w = 0
hxu : a + x + u ∈ s
hw₂ : ∃ (y : M) (z : M), (z ∈ f a ∧ z ≠ 0) ∧ y + z = w
⊢ w + u ∈ f a
have neg : ∀ (w' u' : M) (hu'₁ : u' ∈ f a) (hu'₂ : u' ≠ 0)
  (ih : ∀ y < w' + u', ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a)
  (hxy : a + x + (w' + u' + u) ∈ s) (hw₁ : ¬w' + u' = 0), w' + u' + u ∈ f a
Tactic: rcases hw₂ with ⟨w', u', ⟨hu'₁, hu'₂⟩, rfl⟩
Cleared hypotheses: w, ih, hxy, hw₁, hw₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
⊢ w' + u' + u ∈ f a
have neg : w' + (u' + u) ∈ f a
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
⊢ w' + (u' + u) ∈ f a
have neg : w' < w' + u'
Tactic: apply ih
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
neg : w' < w' + u'
⊢ w' + (u' + u) ∈ f a
have neg₁ : u' + u ∈ f a
Tactic: apply ih
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
neg : w' < w' + u'
neg₁ : u' + u ∈ f a
⊢ w' + (u' + u) ∈ f a
have neg₂ : u' + u ≠ 0
Tactic: apply ih
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : WellQuasiOrderedLE M
inst_3 : IsOrderedCancelAddMonoid M
inst_4 : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : (x : M) → AddSubmonoid M :=
  fun (x : M) ↦ if hx : x ∈ s then { carrier := {y : M | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : (x : M) → AddSemigroupIdeal M := fun (x : M) ↦ AddSemigroupIdeal.closure ((↑(f x) : Set M) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxu : a + x + u ∈ s
w' u' : M
hu'₁ : u' ∈ f a
hu'₂ : u' ≠ 0
ih : ∀ y < w' + u', ∀ (u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (y + u) ∈ s), y + u ∈ f a
hxy : a + x + (w' + u' + u) ∈ s
hw₁ : ¬w' + u' = 0
neg : w' < w' + u'
neg₁ : u' + u ∈ f a
neg₂ : u' + u ≠ 0
⊢ w' + (u' + u) ∈ f a
have neg₃ : a + x + (w' + (u' + u)) ∈ s
Tactic: apply ih
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s
⊢ IsSemilinearSet s
have haveI : ∀ (this : Fintype ι), IsSemilinearSet s
Tactic: haveI := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
⊢ IsSemilinearSet s
have suffices : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s
Tactic: suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    haveI := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
t : Finset ι
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
⊢ IsSemilinearSet s
have a₁ : ∀ (t : Finset ι)
  (ih :
    ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
  {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
Tactic: induction t using Finset.strongInductionOn generalizing s a with | _ t ih
Cleared hypotheses: s, hs, a, t, ht
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
⊢ IsSemilinearSet s
have a₁ : ∀ (hs : IsSlice.{u_1} (M := ι → ℕ) ∅) (ht : ∀ (x : ι → ℕ), Membership.mem (γ := Set (ι → ℕ)) ∅ x → ∀ i ∉ t, x i = a i),
  IsSemilinearSet.{u_1} (M := ι → ℕ) ∅
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs, ht
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
a₁ :
  ∀ (hs : IsSlice.{u_1} (M := ι → ℕ) ∅)
    (ht : ∀ (x : ι → ℕ), Membership.mem (γ := Set (ι → ℕ)) ∅ x → ∀ i ∉ t, x i = a i),
    IsSemilinearSet.{u_1} (M := ι → ℕ) ∅
⊢ IsSemilinearSet s
have a₂ : ∀ (hs' : s.Nonempty), IsSemilinearSet s
Tactic: obtain rfl | hs' := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
⊢ IsSemilinearSet s
have a₁ : ∀ (x : ι → ℕ) (hx : x ∈ s) (hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}), IsSemilinearSet s
Tactic: rcases hs.exists_isSemilinearSet_setOf_le hs' with ⟨x, hx, hx'⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}
⊢ IsSemilinearSet s
have h : s = {y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j}
Tactic: convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}
h : s = {y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j}
⊢ IsSemilinearSet s
have a₁ : IsSemilinearSet.{u_1} (M := ι → ℕ)
  ({y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j})
Tactic: convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}
⊢ s = {y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j}
have h : ∀ (y : ι → ℕ),
  y ∈ s ↔
    Membership.mem (γ := Set (ι → ℕ))
      ({y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j}) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}
y : ι → ℕ
⊢ y ∈ s ↔
    Membership.mem (γ := Set (ι → ℕ))
      ({y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j}) y
have h : y ∈ s ↔ (y ∈ s ∧ ∀ (i : ι), x i ≤ y i) ∨ ∃ (i : ι) (_ : i ∈ t) (i_1 : ℕ) (_ : i_1 < x i), y ∈ s ∧ y i = i_1
Tactic: simp only [Finset.mem_range, mem_union, mem_setOf_eq, mem_iUnion, Pi.le_def]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}
⊢ IsSemilinearSet.{u_1} (M := ι → ℕ)
    ({y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j})
have a₁ : ∀ (i : ι) (hi : i ∈ t) (j : ℕ) (hj : j ∈ Finset.range (x i)),
  IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ y i = j}
Tactic: refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}
i : ι
hi : i ∈ t
j : ℕ
hj : j ∈ Finset.range (x i)
⊢ IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ y i = j}
have hj₁ : j < x i
Tactic: simp only [Finset.mem_range] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}
i : ι
hi : i ∈ t
j : ℕ
hj : j < x i
⊢ IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ y i = j}
have a₁ : ∀ (x : ι → ℕ),
  Membership.mem (γ := Set (ι → ℕ)) {x : (i : ι) → ℕ | x ∈ s ∧ x i = j} x →
    ∀ i_1 ∉ t.erase i, x i_1 = Function.update (β := fun (a : ι) ↦ ℕ) a i j i_1
Tactic: apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
⊢ IsSemilinearSet s
have suffices : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s
Tactic: classical
  suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    haveI := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
  intro a t ht
  induction t using Finset.strongInductionOn generalizing s a with | _ t ih
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · exact .empty
  rcases hs.exists_isSemilinearSet_setOf_le hs' with ⟨x, hx, hx'⟩
  convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
  · ext y
    simp only [Finset.mem_range, mem_union, mem_setOf_eq, mem_iUnion, Pi.le_def]
    grind
  · refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (a : ι → ℕ) (t : Finset ι) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
⊢ IsSemilinearSet s
have a : ∀ (t : Finset ι)
  (ih :
    ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t_1, x i = a i), IsSemilinearSet s)
  {s : Set (ι → ℕ)} (hs : IsSlice s) (a : ι → ℕ) (ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i), IsSemilinearSet s
Tactic: classical
  suffices h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s by
    haveI := Fintype.ofFinite ι
    exact h 0 Finset.univ (by simp)
  intro a t ht
  induction t using Finset.strongInductionOn generalizing s a with | _ t ih
  obtain rfl | hs' := s.eq_empty_or_nonempty
  · exact .empty
  rcases hs.exists_isSemilinearSet_setOf_le hs' with ⟨x, hx, hx'⟩
  convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })
  · ext y
    simp only [Finset.mem_range, mem_union, mem_setOf_eq, mem_iUnion, Pi.le_def]
    grind
  · refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)
    simp only [Finset.mem_range] at hj
    apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)
    grind [Function.update]
Cleared hypotheses: s, hs