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
y : M
hxy : x + y ∈ f a
⊢ a + x + y ∈ s

Tactic:
rw [hf _ ha.1, ← add_assoc] at hxy

Premises used: add_assoc, And.left
-- 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
y : M
hxy : a + x + y ∈ s
pos : ∀ (hy : y = 0), y ∈ f a
neg : ∀ (hy : ¬y = 0), y ∈ f a
⊢ y ∈ f a

Tactic:
by_cases hy : y = 0
-- 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
y : M
hxy : a + x + y ∈ s
hy : y = 0
⊢ y ∈ f a

Tactic:
simp [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})
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
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
a₁ : y ∈ (↑(f (a + x)) : Set M) \ {0}
⊢ y ∈ g (a + x)

Tactic:
apply AddSemigroupIdeal.subset_closure

Premises used: AddSemigroupIdeal.subset_closure
-- 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
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ y ∈ (↑(f (a + x)) : Set M) \ {0}

Tactic:
Set.mem_diff_of_mem ?_ hy

Premises used: Set.mem_diff_of_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
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
a₁ : y ∈ (↑(f (a + x)) : Set M)
⊢ y ∈ (↑(f (a + x)) : Set M) \ {0}

Tactic:
refine Set.mem_diff_of_mem ?_ hy

Premises used: Set.mem_diff_of_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
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
a₁ : y ∈ f (a + x)
a₂ a₃ a₄ a₅ : a + x + y ∈ s
⊢ y ∈ (↑(f (a + x)) : Set M)

Tactic:
rwa [SetLike.mem_coe, hf _ hx]

Premises used: SetLike.mem_coe
-- 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
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ y ∈ g (a + x)

Tactic:
replace hy : y ∈ g (a + x) := by
      apply AddSemigroupIdeal.subset_closure
      refine Set.mem_diff_of_mem ?_ hy
      rwa [SetLike.mem_coe, hf _ hx]
-- 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
y : M
hxy : a + x + y ∈ s
hy : y ∈ g (a + x)
⊢ y ∈ g a

Tactic:
apply ha.2 hx (hg _ ha.1 _ hx le_self_add) at hy

Premises used: And.right, And.left, le_self_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})
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
y : M
hxy : a + x + y ∈ s
hy : y ∈ g a
⊢ ∃ (y_1 : M) (z : M), (z ∈ f a ∧ z ≠ 0) ∧ y_1 + z = y

Tactic:
simp only [g, AddSemigroupIdeal.mem_closure'', Set.mem_diff, SetLike.mem_coe,
      Set.notMem_singleton_iff] at hy

Premises used: AddSemigroupIdeal.mem_closure'', Set.notMem_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})
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
y : M
hxy : a + x + y ∈ s
hy : ∃ (y_1 : M) (z : M), (z ∈ f a ∧ z ≠ 0) ∧ y_1 + z = y
neg : ∀ (w u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (w + u) ∈ s), w + u ∈ f a
⊢ y ∈ f a

Tactic:
rcases hy with ⟨w, u, ⟨hu₁, hu₂⟩, 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})
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 u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
neg :
  ∀ (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), w + u ∈ f a
⊢ w + u ∈ f a

Tactic:
induction w using WellQuasiOrderedLE.to_wellFoundedLT.induction (α := M) generalizing u with
      | _ w ih

Premises used: WellFoundedLT.induction
-- 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
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
pos : ∀ (hw₁ : w = 0), w + u ∈ f a
neg : ∀ (hw₁ : ¬w = 0), w + u ∈ f a
⊢ w + u ∈ f a

Tactic:
by_cases hw₁ : w = 0
-- 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
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
⊢ w + u ∈ f a

Tactic:
simpa [hw₁]
-- 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
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (hu₁ : a + u ∈ s) (hu₂ : u ≠ 0) (hxy : a + x + (w + u) ∈ s) (hw₁ : ¬w = 0), a + u ∈ s
⊢ a + u ∈ s

Tactic:
rwa [hf _ ha.1] at hu₁

Premises used: And.left
-- 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
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
⊢ a + x + u ∈ s

Tactic:
have hxu : a + x + u ∈ s := hs _ ha.1 _ _ hx (by rwa [hf _ ha.1] at 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
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)) : Set M) \ {0}
⊢ w ∈ g (a + x + u)

Tactic:
apply AddSemigroupIdeal.subset_closure

Premises used: AddSemigroupIdeal.subset_closure
-- 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
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 ∈ (↑(f (a + x + u)) : Set M) \ {0}

Tactic:
Set.mem_diff_of_mem ?_ hw₁

Premises used: Set.mem_diff_of_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
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)) : Set M)
⊢ w ∈ (↑(f (a + x + u)) : Set M) \ {0}

Tactic:
refine Set.mem_diff_of_mem ?_ hw₁

Premises used: Set.mem_diff_of_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
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
a₃ : a + x + (u + w) ∈ s
a₄ a₅ a₆ a₇ : a + x + (w + u) ∈ s
⊢ w ∈ (↑(f (a + x + u)) : Set M)

Tactic:
rwa [SetLike.mem_coe, hf _ hxu, add_assoc, add_comm u w]

Premises used: add_assoc, add_comm, SetLike.mem_coe
-- 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
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 ∈ 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]
-- 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
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 ∈ g a

Tactic:
apply ha.2 hxu (hg _ ha.1 _ hxu (le_add_right le_self_add)) at hw₂

Premises used: And.right, And.left, le_self_add, le_add_right
-- 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
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
⊢ ∃ (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₂

Premises used: AddSemigroupIdeal.mem_closure'', Set.notMem_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})
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
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
⊢ w + u ∈ f a

Tactic:
rcases hw₂ with ⟨w', u', ⟨hu'₁, hu'₂⟩, 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})
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' + (u' + u) ∈ f a
⊢ w' + u' + u ∈ f a

Tactic:
rw [add_assoc]

Premises used: add_assoc