awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
x : α → ℕ
⊢ φ.Realize x ↔
    ∃ (x_1 : α ⊕ Fin 0 → ℕ),
      BoundedFormula.Realize φ (x_1 ∘ Sum.inl) (x_1 ∘ Sum.inr) ∧
        (LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ) x_1 = x
have h : φ.Realize x ↔
  ∃ (b : α → ℕ),
    BoundedFormula.Realize (M := ℕ) φ
        (Function.comp (β := α ⊕ Fin 0) (((e.arrowCongr (_root_.Equiv.refl ℕ)).symm : (a : α → ℕ) → α ⊕ Fin 0 → ℕ) b)
          Sum.inl)
        (Function.comp.{1, u_1 + 1, 1} (β := α ⊕ Fin 0)
          (((e.arrowCongr (_root_.Equiv.refl ℕ)).symm : (a : α → ℕ) → α ⊕ Fin 0 → ℕ) b) Sum.inr) ∧
      (LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
          (((e.arrowCongr (_root_.Equiv.refl ℕ)).symm : (a : α → ℕ) → α ⊕ Fin 0 → ℕ) b : α ⊕ Fin 0 → ℕ) =
        x
Tactic: rw [(e.arrowCongr (.refl ℕ)).exists_congr_left]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A s : Set ℕ
⊢ A.Definable₁ presburger s ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
have rw : IsSemilinearSet (M := ℕ)
    (image (α := Fin 1 → ℕ) (⇑(LinearEquiv.funUnique (Fin 1) ℕ ℕ) : (a : Fin 1 → ℕ) → ℕ)
      (preimage (β := ℕ) (fun (x : Fin 1 → ℕ) ↦ x 0) {a : ℕ | a ∈ s})) ↔
  ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Tactic: rw [Definable₁, definable_iff_isSemilinearSet,
    ← isSemilinearSet_image_iff (LinearEquiv.funUnique (Fin 1) ℕ ℕ), ← preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A s : Set ℕ
⊢ IsSemilinearSet (M := ℕ)
      (image (α := Fin 1 → ℕ) (⇑(LinearEquiv.funUnique (Fin 1) ℕ ℕ) : (a : Fin 1 → ℕ) → ℕ)
        (preimage (β := ℕ) (fun (x : Fin 1 → ℕ) ↦ x 0) {a : ℕ | a ∈ s})) ↔
    ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
have simp : IsSemilinearSet (M := ℕ) ((fun (a : Fin 1 → ℕ) ↦ a 0) '' (fun (x : Fin 1 → ℕ) ↦ x 0) ⁻¹' s) ↔
  ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Tactic: simp only [LinearEquiv.funUnique_apply, Function.eval, Fin.default_eq_zero, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A s : Set ℕ
⊢ IsSemilinearSet (M := ℕ) ((fun (a : Fin 1 → ℕ) ↦ a 0) '' (fun (x : Fin 1 → ℕ) ↦ x 0) ⁻¹' s) ↔
    ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
have rw : IsSemilinearSet s ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Tactic: rw [image_preimage_eq s fun x => ⟨![x], rfl⟩, Nat.isSemilinearSet_iff_ultimately_periodic]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A s : Set ℕ
rw : IsSemilinearSet s ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
⊢ IsSemilinearSet (M := ℕ) ((fun (a : Fin 1 → ℕ) ↦ a 0) '' (fun (x : Fin 1 → ℕ) ↦ x 0) ⁻¹' s) ↔
    ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
have rw₁ : (∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s) ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Tactic: rw [image_preimage_eq s fun x => ⟨![x], rfl⟩, Nat.isSemilinearSet_iff_ultimately_periodic]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
⊢ A.Definable presburger (α := Fin 1)
    {x : Fin 1 → ℕ | Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (x 0)}
have h : Eq (α := Set (Fin 1 → ℕ)) {x : Fin 1 → ℕ | Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (x 0)}
  ((fun (g : Fin 2 → ℕ) ↦ g ∘ ![0]) ''
    preimage (β := Fin (Nat.succ 0).succ.succ → ℕ) (fun (g : Fin 2 → ℕ) ↦ g ∘ ![0, 1, 1])
      {v : Fin 3 → ℕ | v 0 = v 1 * v 2})
Tactic: convert! (hmul.preimage_comp (β := Fin 2) ![0, 1, 1]).image_comp ![0]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
⊢ Eq (α := Set (Fin 1 → ℕ)) {x : Fin 1 → ℕ | Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (x 0)}
    ((fun (g : Fin 2 → ℕ) ↦ g ∘ ![0]) ''
      preimage (β := Fin (Nat.succ 0).succ.succ → ℕ) (fun (g : Fin 2 → ℕ) ↦ g ∘ ![0, 1, 1])
        {v : Fin 3 → ℕ | v 0 = v 1 * v 2})
have h : ∀ (x : Fin 1 → ℕ),
  Membership.mem (γ := Set (Fin 1 → ℕ))
      {x : Fin 1 → ℕ | Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (x 0)} x ↔
    Membership.mem (γ := Set (Fin 1 → ℕ))
      ((fun (g : Fin 2 → ℕ) ↦ g ∘ ![0]) ''
        preimage (β := Fin (Nat.succ 0).succ.succ → ℕ) (fun (g : Fin 2 → ℕ) ↦ g ∘ ![0, 1, 1])
          {v : Fin 3 → ℕ | v 0 = v 1 * v 2})
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
⊢ False
have hsqr : A.Definable₁ presburger {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x}
Tactic: have hsqr : A.Definable₁ presburger {x * x | x : ℕ} := by
    rw [Definable₁]
    convert! (hmul.preimage_comp (β := Fin 2) ![0, 1, 1]).image_comp ![0]
    ext
    simpa [funext_iff, Fin.exists_fin_succ_pi] using exists_congr fun _ => Eq.comm
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
hsqr : A.Definable₁ presburger {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x}
⊢ False
have hsqr₁ : ∃ (k : ℕ),
  ∃ p > 0,
    ∀ x ≥ k,
      Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} x ↔
        Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (x + p)
Tactic: rw [definable₁_iff_ultimately_periodic] at hsqr
Cleared hypotheses: hsqr
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
hsqr :
  ∃ (k : ℕ),
    ∃ p > 0,
      ∀ x ≥ k,
        Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} x ↔
          Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (x + p)
⊢ False
have rcases : ∀ (k p : ℕ) (hp : p > 0)
  (h :
    ∀ x ≥ k,
      Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} x ↔
        Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (x + p)),
  False
Tactic: rcases hsqr with ⟨k, p, hp, h⟩
Cleared hypotheses: hsqr
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
h :
  ∀ x ≥ k,
    Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} x ↔
      Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (x + p)
⊢ False
have h₁ : Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (max k p * max k p) ↔
  Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (max k p * max k p + p)
Tactic: specialize h ((max k p) * (max k p)) ((Nat.le_mul_self _).trans' (le_max_left _ _))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
h :
  Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (max k p * max k p) ↔
    Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (max k p * max k p + p)
⊢ False
have h₁ : ∃ (x : ℕ), x * x = max k p * max k p + p
Tactic: simp only [mem_setOf_eq, exists_apply_eq_apply, true_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
h : ∃ (x : ℕ), x * x = max k p * max k p + p
⊢ False
have rcases : ∀ (x : ℕ) (h₁ : x * x = max k p * max k p + p), False
Tactic: rcases h with ⟨x, h₁⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
⊢ False
have pos : ∀ (h₂ : x ≤ max k p), False
Tactic: by_cases h₂ : x ≤ max k p
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (goal)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
pos : ∀ (h₂ : x ≤ max k p), False
⊢ False
have neg : ∀ (h₂ : ¬x ≤ max k p), False
Tactic: by_cases h₂ : x ≤ max k p
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : x ≤ max k p
⊢ False
have h₃ : x * x ≤ max k p * max k p
Tactic: apply Nat.mul_self_le_mul_self at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : ¬x ≤ max k p
⊢ False
have h₃ : max k p + 1 ≤ x
Tactic: simp only [not_le, Nat.lt_iff_add_one_le] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Definability (hypothesis)
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : max k p + 1 ≤ x
⊢ False
have h₃ : (max k p + 1) * (max k p + 1) ≤ x * x
Tactic: apply Nat.mul_self_le_mul_self at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} x →
    ∀ (b c : (i : ι) → M i),
      Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + b) →
        Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + c) →
          Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + b + c)
