awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : (x + y) i = a
this :
  ∀ (hxz : x + z ∈ s) (hxzi : (x + z) i = a),
    Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + y + z)
⊢ Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + z) →
    Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + y + z)

Tactic:
⟨hxz, hxzi⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : (x + y) i = a
hxz : x + z ∈ s
hxzi : (x + z) i = a
⊢ Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + y + z)

Tactic:
⟨hs _ hx _ _ hxy hxz, ?_⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : (x + y) i = a
hxz : x + z ∈ s
hxzi : (x + z) i = a
refine : (x + y + z) i = a
⊢ Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + y + z)

Tactic:
refine ⟨hs _ hx _ _ hxy hxz, ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : (x + y) i = a
hxz : x + z ∈ s
hxzi : (x + z) i = a
simp : x i + y i + z i = a
⊢ (x + y + z) i = a

Tactic:
simp only [Pi.add_apply] at *

Premises used: Pi.add_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_1
M : ι → Type u_2
inst : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
hx : x ∈ s
hxi : x i = a
y z : (i : ι) → M i
hxy : x + y ∈ s
hxyi : x i + y i = a
hxz : x + z ∈ s
hxzi : x i + z i = a
rw : a + z i = a
rw₁ : x i + z i = x i
rw₂ : a = x i
rw₃ rw₄ : a = a
⊢ x i + y i + z i = a

Tactic:
rw [hxyi, ← hxi, hxzi, hxi]
-- 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
x : M
hx : x ∈ s
a b : M
ha : Membership.mem (γ := Set M) {y : M | x + y ∈ s} a
hb : Membership.mem (γ := Set M) {y : M | x + y ∈ s} b
simp : x + (a + b) ∈ s
⊢ Membership.mem (γ := Set M) {y : M | x + y ∈ s} (a + b)

Tactic:
simp only [mem_setOf_eq] at *

Premises used: Set.mem_setOf_eq
-- 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
x : M
hx : x ∈ s
a b : M
ha : x + a ∈ s
hb : x + b ∈ s
rw : x + a + b ∈ s
⊢ x + (a + b) ∈ s

Tactic:
rw [← add_assoc]

Premises used: add_assoc
-- 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
x : M
hx : x ∈ s
a b : M
ha : x + a ∈ s
hb : x + b ∈ s
⊢ x + a + b ∈ s

Tactic:
hs _ hx _ _ ha hb

Premises used: Set.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
x : M
hx : x ∈ s
a b : M
ha : x + a ∈ s
hb : x + b ∈ s
⊢ x + a + b ∈ s

Tactic:
exact hs _ hx _ _ ha hb
-- 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
x : M
hx : x ∈ s
⊢ Membership.mem (γ := Set M) {y : M | x + y ∈ s} 0

Tactic:
simpa
-- 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 ⊥
⊢ ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s

Tactic:
simp_all [f]
-- 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 ⊥
⊢ ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s

Tactic:
have hf : ∀ x ∈ s, ∀ y, y ∈ f x ↔ x + y ∈ s := by simp_all [f]
-- 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})
x : M
hx : x ∈ s
y : M
hy : y ∈ s
hxy : x ≤ y
z : M
hz : z ∈ g x
rw : ∀ (hxy : ∃ (c : M), y = x + c) ⦃z : M⦄ (hz : z ∈ g x), z ∈ g y
⊢ z ∈ g y

Tactic:
rw [le_iff_exists_add] at hxy

Premises used: le_iff_exists_add
-- 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})
x : M
hx : x ∈ s
y : M
hy : y ∈ s
hxy : ∃ (c : M), y = x + c
z : M
hz : z ∈ g x
rcases : ∀ (y : M) (hy : x + y ∈ s), z ∈ g (x + y)
⊢ z ∈ g y

Tactic:
rcases hxy with ⟨y, rfl⟩

Premises used: rfl
-- 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})
x : M
hx : x ∈ s
z : M
hz : z ∈ g x
y : M
hy : x + y ∈ s
simp :
  ∀ (hz : ∃ (y : M) (z_1 : M), (z_1 ∈ f x ∧ ¬z_1 = 0) ∧ y + z_1 = z),
    ∃ (y_1 : M) (z_1 : M), (z_1 ∈ f (x + y) ∧ ¬z_1 = 0) ∧ y_1 + z_1 = z
⊢ z ∈ g (x + y)

Tactic:
simp only [AddSemigroupIdeal.mem_closure'', mem_diff, SetLike.mem_coe, mem_singleton_iff,
      g] at hz ⊢

Premises used: AddSemigroupIdeal.mem_closure'', Set.mem_singleton_iff, SetLike.mem_coe, Set.mem_diff
-- 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})
x : M
hx : x ∈ s
z y : M
hy : x + y ∈ s
hz : ∃ (y : M) (z_1 : M), (z_1 ∈ f x ∧ ¬z_1 = 0) ∧ y + z_1 = z
rcases :
  ∀ (y' z : M) (hz₁ : z ∈ f x) (hz₂ : ¬z = 0), ∃ (y_1 : M) (z_1 : M), (z_1 ∈ f (x + y) ∧ ¬z_1 = 0) ∧ y_1 + z_1 = y' + z
⊢ ∃ (y_1 : M) (z_1 : M), (z_1 ∈ f (x + y) ∧ ¬z_1 = 0) ∧ y_1 + z_1 = z

Tactic:
rcases hz with ⟨y', z, ⟨hz₁, hz₂⟩, rfl⟩

Premises used: rfl
-- 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})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : z ∈ f x
hz₂ : ¬z = 0
⊢ x + z ∈ s

