awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
S : Set (Set M)
a : Set M
s : Set (Set M)
h : a ∉ s
hs : s.Finite
ih : ∀ (hS' : ∀ s_1 ∈ s, IsSemilinearSet s_1), IsSemilinearSet (⋂₀ s)
hS' : ∀ s_1 ∈ insert a s, IsSemilinearSet s_1
⊢ IsSemilinearSet a ∧ ∀ a ∈ s, IsSemilinearSet a

Tactic:
simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'

Premises used: forall_eq_or_imp, Set.mem_insert_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
S : Set (Set M)
a : Set M
s : Set (Set M)
h : a ∉ s
hs : s.Finite
ih : ∀ (hS' : ∀ s_1 ∈ s, IsSemilinearSet s_1), IsSemilinearSet (⋂₀ s)
hS' : IsSemilinearSet a ∧ ∀ a ∈ s, IsSemilinearSet a
⊢ IsSemilinearSet (⋂₀ insert a s)

Tactic:
simpa using hS'.1.inter (ih hS'.2)

Premises used: IsSemilinearSet.inter, And.right, And.left
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
S : Set (Set M)
hS : S.Finite
hS' : ∀ s ∈ S, IsSemilinearSet s
empty :
  ∀ (hS' : ∀ (s : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsSemilinearSet s),
    IsSemilinearSet.{u_1} (M := M) (⋂₀ ∅)
insert :
  ∀ {a : Set M} {s : Set (Set M)},
    a ∉ s →
      s.Finite →
        ∀ (ih : ∀ (hS' : ∀ s_1 ∈ s, IsSemilinearSet s_1), IsSemilinearSet (⋂₀ s))
          (hS' : ∀ s_1 ∈ Insert.insert a s, IsSemilinearSet s_1), IsSemilinearSet (⋂₀ Insert.insert a s)
⊢ IsSemilinearSet (⋂₀ S)

Tactic:
induction S, hS using Finite.induction_on with
  | empty => simp
  | insert _ _ ih =>
    simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
    simpa using hS'.1.inter (ih hS'.2)

Premises used: Insert.insert, forall_eq_or_imp, Set.mem_insert_iff, IsSemilinearSet.empty
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
inst_2 : Finite ι
s : ι → Set M
hs : ∀ (i : ι), IsSemilinearSet (s i)
apply : ∀ s_1 ∈ range s, IsSemilinearSet s_1
⊢ IsSemilinearSet (⋂₀ range s)

Tactic:
apply sInter (finite_range s)

Premises used: Set.finite_range, IsSemilinearSet.sInter
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
inst_2 : Finite ι
s : ι → Set M
hs : ∀ (i : ι), IsSemilinearSet (s i)
⊢ ∀ s_1 ∈ range s, IsSemilinearSet s_1

Tactic:
simpa
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
rw : IsSemilinearSet (⋂₀ (t '' s))
⊢ IsSemilinearSet.{u_1} (M := M) (⋂ i ∈ s, t i)

Tactic:
rw [← sInter_image]

Premises used: Set.sInter_image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
apply : ∀ s_1 ∈ t '' s, IsSemilinearSet s_1
⊢ IsSemilinearSet (⋂₀ (t '' s))

Tactic:
apply sInter (hs.image t)

Premises used: Set.Finite.image, IsSemilinearSet.sInter
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ ∀ s_1 ∈ t '' s, IsSemilinearSet s_1

Tactic:
simpa
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : AddMonoid.FG M
s : Finset ι
t : ι → Set M
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ IsSemilinearSet.{u_1} (M := M) (⋂ i ∈ s, t i)

Tactic:
biInter s.finite_toSet ht

Premises used: IsSemilinearSet.biInter, Finset.finite_toSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
x y : ι → ℕ
⊢ Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) ↔ x = y

Tactic:
⟨fun h => ?_, congr_arg toRatVec⟩

Premises used: _private.0.toRatVec, congr_arg, Iff.intro, DFunLike.coe
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
x y : ι → ℕ
refine :
  ∀ (h : Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ)),
    x = y
⊢ Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) ↔ x = y

Tactic:
refine ⟨fun h => ?_, congr_arg toRatVec⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
x y : ι → ℕ
h : Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ)
h₁ : ∀ (i : ι), x i = y i
⊢ x = y

Tactic:
ext i
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
x y : ι → ℕ
h : Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ)
i : ι
⊢ x i = y i

Tactic:
simpa [toRatVec] using congr_fun h i

