awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
neg₃ : a + x + (w' + (u' + u)) ∈ s
⊢ w' + (u' + u) ∈ f a

Tactic:
apply ih
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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' < w' + u'

Tactic:
lt_add_of_pos_right _ (pos_of_ne_zero hu'₂)

Premises used: lt_add_of_pos_right, pos_of_ne_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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' < w' + u'

Tactic:
exact lt_add_of_pos_right _ (pos_of_ne_zero hu'₂)

Premises used: lt_add_of_pos_right, pos_of_ne_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
⊢ u' + u ∈ f a

Tactic:
add_mem hu'₁ hu₁

Premises used: AddMemClass.add_mem
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
⊢ u' + u ∈ f a

Tactic:
exact add_mem hu'₁ hu₁

Premises used: AddMemClass.add_mem
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
⊢ u' + u ≠ 0

Tactic:
simp [hu₂, hu'₂]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 neg₁ neg₂ neg₃ : a + x + (w' + u' + u) ∈ s
⊢ a + x + (w' + (u' + u)) ∈ s

Tactic:
rwa [← add_assoc w']

Premises used: add_assoc
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
haveI : ∀ (this : Fintype ι), IsSemilinearSet s
⊢ IsSemilinearSet s

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
this : Fintype ι
⊢ ∀ x ∈ s, ∀ i ∉ Finset.univ, x i = 0 i

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
this : Fintype ι
⊢ IsSemilinearSet s

Tactic:
exact h 0 Finset.univ (by simp)

Premises used: Finset.univ, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
suffices : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s
⊢ 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)
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_1
inst : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
t : Finset ι
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
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
⊢ IsSemilinearSet s

Tactic:
induction t using Finset.strongInductionOn generalizing s a with | _ t ih
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 := ι → ℕ) ∅
a₂ : ∀ (hs' : s.Nonempty), IsSemilinearSet s
⊢ IsSemilinearSet s

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
a : ι → ℕ
hs : IsSlice.{u_1} (M := ι → ℕ) ∅
ht : ∀ (x : ι → ℕ), Membership.mem (γ := Set (ι → ℕ)) ∅ x → ∀ i ∉ t, x i = a i
⊢ IsSemilinearSet.{u_1} (M := ι → ℕ) ∅

Tactic:
.empty

Premises used: IsSemilinearSet.empty
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
a : ι → ℕ
hs : IsSlice.{u_1} (M := ι → ℕ) ∅
ht : ∀ (x : ι → ℕ), Membership.mem (γ := Set (ι → ℕ)) ∅ x → ∀ i ∉ t, x i = a i
⊢ IsSemilinearSet.{u_1} (M := ι → ℕ) ∅

Tactic:
exact .empty
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
a₁ :
  ∀ (x : ι → ℕ) (hx : x ∈ s) (hx' : IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ x ≤ y}), IsSemilinearSet s
⊢ IsSemilinearSet s

Tactic:
rcases hs.exists_isSemilinearSet_setOf_le hs' with ⟨x, hx, hx'⟩

Premises used: _private.0.IsSlice.exists_isSemilinearSet_setOf_le
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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}
a₁ :
  IsSemilinearSet.{u_1} (M := ι → ℕ)
    ({y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j})
⊢ IsSemilinearSet s

Tactic:
convert_to IsSemilinearSet ({ y ∈ s | x ≤ y } ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i),
    { y ∈ s | y i = j })

Premises used: setOf, Membership.mem, LE.le, And, IsSemilinearSet, Union.union, Eq, Set.iUnion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 :
  ∀ (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
⊢ s = {y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j}

Tactic:
ext y
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 : ι → ℕ
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
⊢ 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:
simp only [Finset.mem_range, mem_union, mem_setOf_eq, mem_iUnion, Pi.le_def]

Premises used: Set.mem_union, Set.mem_iUnion, Set.mem_setOf_eq, Finset.mem_range, Pi.le_def
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 ↔ (y ∈ s ∧ ∀ (i : ι), x i ≤ y i) ∨ ∃ (i : ι) (_ : i ∈ t) (i_1 : ℕ) (_ : i_1 < x i), y ∈ s ∧ y i = i_1

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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})

