awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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, (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ f) x • id x))
    (∑ x ∈ t, (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) x • id x))
have 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 : ι → ℚ))
Tactic: rw [← sub_eq_zero, ← Finset.sum_sub_distrib, ← heq]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 : ι → ℚ))
have 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 : ι → ℚ)
Tactic: refine Finset.sum_congr rfl fun j hj => ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
| HSMul.hSMul (β := ι → ℚ) (f j) ((toRatVec : (a : ι → ℕ) → ι → ℚ) j : ι → ℚ)
have rw : HSMul.hSMul (β := ι → ℚ) (HSub.hSub (α := ℤ) (↑(f j).toNat : ℤ) (↑(-f j).toNat : ℤ))
  ((toRatVec : (a : ι → ℕ) → ι → ℚ) j : ι → ℚ)
Tactic: rw [← (f j).toNat_sub_toNat_neg]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 (β := ι → ℚ) (f j) ((toRatVec : (a : ι → ℕ) → ι → ℚ) j : ι → ℚ)
have 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 : ι → ℚ)
Tactic: conv_rhs => rw [← (f j).toNat_sub_toNat_neg]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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 = 0
have rw : (f i).toNat = (-f i).toNat
Tactic: rw [← (f i).toNat_sub_toNat_neg, sub_eq_zero, Int.natCast_inj]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have rw : LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
  (span ℚ
    ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
      (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
Tactic: rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
have apply : LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
  (span ℚ
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
Tactic: apply (span_mono (image_mono subset_union_right)).trans'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
have rw : Eq (α := Submodule ℚ (ι → ℚ))
  (span ℚ
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
  ⊤
Tactic: rw [top_le_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
have h : Eq (α := Set (ι → ℚ))
  (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
  (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))
Tactic: convert! (Pi.basisFun ℚ ι).span_eq
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ Eq (α := Set (ι → ℚ))
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
    (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))
have h : ∀ (x : ι → ℚ),
  Membership.mem (γ := Set (ι → ℚ))
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))) x ↔
    Membership.mem (γ := Set (ι → ℚ)) (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℚ
⊢ Membership.mem (γ := Set (ι → ℚ))
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))) x ↔
    Membership.mem (γ := Set (ι → ℚ)) (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ)) x
have h : (∃ (a : ι), (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) a : ι → ℕ) = x) ↔
  ∃ (y : ι), (Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) y = x
Tactic: simp only [mem_image, mem_range, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℚ
⊢ (∃ (a : ι), (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) a : ι → ℕ) = x) ↔
    ∃ (y : ι), (Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) y = x
have h : ∀ (x : ι),
  Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x : ι → ℕ) : ι → ℚ)
    ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x : ι → ℚ)
Tactic: congr!
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
x : ι → ℚ
x_1 : ι
⊢ Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x_1 : ι → ℕ) : ι → ℚ)
    ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x_1 : ι → ℚ)
have h : ∀ (x : ι),
  Eq (α := ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x_1 : ι → ℕ) x)
    ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x_1 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have rw : Eq (α := Submodule ℚ (ι → ℚ))
  (span ℚ
    ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
      sorry.extend (s := hs.periods (s := s)) (t :=
        hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) sorry))
  ⊤
Tactic: classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        ⋯.extend (s := hs.periods (s := s)) (t :=
          hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) ⋯))
    ⊤
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have rw₁ : Eq (α := Submodule ℚ (ι → ℚ))
  (span ℚ
    ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
      (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
  ⊤
Tactic: classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        ⋯.extend (s := hs.periods (s := s)) (t :=
          hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) ⋯))
    ⊤
rw₁ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have rw₂ : LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
  (span ℚ
    ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
      (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
Tactic: classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        ⋯.extend (s := hs.periods (s := s)) (t :=
          hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) ⋯))
    ⊤
rw₁ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
rw₂ rw₃ rw₄ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have rw₅ : LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
  (span ℚ
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
Tactic: classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        ⋯.extend (s := hs.periods (s := s)) (t :=
          hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) ⋯))
    ⊤