Premises used: _private.0.toRatVec, congr_fun
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
x y : ι → ℕ
h :
  ∀ (a : ι),
    LE.le (α := (fun (a : ι) ↦ ℚ) a) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x a) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y a) ↔
      x a ≤ y a
⊢ LE.le (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) ↔ x ≤ y

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
x y : ι → ℕ
⊢ ∀ (a : ι),
    LE.le (α := (fun (a : ι) ↦ ℚ) a) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x a) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y a) ↔
      x a ≤ y a

Tactic:
simp [toRatVec]

Premises used: _private.0.toRatVec
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
x : ι → ℕ
rw : 0 ≤ x
⊢ LE.le (α := ι → ℚ) (0 : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)

Tactic:
rw [← map_zero toRatVec, toRatVec_mono]

Premises used: _private.0.toRatVec_mono, map_zero, _private.0.toRatVec
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
x : ι → ℕ
⊢ 0 ≤ x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
rw :
  ∀ (t : Finset (ι → ℕ)) (g : (ι → ℕ) → ℤ),
    (↑t : Set (ι → ℕ)) ⊆ s →
      (∀ i ∉ t, g i = 0) →
        Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (g i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0 →
          ∀ i ∈ t, g i = 0
⊢ LinearIndepOn ℚ (M := ι → ℚ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) s

Tactic:
rw [LinearIndepOn, ← LinearIndependent.iff_fractionRing ℤ ℚ, ← LinearIndepOn, linearIndepOn_iff'']

Premises used: Rat, linearIndepOn_iff'', Int, LinearIndependent.iff_fractionRing, LinearIndepOn
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
rw :
  ∀ (hs : ∀ (t : Finset (ι → ℕ)), (↑t : Set (ι → ℕ)) ⊆ s → LinearIndepOn ℕ id (↑t : Set (ι → ℕ))) (t : Finset (ι → ℕ))
    (f : (ι → ℕ) → ℤ) (ht : (↑t : Set (ι → ℕ)) ⊆ s) (hf : ∀ i ∉ t, f i = 0)
    (heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0)
    (i : ι → ℕ) (hi : i ∈ t), f i = 0
⊢ f i = 0

Tactic:
rw [linearIndepOn_iff_linearIndepOn_finset] at hs

Premises used: linearIndepOn_iff_linearIndepOn_finset
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : ∀ (t : Finset (ι → ℕ)), (↑t : Set (ι → ℕ)) ⊆ s → LinearIndepOn ℕ id (↑t : Set (ι → ℕ))
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
⊢ LinearIndepOn ℕ id (↑t : Set (ι → ℕ))

Tactic:
specialize hs t ht
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : LinearIndepOn ℕ id (↑t : Set (ι → ℕ))
⊢ ∀ (f g : (ι → ℕ) → ℕ), Eq (α := ι → ℕ) (∑ i ∈ t, f i • id i) (∑ i ∈ t, g i • id i) → ∀ i ∈ t, f i = g i

Tactic:
rw [linearIndepOn_finset_iffₛ] at hs

Premises used: linearIndepOn_finset_iffₛ
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : ∀ (f g : (ι → ℕ) → ℕ), Eq (α := ι → ℕ) (∑ i ∈ t, f i • id i) (∑ i ∈ t, g i • id i) → ∀ i ∈ t, f i = g i
specialize :
  Eq (α := ι → ℕ) (∑ i ∈ t, (Int.toNat ∘ f) i • id i) (∑ i ∈ t, (Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) i • id i)
specialize₁ : ∀ (hs : (Int.toNat ∘ f) i = (Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) i), f i = 0
⊢ f i = 0

Tactic:
specialize hs (Int.toNat ∘ f) (Int.toNat ∘ (-·) ∘ f) ?_ i hi

Premises used: Function.comp, Int.toNat, Neg.neg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : ∀ (f g : (ι → ℕ) → ℕ), Eq (α := ι → ℕ) (∑ i ∈ t, f i • id i) (∑ i ∈ t, g i • id i) → ∀ i ∈ t, f i = g i
simp_rw :
  Eq (α := ι → ℚ) (∑ x ∈ t, (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) x • id x))
    (∑ x ∈ t, (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) x • id x))
⊢ Eq (α := ι → ℕ) (∑ i ∈ t, (Int.toNat ∘ f) i • id i) (∑ i ∈ t, (Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) i • id i)

Tactic:
simp_rw [← toRatVec_inj, map_sum]