have this : ∀ (hx : x ∈ s) (hxi : x i = a) (b c : (i : ι) → M i),
  Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + b) →
    Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + c) →
      Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + b + c)
Tactic: ⟨hx, hxi⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ Membership.mem (γ := Set ((i : ι) → M i)) {x : (i : ι) → M i | x ∈ s ∧ x i = a} (x + y) →
    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)
have this : ∀ (hxy : x + y ∈ s) (hxyi : (x + y) i = a),
  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: ⟨hxy, hxyi⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ 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)
have 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)
Tactic: ⟨hxz, hxzi⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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)
have refine : (x + y + z) i = a
Tactic: refine ⟨hs _ hx _ _ hxy hxz, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ (x + y + z) i = a
have simp : x i + y i + z i = a
Tactic: simp only [Pi.add_apply] at *
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ x i + y i + z i = a
have rw : a + z i = a
Tactic: rw [hxyi, ← hxi, hxzi, hxi]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ x i + y i + z i = a
have rw₁ : x i + z i = x i
Tactic: rw [hxyi, ← hxi, hxzi, hxi]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ x i + y i + z i = a
have rw₂ : a = x i
Tactic: rw [hxyi, ← hxi, hxzi, hxi]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ x i + y i + z i = a
have rw₃ : a = a
Tactic: rw [hxyi, ← hxi, hxzi, hxi]
-- 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
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
⊢ Membership.mem (γ := Set M) {y : M | x + y ∈ s} (a + b)
have simp : x + (a + b) ∈ s
Tactic: simp only [mem_setOf_eq] at *
-- 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
x : M
hx : x ∈ s
a b : M
ha : x + a ∈ s
hb : x + b ∈ s
⊢ x + (a + b) ∈ s
have rw : x + a + b ∈ s
Tactic: rw [← add_assoc]
-- 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 ⊥
⊢ ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}
have hf : ∀ 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]
-- 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})
x : M
hx : x ∈ s
y : M
hy : y ∈ s
hxy : x ≤ y
z : M
hz : z ∈ g x
⊢ z ∈ g y
have rw : ∀ (hxy : ∃ (c : M), y = x + c) ⦃z : M⦄ (hz : z ∈ g x), z ∈ g y
Tactic: rw [le_iff_exists_add] at hxy
Cleared hypotheses: hxy, z, hz
-- 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})
x : M
hx : x ∈ s
y : M
hy : y ∈ s
hxy : ∃ (c : M), y = x + c
z : M
hz : z ∈ g x
⊢ z ∈ g y
have rcases : ∀ (y : M) (hy : x + y ∈ s), z ∈ g (x + y)
Tactic: rcases hxy with ⟨y, rfl⟩
Cleared hypotheses: y, hy, 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})
x : M
hx : x ∈ s
z : M
hz : z ∈ g x
y : M
hy : x + y ∈ s
⊢ z ∈ g (x + y)
have 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
Tactic: simp only [AddSemigroupIdeal.mem_closure'', mem_diff, SetLike.mem_coe, mem_singleton_iff,
      g] at hz ⊢
Cleared hypotheses: hz
-- 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})
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
⊢ ∃ (y_1 : M) (z_1 : M), (z_1 ∈ f (x + y) ∧ ¬z_1 = 0) ∧ y_1 + z_1 = z
have 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
Tactic: rcases hz with ⟨y', z, ⟨hz₁, hz₂⟩, rfl⟩
Cleared hypotheses: z, hz
-- 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})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
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
have hz₃ : x + z ∈ s
Tactic: rw [hf _ hx] at hz₁
Cleared hypotheses: hz₁, hz₂
-- 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})
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
have refine : z ∈ f (x + y)
Tactic: refine ⟨y', z, ⟨?_, hz₂⟩, rfl⟩
-- 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})
x : M
hx : x ∈ s
y : M
hy : x + y ∈ s
y' z : M
hz₁ : x + z ∈ s
hz₂ : ¬z = 0
⊢ z ∈ f (x + y)
have rw : x + y + z ∈ s
Tactic: rw [hf _ 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})
⊢ ∃ x ∈ s, IsSemilinearSet.{u_1} (M := M) {y : M | y ∈ s ∧ x ≤ y}
have hg : ∀ 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₁