awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
refine :
  v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)) =
    setOf
      (Formula.Realize (L := presburger[[(↑A : Type)]])
        (Formula.iExs (↥t)
          (Formula.iInf fun (i : α) ↦
            Term.equal (var (Sum.inl i))
              (HAdd.hAdd (α := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) (↑(v i) : presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                  (presburger.sum Finset.univ fun (x : ↥t) ↦
                    HSMul.hSMul (β := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) ((↑x : α → ℕ) i)
                      (var (Sum.inr (Sum.inr x))))).varsToConstants)))
⊢ A.Definable presburger (v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)))

Tactic:
refine ⟨Formula.iExs t (Formula.iInf fun i : α =>
    (Term.var (Sum.inl i)).equal
      (Term.varsToConstants
        ((v i : presburger.Term _) + presburger.sum Finset.univ fun x : t =>
          x.1 i • Term.var (Sum.inr (Sum.inr x))))), ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
h :
  ∀ (x : α → ℕ),
    x ∈ v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)) ↔
      Membership.mem (γ := Set (α → ℕ))
        (setOf
          (Formula.Realize (L := presburger[[(↑A : Type)]])
            (Formula.iExs (↥t)
              (Formula.iInf fun (i : α) ↦
                Term.equal (var (Sum.inl i))
                  (HAdd.hAdd (α := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                      (↑(v i) : presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                      (presburger.sum Finset.univ fun (x : ↥t) ↦
                        HSMul.hSMul (β := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) ((↑x : α → ℕ) i)
                          (var (Sum.inr (Sum.inr x))))).varsToConstants))))
        x
⊢ v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)) =
    setOf
      (Formula.Realize (L := presburger[[(↑A : Type)]])
        (Formula.iExs (↥t)
          (Formula.iInf fun (i : α) ↦
            Term.equal (var (Sum.inl i))
              (HAdd.hAdd (α := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) (↑(v i) : presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                  (presburger.sum Finset.univ fun (x : ↥t) ↦
                    HSMul.hSMul (β := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) ((↑x : α → ℕ) i)
                      (var (Sum.inr (Sum.inr x))))).varsToConstants)))

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
h :
  (∃ (a : ↥t → ℕ), v + ∑ x ∈ t.attach, (↑(a x) : α → ℕ) * (↑x : α → ℕ) = x) ↔
    ∃ (i : ↥t → ℕ), ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * i x
⊢ x ∈ v +ᵥ (↑(AddSubmonoid.closure (↑t : Set (α → ℕ))) : Set (α → ℕ)) ↔
    Membership.mem (γ := Set (α → ℕ))
      (setOf
        (Formula.Realize (L := presburger[[(↑A : Type)]])
          (Formula.iExs (↥t)
            (Formula.iInf fun (i : α) ↦
              Term.equal (var (Sum.inl i))
                (HAdd.hAdd (α := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                    (↑(v i) : presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t))
                    (presburger.sum Finset.univ fun (x : ↥t) ↦
                      HSMul.hSMul (β := presburger.Term ((↑A : Type) ⊕ α ⊕ ↥t)) ((↑x : α → ℕ) i)
                        (var (Sum.inr (Sum.inr x))))).varsToConstants))))
      x

Tactic:
simp only [mem_vadd_set, SetLike.mem_coe, AddSubmonoid.mem_closure_finset', Finset.univ_eq_attach,
    nsmul_eq_mul, vadd_eq_add, ↓existsAndEq, true_and, mem_setOf_eq, Formula.realize_iExs,
    Formula.realize_iInf, Formula.realize_equal, Term.realize_var, Sum.elim_inl,
    Term.realize_varsToConstants, coe_con, presburger.realize_add, presburger.realize_natCast,
    Nat.cast_id, presburger.realize_sum, presburger.realize_nsmul, Sum.elim_inr, smul_eq_mul]

Premises used: FirstOrder.Language.Formula.realize_equal, FirstOrder.Language.coe_con, Set.mem_vadd_set, Nat.cast_id, FirstOrder.Language.presburger.realize_sum, FirstOrder.Language.presburger.realize_add, FirstOrder.Language.presburger.realize_natCast, ExistsAndEq.existsAndEq, Set.mem_setOf_eq, Sum.elim_inr, Finset.univ_eq_attach, FirstOrder.Language.Term.realize_var, FirstOrder.Language.presburger.realize_nsmul, SetLike.mem_coe, FirstOrder.Language.Formula.realize_iInf, vadd_eq_add, nsmul_eq_mul, Sum.elim_inl, smul_eq_mul, AddSubmonoid.mem_closure_finset', FirstOrder.Language.Formula.realize_iExs, FirstOrder.Language.Term.realize_varsToConstants, true_and
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
h :
  ∀ (a : ↥t → ℕ),
    v + ∑ x ∈ t.attach, (↑(a x) : α → ℕ) * (↑x : α → ℕ) = x ↔
      ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * a x
⊢ (∃ (a : ↥t → ℕ), v + ∑ x ∈ t.attach, (↑(a x) : α → ℕ) * (↑x : α → ℕ) = x) ↔
    ∃ (i : ↥t → ℕ), ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * i x

Tactic:
congr! with a
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
a : ↥t → ℕ
h :
  (∀ (x_1 : α), x x_1 = HAdd.hAdd (β := α → ℕ) v (∑ x ∈ t.attach, (↑x : α → ℕ) * (↑(a x) : α → ℕ)) x_1) ↔
    ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * a x
⊢ v + ∑ x ∈ t.attach, (↑(a x) : α → ℕ) * (↑x : α → ℕ) = x ↔ ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * a x

Tactic:
simp_rw [Eq.comm (b := x), fun x : t => mul_comm (a x : α → ℕ) x, funext_iff]

Premises used: funext_iff, Nat.cast, Eq.comm, mul_comm, Subtype.val
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
a : ↥t → ℕ
h :
  ∀ (i : α),
    x i = HAdd.hAdd (β := α → ℕ) v (∑ x ∈ t.attach, (↑x : α → ℕ) * (↑(a x) : α → ℕ)) i ↔
      x i = v i + ∑ x ∈ t.attach, (↑x : α → ℕ) i * a x
⊢ (∀ (x_1 : α), x x_1 = HAdd.hAdd (β := α → ℕ) v (∑ x ∈ t.attach, (↑x : α → ℕ) * (↑(a x) : α → ℕ)) x_1) ↔
    ∀ (b : α), x b = v b + ∑ x ∈ t.attach, (↑x : α → ℕ) b * a x

Tactic:
congr! 1 with i
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
v : α → ℕ
t : Finset (α → ℕ)
x : α → ℕ
a : ↥t → ℕ
i : α
⊢ x i = HAdd.hAdd (β := α → ℕ) v (∑ x ∈ t.attach, (↑x : α → ℕ) * (↑(a x) : α → ℕ)) i ↔
    x i = v i + ∑ x ∈ t.attach, (↑x : α → ℕ) i * a x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst : Finite α
hs : IsSemilinearSet s
⊢ ∃ (S : Finset (Set (α → ℕ))), (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set (α → ℕ)))