Premises used: map_sum, _private.0.toRatVec_inj
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : ∀ (f g : (ι → ℕ) → ℕ), Eq (α := ι → ℕ) (∑ i ∈ t, f i • id i) (∑ i ∈ t, g i • id i) → ∀ i ∈ t, f i = g i
rw :
  Eq (α := ι → ℚ)
    (∑ x ∈ t,
      HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) x • id x) : ι → ℚ)
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) x • id x) : ι → ℚ))
    (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ))
⊢ Eq (α := ι → ℚ) (∑ x ∈ t, (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) x • id x))
    (∑ x ∈ t, (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) x • id x))

Tactic:
rw [← sub_eq_zero, ← Finset.sum_sub_distrib, ← heq]

Premises used: sub_eq_zero, Finset.sum_sub_distrib
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : ∀ (f g : (ι → ℕ) → ℕ), Eq (α := ι → ℕ) (∑ i ∈ t, f i • id i) (∑ i ∈ t, g i • id i) → ∀ i ∈ t, f i = g i
⊢ Eq (α := ι → ℚ)
    (∑ x ∈ t,
      HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) x • id x) : ι → ℚ)
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) x • id x) : ι → ℚ))
    (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ))

Tactic:
Finset.sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : ∀ (f g : (ι → ℕ) → ℕ), Eq (α := ι → ℕ) (∑ i ∈ t, f i • id i) (∑ i ∈ t, g i • id i) → ∀ i ∈ t, f i = g i
refine :
  ∀ (j : ι → ℕ) (hj : j ∈ t),
    HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) j • id j) : ι → ℚ)
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) j • id j) : ι → ℚ) =
      HSMul.hSMul (β := ι → ℚ) (f j) ((toRatVec : (a : ι → ℕ) → ι → ℚ) j : ι → ℚ)
⊢ Eq (α := ι → ℚ)
    (∑ x ∈ t,
      HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) x • id x) : ι → ℚ)
        ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) x • id x) : ι → ℚ))
    (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ))

Tactic:
refine Finset.sum_congr rfl fun j hj => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : ∀ (f g : (ι → ℕ) → ℕ), Eq (α := ι → ℕ) (∑ i ∈ t, f i • id i) (∑ i ∈ t, g i • id i) → ∀ i ∈ t, f i = g i
j : ι → ℕ
hj : j ∈ t
rw :
  HSMul.hSMul (β := ι → ℚ) (HSub.hSub (α := ℤ) (↑(f j).toNat : ℤ) (↑(-f j).toNat : ℤ))
    ((toRatVec : (a : ι → ℕ) → ι → ℚ) j : ι → ℚ)
| HSMul.hSMul (β := ι → ℚ) (f j) ((toRatVec : (a : ι → ℕ) → ι → ℚ) j : ι → ℚ)

Tactic:
rw [← (f j).toNat_sub_toNat_neg]

Premises used: Int.toNat_sub_toNat_neg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : ∀ (f g : (ι → ℕ) → ℕ), Eq (α := ι → ℕ) (∑ i ∈ t, f i • id i) (∑ i ∈ t, g i • id i) → ∀ i ∈ t, f i = g i
j : ι → ℕ
hj : j ∈ t
conv_rhs :
  HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) j • id j) : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) j • id j) : ι → ℚ) =
    HSMul.hSMul (β := ι → ℚ) (HSub.hSub (α := ℤ) (↑(f j).toNat : ℤ) (↑(-f j).toNat : ℤ))
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) j : ι → ℚ)
⊢ HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) j • id j) : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) j • id j) : ι → ℚ) =
    HSMul.hSMul (β := ι → ℚ) (f j) ((toRatVec : (a : ι → ℕ) → ι → ℚ) j : ι → ℚ)

Tactic:
conv_rhs => rw [← (f j).toNat_sub_toNat_neg]

Premises used: Int.toNat_sub_toNat_neg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : ∀ (f g : (ι → ℕ) → ℕ), Eq (α := ι → ℕ) (∑ i ∈ t, f i • id i) (∑ i ∈ t, g i • id i) → ∀ i ∈ t, f i = g i
j : ι → ℕ
hj : j ∈ t
⊢ HSub.hSub (α := ι → ℚ) (β := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) j • id j) : ι → ℚ)
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) j • id j) : ι → ℚ) =
    HSMul.hSMul (β := ι → ℚ) (HSub.hSub (α := ℤ) (↑(f j).toNat : ℤ) (↑(-f j).toNat : ℤ))
      ((toRatVec : (a : ι → ℕ) → ι → ℚ) j : ι → ℚ)

Tactic:
simp only [sub_smul, map_nsmul, natCast_zsmul, Function.comp_apply, id_eq]

