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
⊢ ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}
have 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}
Tactic: rcases exists_maximalFor_of_wellFoundedGT (· ∈ s) g hs' with ⟨a, ha⟩
-- 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 ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}
have refine : IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ a ≤ y}
Tactic: refine ⟨a, ha.1, ?_⟩
-- 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
⊢ IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ a ≤ y}
have h : {y : M | y ∈ s ∧ a ≤ y} = a +ᵥ (↑(f a) : Set M)
Tactic: convert_to IsSemilinearSet (a +ᵥ (f a : Set M))
-- 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
h : {y : M | y ∈ s ∧ a ≤ y} = a +ᵥ (↑(f a) : Set M)
⊢ IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ a ≤ y}
have convert_to : IsSemilinearSet (a +ᵥ (↑(f a) : Set M))
Tactic: convert_to IsSemilinearSet (a +ᵥ (f a : Set M))
-- 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
⊢ {y : M | y ∈ s ∧ a ≤ y} = a +ᵥ (↑(f a) : Set M)
have h : ∀ (x : M), Membership.mem (γ := Set M) {y : M | y ∈ s ∧ a ≤ y} x ↔ x ∈ a +ᵥ (↑(f a) : Set M)
Tactic: ext x
-- 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
⊢ Membership.mem (γ := Set M) {y : M | y ∈ s ∧ a ≤ y} x ↔ x ∈ a +ᵥ (↑(f a) : Set M)
have h : (x ∈ s ∧ ∃ (c : M), x = a + c) ↔ ∃ (y : M), a + y ∈ s ∧ a + y = x
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]
-- 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
⊢ IsSemilinearSet (a +ᵥ (↑(f a) : Set M))
have refine : ∀ x ∈ f a, ∀ (y : M), x + y ∈ f a → y ∈ f a
Tactic: refine IsSemilinearSet.vadd a (.of_fg (AddSubmonoid.fg_of_subtractive ?_))
-- 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 : x ∈ f a
y : M
hxy : x + y ∈ f a
⊢ y ∈ f a
have rw : ∀ (hx : a + x ∈ s) (y : M) (hxy : x + y ∈ f a), y ∈ f a
Tactic: rw [hf _ ha.1] at hx
Cleared hypotheses: hx, y, hxy
-- 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
y : M
hxy : x + y ∈ f a
⊢ y ∈ f a
have hxy₁ : a + x + y ∈ s
Tactic: rw [hf _ ha.1, ← add_assoc] at hxy
Cleared hypotheses: hxy
-- 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
y : M
hxy : a + x + y ∈ s
⊢ y ∈ f a
have pos : ∀ (hy : y = 0), y ∈ f a
Tactic: by_cases hy : y = 0
-- 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
y : M
hxy : a + x + y ∈ s
pos : ∀ (hy : y = 0), y ∈ f a
⊢ y ∈ f a
have neg : ∀ (hy : ¬y = 0), y ∈ f a
Tactic: by_cases hy : y = 0
-- 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
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ y ∈ g (a + x)
have a₁ : y ∈ (↑(f (a + x)) : Set M) \ {0}
Tactic: apply AddSemigroupIdeal.subset_closure
-- 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
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ y ∈ (↑(f (a + x)) : Set M) \ {0}
have a₁ : y ∈ (↑(f (a + x)) : Set M)
Tactic: refine Set.mem_diff_of_mem ?_ hy
-- 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
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ y ∈ (↑(f (a + x)) : Set M)
have a₁ : y ∈ f (a + x)
Tactic: rwa [SetLike.mem_coe, hf _ hx]
-- 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
y : M
hxy : a + x + y ∈ s
hy : ¬y = 0
⊢ y ∈ f a
have hy₁ : 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]
Cleared hypotheses: hy
-- 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
y : M
hxy : a + x + y ∈ s
hy : y ∈ g (a + x)
⊢ y ∈ f a
have hy₁ : y ∈ g a
Tactic: apply ha.2 hx (hg _ ha.1 _ hx le_self_add) at hy
Cleared hypotheses: hy
-- 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
y : M
hxy : a + x + y ∈ s
hy : y ∈ g a
⊢ y ∈ f a
have hy₁ : ∃ (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
Cleared hypotheses: hy
-- 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
y : M
hxy : a + x + y ∈ s
hy : ∃ (y_1 : M) (z : M), (z ∈ f a ∧ z ≠ 0) ∧ y_1 + z = y
⊢ y ∈ f a
have neg : ∀ (w u : M) (hu₁ : u ∈ f a) (hu₂ : u ≠ 0) (hxy : a + x + (w + u) ∈ s), w + u ∈ f a
Tactic: rcases hy with ⟨w, u, ⟨hu₁, hu₂⟩, rfl⟩
Cleared hypotheses: y, hxy, hy
-- 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 u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
⊢ w + u ∈ f a
have 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
Tactic: induction w using WellQuasiOrderedLE.to_wellFoundedLT.induction (α := M) generalizing u with
      | _ w ih
Cleared hypotheses: w, u, hu₁, hu₂, hxy
-- 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
⊢ w + u ∈ f a
have pos : ∀ (hw₁ : w = 0), w + u ∈ f a
Tactic: by_cases hw₁ : w = 0
-- 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
pos : ∀ (hw₁ : w = 0), w + u ∈ f a
⊢ w + u ∈ f a
have neg : ∀ (hw₁ : ¬w = 0), w + u ∈ f a
Tactic: by_cases hw₁ : w = 0
-- 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
⊢ a + u ∈ s
have rwa : ∀ (hu₁ : a + u ∈ s) (hu₂ : u ≠ 0) (hxy : a + x + (w + u) ∈ s) (hw₁ : ¬w = 0), a + u ∈ s
Tactic: rwa [hf _ ha.1] at hu₁
Cleared hypotheses: hu₁, hu₂, hxy, 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
⊢ w + u ∈ f a
have hxu : a + x + u ∈ s
Tactic: have hxu : a + x + u ∈ s := hs _ ha.1 _ _ hx (by rwa [hf _ ha.1] at hu₁)
-- 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
⊢ w ∈ g (a + x + u)
have a₁ : w ∈ (↑(f (a + x + u)) : Set M) \ {0}
Tactic: apply AddSemigroupIdeal.subset_closure
-- 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
⊢ w ∈ (↑(f (a + x + u)) : Set M) \ {0}
have a₁ : w ∈ (↑(f (a + x + u)) : Set M)
Tactic: refine Set.mem_diff_of_mem ?_ 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
⊢ w ∈ (↑(f (a + x + u)) : Set M)
have a₁ : w ∈ f (a + x + u)
Tactic: rwa [SetLike.mem_coe, hf _ hxu, add_assoc, add_comm u w]