Tactic:
rw [isSemilinearSet_iff] at hs

Premises used: isSemilinearSet_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
s : Set (α → ℕ)
A : Set ℕ
inst : Finite α
hs : ∃ (S : Finset (Set (α → ℕ))), (∀ t ∈ S, IsLinearSet t) ∧ s = ⋃₀ (↑S : Set (Set (α → ℕ)))
rcases :
  ∀ (S : Finset (Set (α → ℕ))) (hS : ∀ t ∈ S, IsLinearSet t), A.Definable presburger (⋃₀ (↑S : Set (Set (α → ℕ))))
⊢ A.Definable presburger s

Tactic:
rcases hs with ⟨S, hS, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
choose :
  ∀ (φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α) (hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize),
    A.Definable presburger (⋃₀ (↑S : Set (Set (α → ℕ))))
⊢ A.Definable presburger (⋃₀ (↑S : Set (Set (α → ℕ))))

Tactic:
choose φ hφ using fun s : S => (hS s.1 s.2).definable

Premises used: Subtype.val, IsLinearSet.definable, Subtype.property
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α
hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize
⊢ A.Definable presburger (⋃₀ (↑S : Set (Set (α → ℕ))))

Tactic:
⟨Formula.iSup φ, ?_⟩

Premises used: Set.Definable, FirstOrder.Language.Formula.iSup, Exists.intro
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α
hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize
refine : ⋃₀ (↑S : Set (Set (α → ℕ))) = setOf (Formula.iSup φ).Realize
⊢ A.Definable presburger (⋃₀ (↑S : Set (Set (α → ℕ))))