rw₁ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
rw₂ rw₃ rw₄ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₅ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have rw₆ : Eq (α := Submodule ℚ (ι → ℚ))
  (span ℚ
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
  ⊤
Tactic: classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        ⋯.extend (s := hs.periods (s := s)) (t :=
          hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) ⋯))
    ⊤
rw₁ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
rw₂ rw₃ rw₄ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₅ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₆ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have h : Eq (α := Set (ι → ℚ))
  (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
  (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))
Tactic: classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        ⋯.extend (s := hs.periods (s := s)) (t :=
          hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) ⋯))
    ⊤
rw₁ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
rw₂ rw₃ rw₄ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₅ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₆ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
h :
  Eq (α := Set (ι → ℚ))
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
    (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have h₁ : ∀ (x : ι → ℚ),
  Membership.mem (γ := Set (ι → ℚ))
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))) x ↔
    Membership.mem (γ := Set (ι → ℚ)) (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ)) x
Tactic: classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        ⋯.extend (s := hs.periods (s := s)) (t :=
          hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) ⋯))
    ⊤
rw₁ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
rw₂ rw₃ rw₄ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₅ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₆ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
h :
  Eq (α := Set (ι → ℚ))
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
    (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))
h₁ :
  ∀ (x : ι → ℚ),
    Membership.mem (γ := Set (ι → ℚ))
        (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
        x ↔
      Membership.mem (γ := Set (ι → ℚ)) (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ)) x
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have h₂ : ∀ (x : ι → ℚ),
  (∃ (a : ι), (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) a : ι → ℕ) = x) ↔
    ∃ (y : ι), (Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) y = x
Tactic: classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst : Finite ι
rw :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        ⋯.extend (s := hs.periods (s := s)) (t :=
          hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)) ⋯))
    ⊤
rw₁ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
rw₂ rw₃ rw₄ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) ''
        (hs.periods (s := s) ∪ range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₅ :
  LE.le (α := Submodule ℚ (ι → ℚ)) ⊤
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
rw₆ :
  Eq (α := Submodule ℚ (ι → ℚ))
    (span ℚ
      (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ))))
    ⊤
h :
  Eq (α := Set (ι → ℚ))
    (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
    (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ))
h₁ :
  ∀ (x : ι → ℚ),
    Membership.mem (γ := Set (ι → ℚ))
        (image (α := ι → ℕ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) (range (ι := ι) (⇑(Pi.basisFun ℕ ι) : (a : ι) → ι → ℕ)))
        x ↔
      Membership.mem (γ := Set (ι → ℚ)) (range (ι := ι) (⇑(Pi.basisFun ℚ ι) : (a : ι) → ι → ℚ)) x
h₂ :
  ∀ (x : ι → ℚ),
    (∃ (a : ι), (toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) a : ι → ℕ) = x) ↔
      ∃ (y : ι), (Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) y = x
⊢ Eq (α := Submodule ℚ (ι → ℚ)) (span ℚ ((⇑toRatVec : (a : ι → ℕ) → ι → ℚ) '' hs.basisSet (s := s))) ⊤
have h₃ : ∀ (x : ι → ℚ) (x : ι),
  Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) ((Pi.basisFun ℕ ι : (a : ι) → ι → ℕ) x : ι → ℕ) : ι → ℚ)
    ((Pi.basisFun ℚ ι : (a : ι) → ι → ℚ) x : ι → ℚ)
Tactic: classical
  rw [basisSet, (linearIndepOn_toRatVec hs.linearIndepOn_periods).span_image_extend_eq_span_image,
    ← top_le_iff]
  apply (span_mono (image_mono subset_union_right)).trans'
  rw [top_le_iff]
  convert! (Pi.basisFun ℚ ι).span_eq
  ext
  simp only [mem_image, mem_range, exists_exists_eq_and]
  congr!
  ext
  simp [toRatVec, Pi.basisFun_apply, Pi.single_apply]