Tactic:
rw [hf _ hx] at hz₁
-- 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})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : z ∈ f x
hz₂ : ¬z = 0
hz₃ : x + z ∈ s
⊢ ¬z = 0

Tactic:
rw [hf _ hx] at hz₁
-- 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})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : x + z ∈ s
hz₂ : ¬z = 0
⊢ ∃ (y_1 : M) (z_1 : M), (z_1 ∈ f (x + y) ∧ ¬z_1 = 0) ∧ y_1 + z_1 = y' + z

Tactic:
⟨y', z, ⟨?_, hz₂⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- 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})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : x + z ∈ s
hz₂ : ¬z = 0
refine : z ∈ f (x + y)
⊢ ∃ (y_1 : M) (z_1 : M), (z_1 ∈ f (x + y) ∧ ¬z_1 = 0) ∧ y_1 + z_1 = y' + z

Tactic:
refine ⟨y', z, ⟨?_, hz₂⟩, rfl⟩
-- 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})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : x + z ∈ s
hz₂ : ¬z = 0
rw : x + y + z ∈ s
⊢ z ∈ f (x + y)

Tactic:
rw [hf _ hy]
-- 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})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : x + z ∈ s
hz₂ : ¬z = 0
⊢ x + y + z ∈ s

Tactic:
hs _ hx _ _ hy hz₁
-- 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})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : x + z ∈ s
hz₂ : ¬z = 0
⊢ x + y + z ∈ s

Tactic:
exact hs _ hx _ _ hy hz₁
-- 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})
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y

Tactic:
have hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y := by
    intro x hx y hy hxy z hz
    rw [le_iff_exists_add] at hxy
    rcases hxy with ⟨y, rfl⟩
    simp only [AddSemigroupIdeal.mem_closure'', mem_diff, SetLike.mem_coe, mem_singleton_iff,
      g] at hz ⊢
    rcases hz with ⟨y', z, ⟨hz₁, hz₂⟩, rfl⟩
    rw [hf _ hx] at hz₁
    refine ⟨y', z, ⟨?_, hz₂⟩, rfl⟩
    rw [hf _ hy]
    exact hs _ hx _ _ hy hz₁
-- 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
rcases :
  ∀ (a : M) (ha : MaximalFor (fun (x : M) ↦ x ∈ s) g a), ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}
⊢ ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}

Tactic:
rcases exists_maximalFor_of_wellFoundedGT (· ∈ s) g hs' with ⟨a, ha⟩

Premises used: Membership.mem, exists_maximalFor_of_wellFoundedGT
-- 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 ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}

Tactic:
⟨a, ha.1, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- 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
refine : IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ a ≤ y}
⊢ ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}

Tactic:
refine ⟨a, ha.1, ?_⟩
-- 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
h : {y : M | y ∈ s ∧ a ≤ y} = a +ᵥ (↑(f a) : Set M)
convert_to : IsSemilinearSet (a +ᵥ (↑(f a) : Set M))
⊢ IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ a ≤ y}

Tactic:
convert_to IsSemilinearSet (a +ᵥ (f a : Set M))

Premises used: HVAdd.hVAdd, SetLike.coe, IsSemilinearSet
-- 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
h : ∀ (x : M), Membership.mem (γ := Set M) {y : M | y ∈ s ∧ a ≤ y} x ↔ x ∈ a +ᵥ (↑(f a) : Set M)
⊢ {y : M | y ∈ s ∧ a ≤ y} = a +ᵥ (↑(f a) : Set M)

Tactic:
ext x
-- 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
h : (x ∈ s ∧ ∃ (c : M), x = a + c) ↔ ∃ (y : M), a + y ∈ s ∧ a + y = x
⊢ Membership.mem (γ := Set M) {y : M | y ∈ s ∧ a ≤ y} x ↔ x ∈ a +ᵥ (↑(f a) : Set M)

Tactic:
simp only [le_iff_exists_add, mem_setOf_eq, ha.1, ↓reduceDIte, coe_set_mk,
      AddSubsemigroup.coe_set_mk, mem_vadd_set, vadd_eq_add, f]

Premises used: Set.mem_vadd_set, le_iff_exists_add, reduceDIte, Set.mem_setOf_eq, And.left, vadd_eq_add, AddSubsemigroup.coe_set_mk, AddSubmonoid.coe_set_mk
-- 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
⊢ (x ∈ s ∧ ∃ (c : M), x = a + c) ↔ ∃ (y : M), a + y ∈ s ∧ a + y = x

Tactic:
grind
-- 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
⊢ IsSemilinearSet (a +ᵥ (↑(f a) : Set M))

Tactic:
IsSemilinearSet.vadd a (.of_fg (AddSubmonoid.fg_of_subtractive ?_))

Premises used: IsSemilinearSet.vadd, AddSubmonoid.fg_of_subtractive, IsSemilinearSet.of_fg
-- 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
refine : ∀ x ∈ f a, ∀ (y : M), x + y ∈ f a → y ∈ f a
⊢ IsSemilinearSet (a +ᵥ (↑(f a) : Set M))

Tactic:
refine IsSemilinearSet.vadd a (.of_fg (AddSubmonoid.fg_of_subtractive ?_))

Premises used: IsSemilinearSet.vadd, AddSubmonoid.fg_of_subtractive, IsSemilinearSet.of_fg
-- 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 : x ∈ f a
y : M
hxy : x + y ∈ f a
rw : ∀ (hx : a + x ∈ s) (y : M) (hxy : x + y ∈ f a), y ∈ f a
⊢ y ∈ f a

Tactic:
rw [hf _ ha.1] at hx

Premises used: And.left