Tactic:
refine ⟨Formula.iSup φ, ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α
hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize
h :
  ∀ (x : α → ℕ), x ∈ ⋃₀ (↑S : Set (Set (α → ℕ))) ↔ Membership.mem (γ := Set (α → ℕ)) (setOf (Formula.iSup φ).Realize) x
⊢ ⋃₀ (↑S : Set (Set (α → ℕ))) = setOf (Formula.iSup φ).Realize

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α
hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize
x : α → ℕ
⊢ ∀ (s : Set (α → ℕ)) (hs : s ∈ S) (x : α → ℕ),
    Membership.mem (γ := Set (α → ℕ)) (setOf (φ (Subtype.mk (p := fun (x : Set (α → ℕ)) ↦ x ∈ S) s hs)).Realize) x ↔
      x ∈ (↑(Subtype.mk (p := fun (x : Set (α → ℕ)) ↦ x ∈ S) s hs) : Set (α → ℕ))

Tactic:
have := fun s hs x => Set.ext_iff.1 (hφ ⟨s, hs⟩).symm x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Finite α
S : Finset (Set (α → ℕ))
hS : ∀ t ∈ S, IsLinearSet t
φ : (s : ↥S) → presburger[[(↑A : Type)]].Formula α
hφ : ∀ (s : ↥S), (↑s : Set (α → ℕ)) = setOf (φ s).Realize
x : α → ℕ
this :
  ∀ (s : Set (α → ℕ)) (hs : s ∈ S) (x : α → ℕ),
    (φ (Subtype.mk (p := fun (x : Set (α → ℕ)) ↦ x ∈ S) s hs)).Realize x ↔ x ∈ s
⊢ x ∈ ⋃₀ (↑S : Set (Set (α → ℕ))) ↔ Membership.mem (γ := Set (α → ℕ)) (setOf (Formula.iSup φ).Realize) x

Tactic:
simp [this]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
i : α
⊢ ∀ (v : α → ℕ), v i = 0 + Pi.single (M := fun (a : α) ↦ ℕ) i 1 ⬝ᵥ v

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
i : α
⊢ ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), v i = k + u ⬝ᵥ v

Tactic:
exact ⟨0, Pi.single i 1, by simp⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
l : ℕ
ts : Fin l → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : presburger.Functions l
func :
  ∀ (k : Fin l → ℕ) (u : Fin l → α → ℕ) (ih : ∀ (a : Fin l) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v),
    ∃ (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
⊢ ∃ (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

Tactic:
choose k u ih using ih
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.zero) fun (i : Fin 0) ↦
          Term.realize v (ts i)) =
        k + u ⬝ᵥ v

Tactic:
⟨0, 0, fun v => ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
func :
  ∀ (v : α → ℕ),
    (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.zero) fun (i : Fin 0) ↦
        Term.realize v (ts i)) =
      0 + 0 ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.zero) fun (i : Fin 0) ↦
          Term.realize v (ts i)) =
        k + u ⬝ᵥ v

