awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
l : ℕ
f : presburger[[(↑A : Type)]].Functions l
ts : Fin l → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
func :
  ∀ (f : presburger.Functions l),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := l) (Sum.inl f) fun (i : Fin l) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
func₁ :
  ∀ (f : (constantsOn (↑A : Type)).Functions l),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := l) (Sum.inr f) fun (i : Fin l) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), (Structure.funMap f fun (i : Fin l) ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v

Tactic:
cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f

Premises used: add_left_comm, add_assoc, zero_dotProduct, FirstOrder.Language.withConstants_funMap_sumInl, add_dotProduct, FirstOrder.Language.withConstants_funMap_sumInr, add_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
var :
  ∀ (i : α),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (Language.var i) = k + u ⬝ᵥ v
var₁ : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), v i = k + u ⬝ᵥ v
func :
  ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
    (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (Language.func f ts) = k + u ⬝ᵥ v
func₁ :
  ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
    (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), (Structure.funMap f fun (i : Fin l) ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v

Tactic:
induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f

Premises used: add_left_comm, add_assoc, zero_dotProduct, FirstOrder.Language.Term.func, FirstOrder.Language.withConstants_funMap_sumInl, add_dotProduct, FirstOrder.Language.Term.var, FirstOrder.Language.withConstants_funMap_sumInr, FirstOrder.Language.Term.realize, add_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
t : presburger[[(↑A : Type)]].Term α
var :
  ∀ (i : α),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize (L := presburger[[(↑A : Type)]]) v (Language.var i) = k + u ⬝ᵥ v
var₁ : ∀ (i : α), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), v i = k + u ⬝ᵥ v
func :
  ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
    (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (Language.func f ts) = k + u ⬝ᵥ v
func₁ :
  ∀ {l : ℕ} (f : presburger[[(↑A : Type)]].Functions l) (ts : Fin l → presburger[[(↑A : Type)]].Term α)
    (ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), (Structure.funMap f fun (i : Fin l) ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v t = k + u ⬝ᵥ v

Tactic:
classical
  induction t with simp only [Term.realize]
  | var i =>
    exact ⟨0, Pi.single i 1, by simp⟩
  | @func l f ts ih =>
    cases f with
    | inl f =>
      choose k u ih using ih
      cases f with
      | zero =>
        refine ⟨0, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp
      | one =>
        refine ⟨1, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInl]
        simp [ih]
      | add =>
        refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
        rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]
        simp [ih]
    | inr f =>
      cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f

Premises used: add_left_comm, add_assoc, zero_dotProduct, FirstOrder.Language.Term.func, FirstOrder.Language.withConstants_funMap_sumInl, add_dotProduct, FirstOrder.Language.Term.var, FirstOrder.Language.withConstants_funMap_sumInr, FirstOrder.Language.Term.realize, add_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
⊢ IsSemilinearSet (M := α → ℕ)
    (image (α := α ⊕ Fin 0 → ℕ) (⇑(LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0)) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
      {v : α ⊕ Fin 0 → ℕ | BoundedFormula.Realize φ (v ∘ Sum.inl) (v ∘ Sum.inr)})

Tactic:
(isSemilinearSet_boundedFormula_realize φ).image (LinearMap.funLeft ℕ ℕ e.symm)

Premises used: FirstOrder.Language.presburger.isSemilinearSet_boundedFormula_realize, IsSemilinearSet.image, LinearMap.funLeft, Nat, Equiv.symm, DFunLike.coe
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
h :
  Eq (α := Set (α → ℕ)) (setOf φ.Realize)
    (image (α := α ⊕ Fin 0 → ℕ) (⇑(LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0)) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
      {v : α ⊕ Fin 0 → ℕ | BoundedFormula.Realize φ (v ∘ Sum.inl) (v ∘ Sum.inr)})
⊢ IsSemilinearSet (M := α → ℕ) (setOf φ.Realize)

Tactic:
convert! (isSemilinearSet_boundedFormula_realize φ).image (LinearMap.funLeft ℕ ℕ e.symm)

Premises used: FirstOrder.Language.presburger.isSemilinearSet_boundedFormula_realize, IsSemilinearSet.image, LinearMap.funLeft, Nat, Equiv.symm, DFunLike.coe
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
h :
  ∀ (x : α → ℕ),
    Membership.mem (γ := Set (α → ℕ)) (setOf φ.Realize) x ↔
      Membership.mem (γ := Set (α → ℕ))
        (image (α := α ⊕ Fin 0 → ℕ)
          (⇑(LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0)) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
          {v : α ⊕ Fin 0 → ℕ | BoundedFormula.Realize φ (v ∘ Sum.inl) (v ∘ Sum.inr)})
        x
⊢ Eq (α := Set (α → ℕ)) (setOf φ.Realize)
    (image (α := α ⊕ Fin 0 → ℕ) (⇑(LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0)) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
      {v : α ⊕ Fin 0 → ℕ | BoundedFormula.Realize φ (v ∘ Sum.inl) (v ∘ Sum.inr)})

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
x : α → ℕ
h :
  φ.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
⊢ Membership.mem (γ := Set (α → ℕ)) (setOf φ.Realize) x ↔
    Membership.mem (γ := Set (α → ℕ))
      (image (α := α ⊕ Fin 0 → ℕ)
        (⇑(LinearMap.funLeft ℕ ℕ (⇑e.symm : (a : α) → α ⊕ Fin 0)) : (a : α ⊕ Fin 0 → ℕ) → α → ℕ)
        {v : α ⊕ Fin 0 → ℕ | BoundedFormula.Realize φ (v ∘ Sum.inl) (v ∘ Sum.inr)})
      x

Tactic:
simp only [mem_setOf_eq, mem_image]

Premises used: Set.mem_image, Set.mem_setOf_eq
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
x : α → ℕ
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
⊢ φ.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

Tactic:
rw [(e.arrowCongr (.refl ℕ)).exists_congr_left]

Premises used: Equiv.exists_congr_left, Equiv.arrowCongr, Nat, Equiv.refl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
φ : presburger[[(↑A : Type)]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
x : α → ℕ
⊢ φ.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:
simp [Formula.Realize, Unique.eq_default, Function.comp_def, LinearMap.funLeft, e]

Premises used: Unique.eq_default, Function.comp_def, LinearMap.funLeft, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
s : Set (α → ℕ)
⊢ A.Definable presburger s ↔ IsSemilinearSet s

Tactic:
⟨fun ⟨φ, hφ⟩ => hφ ▸ isSemilinearSet_formula_realize_semilinear φ, IsSemilinearSet.definable⟩

Premises used: Eq.rec, IsSemilinearSet, Iff.intro, _private.0.FirstOrder.Language.presburger.definable_iff_isSemilinearSet.match_1, Eq.symm, FirstOrder.Language.presburger.isSemilinearSet_formula_realize_semilinear, IsSemilinearSet.definable
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
A s : Set ℕ
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
⊢ A.Definable₁ presburger 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]

Premises used: LinearEquiv.funUnique, Set.preimage_setOf_eq, isSemilinearSet_image_iff, Nat, OfNat.ofNat, Fin, Set.Definable₁, FirstOrder.Language.presburger.definable_iff_isSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
A s : Set ℕ
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
⊢ 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:
simp only [LinearEquiv.funUnique_apply, Function.eval, Fin.default_eq_zero, setOf_mem_eq]

Premises used: Function.eval, Set.setOf_mem_eq, LinearEquiv.funUnique_apply, Fin.default_eq_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
A s : Set ℕ
rw : IsSemilinearSet s ↔ ∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
rw₁ rw₂ : (∃ (k : ℕ), ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ 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

Tactic:
rw [image_preimage_eq s fun x => ⟨![x], rfl⟩, Nat.isSemilinearSet_iff_ultimately_periodic]

Premises used: Nat.isSemilinearSet_iff_ultimately_periodic, Set.image_preimage_eq, Exists.intro, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
⊢ A.Definable presburger (α := Fin (Nat.succ 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:
(hmul.preimage_comp (β := Fin 2) ![0, 1, 1]).image_comp ![0]

Premises used: Set.Definable.preimage_comp, Set.Definable.image_comp, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
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})
⊢ A.Definable presburger (α := Fin 1)
    {x : Fin 1 → ℕ | Membership.mem (γ := Set ℕ) {x : ℕ | ∃ (x_1 : ℕ), x_1 * x_1 = x} (x 0)}

Tactic:
convert! (hmul.preimage_comp (β := Fin 2) ![0, 1, 1]).image_comp ![0]

Premises used: Set.Definable.preimage_comp, Set.Definable.image_comp, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
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
⊢ 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:
ext
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
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:
simpa [funext_iff, Fin.exists_fin_succ_pi] using exists_congr fun _ => Eq.comm

Premises used: funext_iff, Fin.exists_fin_succ_pi, exists_congr, Eq.comm
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
A : Set ℕ
hmul : A.Definable presburger (α := Fin 3) {v : Fin 3 → ℕ | v 0 = v 1 * v 2}
⊢ 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
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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}
⊢ ∃ (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

Premises used: FirstOrder.Language.presburger.definable₁_iff_ultimately_periodic
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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)
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
⊢ False

Tactic:
rcases hsqr with ⟨k, p, hp, h⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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)
⊢ 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 _ _))