Tactic:
hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)

Premises used: IsSemilinearSet.biUnion_finset, setOf, IsSemilinearSet.union
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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}
a₁ :
  ∀ (i : ι) (hi : i ∈ t) (j : ℕ) (hj : j ∈ Finset.range (x i)),
    IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ y i = j}
⊢ IsSemilinearSet.{u_1} (M := ι → ℕ)
    ({y : ι → ℕ | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y : ι → ℕ | y ∈ s ∧ y i = j})

Tactic:
refine hx'.union (.biUnion_finset fun i hi => .biUnion_finset fun j hj => ?_)

Premises used: IsSemilinearSet.biUnion_finset, IsSemilinearSet.union
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)
⊢ j < x i

Tactic:
simp only [Finset.mem_range] at hj

Premises used: Finset.mem_range
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
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
⊢ IsSemilinearSet.{u_1} (M := ι → ℕ) {y : ι → ℕ | y ∈ s ∧ y i = j}

Tactic:
apply ih _ (Finset.erase_ssubset hi) (hs.sep_apply_eq _ _) (Function.update a i j)

Premises used: Function.update, _private.0.IsSlice.sep_apply_eq, Finset.erase_ssubset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
⊢ ∀ (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:
grind [Function.update]

Premises used: Function.update
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
G : Type u_6
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
inst_4 : FunLike.{u_6 + 1, u_3 + 1, u_1 + 1} G (ι → ℕ) M
inst_5 : AddMonoidHomClass.{u_6, u_3, u_1} G (ι → ℕ) M
a b : M
f : F
g : G
hs :
  IsSlice.{u_3} (M := ι → ℕ)
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}

Tactic:
apply isSemilinearSet_of_isSlice

Premises used: _private.0.Nat.isSemilinearSet_of_isSlice
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
G : Type u_6
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
inst_4 : FunLike.{u_6 + 1, u_3 + 1, u_1 + 1} G (ι → ℕ) M
inst_5 : AddMonoidHomClass.{u_6, u_3, u_1} G (ι → ℕ) M
a b : M
f : F
g : G
x : ι → ℕ
hx :
  Membership.mem (γ := Set (ι → ℕ))
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
    x
y z : ι → ℕ
hy :
  Membership.mem (γ := Set (ι → ℕ))
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
    (x + y)
hz :
  Membership.mem (γ := Set (ι → ℕ))
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
    (x + z)
hs :
  ∀ (hx : HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M))
    (hy :
      HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M) =
        HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
    (hz :
      HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) z : M) =
        HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) z : M)),
    HAdd.hAdd (β := M)
        (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
        ((f : (a : ι → ℕ) → M) z : M) =
      HAdd.hAdd (β := M)
        (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
        ((g : (a : ι → ℕ) → M) z : M)
⊢ Membership.mem (γ := Set (ι → ℕ))
    {x : ι → ℕ |
      HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)}
    (x + y + z)

Tactic:
simp only [mem_setOf, map_add, ← add_assoc] at *

Premises used: add_assoc, map_add, Set.mem_setOf
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
G : Type u_6
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
inst_4 : FunLike.{u_6 + 1, u_3 + 1, u_1 + 1} G (ι → ℕ) M
inst_5 : AddMonoidHomClass.{u_6, u_3, u_1} G (ι → ℕ) M
a b : M
f : F
g : G
x y z : ι → ℕ
hx : HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)
hy :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M)
hz :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) z : M)
rw :
  HAdd.hAdd (β := M)
    (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
    ((g : (a : ι → ℕ) → M) z : M)
| HAdd.hAdd (β := M)
    (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
    ((f : (a : ι → ℕ) → M) z : M)

Tactic:
rw [hy, ← hx, add_right_comm _ (g y) (f z), hz, add_right_comm _ (g z)]

Premises used: add_right_comm, DFunLike.coe