Tactic:
refine ⟨0, 0, fun v => ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
v : α → ℕ
⊢ (Structure.funMap (L := presburger) (n := 0) presburgerFunc.zero fun (i : Fin 0) ↦ Term.realize v (ts i)) = 0 + 0 ⬝ᵥ v

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.one) fun (i : Fin 0) ↦
          Term.realize v (ts i)) =
        k + u ⬝ᵥ v

Tactic:
⟨1, 0, fun v => ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
func :
  ∀ (v : α → ℕ),
    (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.one) fun (i : Fin 0) ↦
        Term.realize v (ts i)) =
      1 + 0 ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.one) fun (i : Fin 0) ↦
          Term.realize v (ts i)) =
        k + u ⬝ᵥ v

Tactic:
refine ⟨1, 0, fun v => ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
k : Fin 0 → ℕ
u : Fin 0 → α → ℕ
ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
v : α → ℕ
⊢ (Structure.funMap (L := presburger) (n := 0) presburgerFunc.one fun (i : Fin 0) ↦ Term.realize v (ts i)) = 1 + 0 ⬝ᵥ v

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 2 → presburger[[(↑A : Type)]].Term α
k : Fin 2 → ℕ
u : Fin 2 → α → ℕ
ih : ∀ (a : Fin 2) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 2) (Sum.inl presburgerFunc.add) fun (i : Fin 2) ↦
          Term.realize v (ts i)) =
        k + u ⬝ᵥ v

Tactic:
⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 2 → presburger[[(↑A : Type)]].Term α
k : Fin 2 → ℕ
u : Fin 2 → α → ℕ
ih : ∀ (a : Fin 2) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
func :
  ∀ (v : α → ℕ),
    (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 2) (Sum.inl presburgerFunc.add) fun (i : Fin 2) ↦
        Term.realize v (ts i)) =
      k 0 + k 1 + (u 0 + u 1) ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 2) (Sum.inl presburgerFunc.add) fun (i : Fin 2) ↦
          Term.realize v (ts i)) =
        k + u ⬝ᵥ v

Tactic:
refine ⟨k 0 + k 1, u 0 + u 1, fun v => ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 2 → presburger[[(↑A : Type)]].Term α
k : Fin 2 → ℕ
u : Fin 2 → α → ℕ
ih : ∀ (a : Fin 2) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
v : α → ℕ
func :
  (Structure.funMap (L := presburger) (n := 2) presburgerFunc.add fun (i : Fin 2) ↦ Term.realize v (ts i)) =
    k 0 + u 0 ⬝ᵥ v + (k 1 + u 1 ⬝ᵥ v)
⊢ (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 2) (Sum.inl presburgerFunc.add) fun (i : Fin 2) ↦
      Term.realize v (ts i)) =
    k 0 + k 1 + (u 0 + u 1) ⬝ᵥ v

Tactic:
rw [withConstants_funMap_sumInl, add_dotProduct, add_left_comm, add_assoc, add_left_comm,
          ← add_assoc]

Premises used: add_left_comm, add_assoc, FirstOrder.Language.withConstants_funMap_sumInl, add_dotProduct
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 2 → presburger[[(↑A : Type)]].Term α
k : Fin 2 → ℕ
u : Fin 2 → α → ℕ
ih : ∀ (a : Fin 2) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
v : α → ℕ
⊢ (Structure.funMap (L := presburger) (n := 2) presburgerFunc.add fun (i : Fin 2) ↦ Term.realize v (ts i)) =
    k 0 + u 0 ⬝ᵥ v + (k 1 + u 1 ⬝ᵥ v)

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
l : ℕ
ts : Fin l → presburger[[(↑A : Type)]].Term α
f : presburger.Functions l
k : Fin l → ℕ
u : Fin l → α → ℕ
ih : ∀ (a : Fin l) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v
func :
  ∀ (ts : Fin 0 → presburger[[(↑A : Type)]].Term α) (k : Fin 0 → ℕ) (u : Fin 0 → α → ℕ)
    (ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.zero) fun (i : Fin 0) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