Premises used: sub_smul, Function.comp_apply, map_nsmul, natCast_zsmul, id_eq
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : (Int.toNat ∘ f) i = (Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) i
rw : (f i).toNat = (-f i).toNat
⊢ f i = 0

Tactic:
rw [← (f i).toNat_sub_toNat_neg, sub_eq_zero, Int.natCast_inj]

Premises used: sub_eq_zero, Int.toNat_sub_toNat_neg, Int.natCast_inj
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : (↑t : Set (ι → ℕ)) ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : Eq (α := ι → ℚ) (∑ i ∈ t, HSMul.hSMul (β := ι → ℚ) (f i) ((toRatVec : (a : ι → ℕ) → ι → ℚ) i : ι → ℚ)) 0
i : ι → ℕ
hi : i ∈ t
hs : (Int.toNat ∘ f) i = (Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) i
⊢ (f i).toNat = (-f i).toNat

Tactic:
simpa using hs
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
⊢ hs.periods (s := s).Finite

Tactic:
hs.choose_spec.choose_spec.1

Premises used: Exists.choose_spec, _private.0.IsProperLinearSet.periods, And.left
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
⊢ LinearIndepOn ℕ id (hs.periods (s := s))

Tactic:
hs.choose_spec.choose_spec.2.1

Premises used: Exists.choose_spec, _private.0.IsProperLinearSet.periods, And.right, And.left
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
⊢ s = hs.base (s := s) +ᵥ (↑(closure (hs.periods (s := s))) : Set (ι → ℕ))

Tactic:
hs.choose_spec.choose_spec.2.2

Premises used: _private.0.IsProperLinearSet.base, Exists.choose_spec, Set.Mem, setOf, _private.0.IsProperLinearSet.periods, And.right
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ hs.periods (s := s) ⊆ hs.basisSet (s := s)

Tactic:
(linearIndepOn_toRatVec hs.linearIndepOn_periods).subset_extend _

Premises used: _private.0.linearIndepOn_toRatVec, _private.0.IsProperLinearSet.linearIndepOn_periods, LinearIndepOn.subset_extend, _private.0.IsProperLinearSet.basisSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ hs.basisSet (s := s) ⊆ hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)

Tactic:
(linearIndepOn_toRatVec hs.linearIndepOn_periods).extend_subset _

Premises used: LinearIndepOn.extend_subset, _private.0.linearIndepOn_toRatVec, _private.0.IsProperLinearSet.linearIndepOn_periods, _private.0.IsProperLinearSet.basisSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ hs.basisSet (s := s).Finite

Tactic:
(hs.finite_periods.union (finite_range _)).subset hs.basisSet_subset_union

Premises used: Set.Finite.union, Set.finite_range, _private.0.IsProperLinearSet.basisSet_subset_union, Set.Finite.subset, _private.0.IsProperLinearSet.finite_periods
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ LinearIndepOn ℚ (M := ι → ℚ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (hs.basisSet (s := s))

Tactic:
(linearIndepOn_toRatVec hs.linearIndepOn_periods).linearIndepOn_extend _

Premises used: _private.0.linearIndepOn_toRatVec, _private.0.IsProperLinearSet.linearIndepOn_periods, LinearIndepOn.linearIndepOn_extend, _private.0.IsProperLinearSet.basisSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤

Tactic:
rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]

Premises used: LinearIndepOn.span_image_extend_eq_span_image, _private.0.linearIndepOn_toRatVec, _private.0.IsProperLinearSet.linearIndepOn_periods, top_le_iff, _private.0.IsProperLinearSet.basisSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
apply :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
⊢ LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))

Tactic:
apply (span_mono (image_mono subset_union_right)).trans'

Premises used: Set.image_mono, Set.subset_union_right, Submodule.span_mono, LE.le.trans'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
⊢ LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))

Tactic:
rw [top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))) ⊤

Tactic:
(Pi.basisFun ℚ ι).span_eq

Premises used: Rat, Pi.basisFun, Module.Basis.span_eq
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
h :
  Eq (α := Set (ι → ℚ))
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
    (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))
⊢ Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤

Tactic:
convert! (Pi.basisFun ℚ ι).span_eq

Premises used: Rat, Pi.basisFun, Module.Basis.span_eq
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
h :
  ∀ (x : ι → ℚ),
    Membership.mem (γ := Set (ι → ℚ))
        (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
        x ↔
      Membership.mem (γ := Set (ι → ℚ)) (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ)) x
⊢ Eq (α := Set (ι → ℚ))
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
    (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))

Tactic:
ext