Premises used: HMul.hMul, Max.max, Nat.le_mul_self, le_max_left, LE.le.trans'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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)
⊢ ∃ (x : ℕ), x * x = max k p * max k p + p

Tactic:
simp only [mem_setOf_eq, exists_apply_eq_apply, true_iff] at h

Premises used: true_iff, Set.mem_setOf_eq, exists_apply_eq_apply
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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
rcases : ∀ (x : ℕ) (h₁ : x * x = max k p * max k p + p), False
⊢ False

Tactic:
rcases h with ⟨x, h₁⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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
neg : ∀ (h₂ : ¬x ≤ max k p), False
⊢ False

Tactic:
by_cases h₂ : x ≤ max k p

Premises used: Max.max
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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
⊢ x * x ≤ max k p * max k p

Tactic:
apply Nat.mul_self_le_mul_self at h₂

Premises used: Nat.mul_self_le_mul_self
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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 * x ≤ max k p * max k p
⊢ False

Tactic:
grind
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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
⊢ max k p + 1 ≤ x

Tactic:
simp only [not_le, Nat.lt_iff_add_one_le] at h₂

Premises used: not_le, Nat.lt_iff_add_one_le
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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
⊢ (max k p + 1) * (max k p + 1) ≤ x * x

Tactic:
apply Nat.mul_self_le_mul_self at h₂

Premises used: Nat.mul_self_le_mul_self
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
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) * (max k p + 1) ≤ x * x
⊢ False

Tactic:
grind
-- 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
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)
⊢ 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)

Tactic:
⟨hx, hxi⟩
-- 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
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)
⊢ 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)

Tactic:
⟨hxy, hxyi⟩