func₁ :
  ∀ (ts : Fin 0 → presburger[[(↑A : Type)]].Term α) (k : Fin 0 → ℕ) (u : Fin 0 → α → ℕ)
    (ih : ∀ (a : Fin 0) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inl presburgerFunc.one) fun (i : Fin 0) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
func₂ :
  ∀ (ts : Fin 2 → presburger[[(↑A : Type)]].Term α) (k : Fin 2 → ℕ) (u : Fin 2 → α → ℕ)
    (ih : ∀ (a : Fin 2) (v : α → ℕ), Term.realize v (ts a) = k a + u a ⬝ᵥ v),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 2) (Sum.inl presburgerFunc.add) fun (i : Fin 2) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
⊢ ∃ (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

Tactic:
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]

Premises used: add_left_comm, add_assoc, FirstOrder.Language.withConstants_funMap_sumInl, add_dotProduct
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin 0), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions 0
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦ Term.realize v (ts i)) =
        k + u ⬝ᵥ v

Tactic:
⟨f, 0, fun v => ?_⟩

Premises used: Exists.intro, FirstOrder.Language.constantMap, OfNat.ofNat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin 0), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions 0
func :
  ∀ (v : α → ℕ),
    (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦ Term.realize v (ts i)) =
      (↑f : ℕ) + 0 ⬝ᵥ v
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦ Term.realize v (ts i)) =
        k + u ⬝ᵥ v

Tactic:
refine ⟨f, 0, fun v => ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin 0), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions 0
v : α → ℕ
func : Eq (α := ℕ) (↑(presburger.con f) : ℕ) (↑f : ℕ)
⊢ (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦ Term.realize v (ts i)) =
    (↑f : ℕ) + 0 ⬝ᵥ v

Tactic:
rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]

Premises used: zero_dotProduct, FirstOrder.Language.withConstants_funMap_sumInr, add_zero
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
ts : Fin 0 → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin 0), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions 0
v : α → ℕ
⊢ Eq (α := ℕ) (↑(presburger.con f) : ℕ) (↑f : ℕ)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
n : ℕ
ts : Fin (n + 1) → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin (n + 1)), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions (n + 1)
⊢ ∃ (k : ℕ) (u : α → ℕ),
    ∀ (v : α → ℕ),
      (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := n + 1) (Sum.inr f) fun (i : Fin (n + 1)) ↦
          Term.realize v (ts i)) =
        k + u ⬝ᵥ v

Tactic:
nomatch f
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability
Goal:
α : Type u_1
A : Set ℕ
inst : Fintype α
l : ℕ
ts : Fin l → presburger[[(↑A : Type)]].Term α
ih : ∀ (a : Fin l), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn (↑A : Type)).Functions l
func :
  ∀ (ts : Fin 0 → presburger[[(↑A : Type)]].Term α)
    (ih : ∀ (a : Fin 0), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v)
    (f : (constantsOn (↑A : Type)).Functions 0),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := 0) (Sum.inr f) fun (i : Fin 0) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
func₁ :
  ∀ (n : ℕ) (ts : Fin (n + 1) → presburger[[(↑A : Type)]].Term α)
    (ih : ∀ (a : Fin (n + 1)), ∃ (k : ℕ) (u : α → ℕ), ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v)
    (f : (constantsOn (↑A : Type)).Functions (n + 1)),
    ∃ (k : ℕ) (u : α → ℕ),
      ∀ (v : α → ℕ),
        (Structure.funMap (L := presburger[[(↑A : Type)]]) (n := n + 1) (Sum.inr f) fun (i : Fin (n + 1)) ↦
            Term.realize v (ts i)) =
          k + u ⬝ᵥ v
⊢ ∃ (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

Tactic:
cases l with
      | zero =>
        refine ⟨f, 0, fun v => ?_⟩
        rw [withConstants_funMap_sumInr, zero_dotProduct, add_zero]
        rfl
      | succ => nomatch f

Premises used: zero_dotProduct, FirstOrder.Language.withConstants_funMap_sumInr, add_zero