awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), IsSemilinearSet (s₁ ∩ s₂)
haveI₃ :
  ∀ (hs₁ : ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s₁ = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x})
    (hs₂ : ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s₂ = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x})
    (this : Fintype ι), IsSemilinearSet (s₁ ∩ s₂)
haveI₄ :
  ∀ (hs₂ : ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s₂ = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x})
    (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ),
    IsSemilinearSet ({x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), u + A *ᵥ x_1 = x} ∩ s₂)
haveI₅ :
  ∀ (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ) (v : ι → ℕ) (m : ℕ) (B : Matrix ι (Fin m) ℕ),
    IsSemilinearSet.{u_3} (M := ι → ℕ)
      ({x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), u + A *ᵥ x_1 = x} ∩ {x : ι → ℕ | ∃ (x_1 : Fin m → ℕ), v + B *ᵥ x_1 = x})
⊢ IsSemilinearSet (s₁ ∩ s₂)
have haveI₆ : ∀ (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ) (v : ι → ℕ) (m : ℕ) (B : Matrix ι (Fin m) ℕ),
  IsSemilinearSet.{u_3} (M := ι → ℕ)
    {a : ι → ℕ | ∃ (a_1 : Fin n → ℕ) (b : Fin m → ℕ), u + A *ᵥ a_1 = a ∧ v + B *ᵥ b = a}
Tactic: classical
  haveI := Fintype.ofFinite ι
  rw [isLinearSet_iff_exists_matrix] at hs₁ hs₂
  rcases hs₁ with ⟨u, n, A, rfl⟩
  rcases hs₂ with ⟨v, m, B, rfl⟩
  simp_rw [← setOf_and, exists_and_exists_comm]
  refine IsSemilinearSet.proj' (IsSemilinearSet.proj' ?_)
  convert!
    isSemilinearSet_setOf_mulVec_eq (κ := (ι ⊕ Fin n) ⊕ Fin m) (Sum.elim u v) 0
      (fromBlocks (fromCols 0 A) 0 0 B) (fromBlocks (fromCols 1 0) 0 (fromCols 1 0) 0)
  simp [fromBlocks_mulVec, fromCols_mulVec, ← Sum.elim_add_add, Sum.elim_eq_iff]
Cleared hypotheses: s₁, s₂, hs₁, hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), IsSemilinearSet (s₁ ∩ s₂)
haveI₃ :
  ∀ (hs₁ : ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s₁ = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x})
    (hs₂ : ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s₂ = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x})
    (this : Fintype ι), IsSemilinearSet (s₁ ∩ s₂)
haveI₄ :
  ∀ (hs₂ : ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s₂ = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x})
    (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ),
    IsSemilinearSet ({x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), u + A *ᵥ x_1 = x} ∩ s₂)
haveI₅ :
  ∀ (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ) (v : ι → ℕ) (m : ℕ) (B : Matrix ι (Fin m) ℕ),
    IsSemilinearSet.{u_3} (M := ι → ℕ)
      ({x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), u + A *ᵥ x_1 = x} ∩ {x : ι → ℕ | ∃ (x_1 : Fin m → ℕ), v + B *ᵥ x_1 = x})
haveI₆ :
  ∀ (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ) (v : ι → ℕ) (m : ℕ) (B : Matrix ι (Fin m) ℕ),
    IsSemilinearSet.{u_3} (M := ι → ℕ)
      {a : ι → ℕ | ∃ (a_1 : Fin n → ℕ) (b : Fin m → ℕ), u + A *ᵥ a_1 = a ∧ v + B *ᵥ b = a}
⊢ IsSemilinearSet (s₁ ∩ s₂)
have haveI₇ : ∀ (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ) (v : ι → ℕ) (m : ℕ) (B : Matrix ι (Fin m) ℕ),
  IsSemilinearSet.{u_3} (M := (ι ⊕ Fin n) ⊕ Fin m → ℕ)
    {x : (ι ⊕ Fin n) ⊕ Fin m → ℕ |
      u + A *ᵥ (x ∘ Sum.inl) ∘ Sum.inr = (x ∘ Sum.inl) ∘ Sum.inl ∧ v + B *ᵥ x ∘ Sum.inr = (x ∘ Sum.inl) ∘ Sum.inl}
Tactic: classical
  haveI := Fintype.ofFinite ι
  rw [isLinearSet_iff_exists_matrix] at hs₁ hs₂
  rcases hs₁ with ⟨u, n, A, rfl⟩
  rcases hs₂ with ⟨v, m, B, rfl⟩
  simp_rw [← setOf_and, exists_and_exists_comm]
  refine IsSemilinearSet.proj' (IsSemilinearSet.proj' ?_)
  convert!
    isSemilinearSet_setOf_mulVec_eq (κ := (ι ⊕ Fin n) ⊕ Fin m) (Sum.elim u v) 0
      (fromBlocks (fromCols 0 A) 0 0 B) (fromBlocks (fromCols 1 0) 0 (fromCols 1 0) 0)
  simp [fromBlocks_mulVec, fromCols_mulVec, ← Sum.elim_add_add, Sum.elim_eq_iff]
Cleared hypotheses: s₁, s₂, hs₁, hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
haveI haveI₁ haveI₂ : ∀ (this : Fintype ι), IsSemilinearSet (s₁ ∩ s₂)
haveI₃ :
  ∀ (hs₁ : ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s₁ = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x})
    (hs₂ : ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s₂ = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x})
    (this : Fintype ι), IsSemilinearSet (s₁ ∩ s₂)
haveI₄ :
  ∀ (hs₂ : ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s₂ = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x})
    (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ),
    IsSemilinearSet ({x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), u + A *ᵥ x_1 = x} ∩ s₂)
haveI₅ :
  ∀ (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ) (v : ι → ℕ) (m : ℕ) (B : Matrix ι (Fin m) ℕ),
    IsSemilinearSet.{u_3} (M := ι → ℕ)
      ({x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), u + A *ᵥ x_1 = x} ∩ {x : ι → ℕ | ∃ (x_1 : Fin m → ℕ), v + B *ᵥ x_1 = x})
haveI₆ :
  ∀ (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ) (v : ι → ℕ) (m : ℕ) (B : Matrix ι (Fin m) ℕ),
    IsSemilinearSet.{u_3} (M := ι → ℕ)
      {a : ι → ℕ | ∃ (a_1 : Fin n → ℕ) (b : Fin m → ℕ), u + A *ᵥ a_1 = a ∧ v + B *ᵥ b = a}
haveI₇ :
  ∀ (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ) (v : ι → ℕ) (m : ℕ) (B : Matrix ι (Fin m) ℕ),
    IsSemilinearSet.{u_3} (M := (ι ⊕ Fin n) ⊕ Fin m → ℕ)
      {x : (ι ⊕ Fin n) ⊕ Fin m → ℕ |
        u + A *ᵥ (x ∘ Sum.inl) ∘ Sum.inr = (x ∘ Sum.inl) ∘ Sum.inl ∧ v + B *ᵥ x ∘ Sum.inr = (x ∘ Sum.inl) ∘ Sum.inl}
⊢ IsSemilinearSet (s₁ ∩ s₂)
have h : ∀ (this : Fintype ι) (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ) (v : ι → ℕ) (m : ℕ) (B : Matrix ι (Fin m) ℕ)
  (x : (ι ⊕ Fin n) ⊕ Fin m → ℕ),
  u + A *ᵥ (x ∘ Sum.inl) ∘ Sum.inr = (x ∘ Sum.inl) ∘ Sum.inl ∧ v + B *ᵥ x ∘ Sum.inr = (x ∘ Sum.inl) ∘ Sum.inl ↔
    Sum.elim u v + fromBlocks (fromCols 0 A) 0 0 B *ᵥ x =
      HAdd.hAdd (α := ι ⊕ ι → ℕ) 0 (fromBlocks (fromCols 1 0) 0 (fromCols 1 0) 0 *ᵥ x)
Tactic: classical
  haveI := Fintype.ofFinite ι
  rw [isLinearSet_iff_exists_matrix] at hs₁ hs₂
  rcases hs₁ with ⟨u, n, A, rfl⟩
  rcases hs₂ with ⟨v, m, B, rfl⟩
  simp_rw [← setOf_and, exists_and_exists_comm]
  refine IsSemilinearSet.proj' (IsSemilinearSet.proj' ?_)
  convert!
    isSemilinearSet_setOf_mulVec_eq (κ := (ι ⊕ Fin n) ⊕ Fin m) (Sum.elim u v) 0
      (fromBlocks (fromCols 0 A) 0 0 B) (fromBlocks (fromCols 1 0) 0 (fromCols 1 0) 0)
  simp [fromBlocks_mulVec, fromCols_mulVec, ← Sum.elim_add_add, Sum.elim_eq_iff]
Cleared hypotheses: s₁, s₂, hs₁, hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
⊢ IsSemilinearSet (s₁ ∩ s₂)
have rcases : ∀ (S₁ : Set (Set (ι → ℕ))) (hS₁ : S₁.Finite) (hS₁' : ∀ t ∈ S₁, IsLinearSet t), IsSemilinearSet (⋃₀ S₁ ∩ s₂)
Tactic: rcases hs₁ with ⟨S₁, hS₁, hS₁', rfl⟩
Cleared hypotheses: s₁, hs₁
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s₂ : Set (ι → ℕ)
hs₂ : IsSemilinearSet s₂
S₁ : Set (Set (ι → ℕ))
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ S₁ ∩ s₂)
have rcases : ∀ (S₂ : Set (Set (ι → ℕ))) (hS₂ : S₂.Finite) (hS₂' : ∀ t ∈ S₂, IsLinearSet t), IsSemilinearSet (⋃₀ S₁ ∩ ⋃₀ S₂)
Tactic: rcases hs₂ with ⟨S₂, hS₂, hS₂', rfl⟩
Cleared hypotheses: s₂, hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
S₁ : Set (Set (ι → ℕ))
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set (ι → ℕ))
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ S₁ ∩ ⋃₀ S₂)
have rw : IsSemilinearSet.{u_3} (M := ι → ℕ) (⋃ p ∈ S₁ ×ˢ S₂, p.1 ∩ p.2)
Tactic: rw [sUnion_inter_sUnion]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
⊢ IsSemilinearSet (s₁ ∩ s₂)
have rcases : ∀ (P : AddSubmonoid M) (s₁' s₂' : Set ↥P) (hP : P.FG) (hs₁' : IsSemilinearSet s₁')
  (hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')) (hs₂' : IsSemilinearSet s₂')
  (hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')),
  IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁' ∩ Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
Tactic: rcases hs₁.exists_fg_eq_subtypeVal₂ hs₂ with ⟨P, s₁', s₂', hP, hs₁', rfl, hs₂', rfl⟩
Cleared hypotheses: s₁, s₂, hs₁, hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁' ∩ Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
have rw : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' (s₁' ∩ s₂'))
Tactic: rw [← image_inter Subtype.val_injective]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' (s₁' ∩ s₂'))
have apply : IsSemilinearSet (s₁' ∩ s₂')
Tactic: apply image (f := P.subtype)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : P.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
⊢ IsSemilinearSet (s₁' ∩ s₂')
have hP₁ : ∃ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P), Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤
Tactic: rw [← AddMonoid.fg_iff_addSubmonoid_fg, AddMonoid.fg_def, fg_iff_exists_fin_addMonoidHom] at hP
Cleared hypotheses: hP, hs₁', hs₁, hs₂', hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hP : ∃ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P), Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
⊢ IsSemilinearSet (s₁' ∩ s₂')
have rcases : ∀ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P) (hf : Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤),
  IsSemilinearSet (s₁' ∩ s₂')
Tactic: rcases hP with ⟨n, f, hf⟩
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤
⊢ IsSemilinearSet (s₁' ∩ s₂')
have hf₁ : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
Tactic: rw [AddMonoidHom.mrange_eq_top] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
⊢ IsSemilinearSet (s₁' ∩ s₂')
have rw : IsSemilinearSet (M := ↥P)
  (Set.image (α := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ↥P)
    ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' ∩ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂'))
Tactic: rw [← image_preimage_eq (s₁' ∩ s₂') hf, preimage_inter]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
⊢ IsSemilinearSet (M := ↥P)
    (Set.image (α := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ↥P)
      ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' ∩ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂'))
have hs : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' ∩ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
Tactic: apply image
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
⊢ IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' ∩ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
have hs : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁')
Tactic: apply Nat.isSemilinearSet_inter
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)
hs : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁')
⊢ IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁' ∩ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
have hs₃ : IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
Tactic: apply Nat.isSemilinearSet_inter
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
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 (⋂₀ insert a s)
have hS'₁ : IsSemilinearSet a ∧ ∀ a ∈ s, IsSemilinearSet a
Tactic: simp_rw [mem_insert_iff, forall_eq_or_imp] at hS'
Cleared hypotheses: hS'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ IsSemilinearSet (⋂₀ S)
have empty : ∀ (hS' : ∀ (s : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsSemilinearSet s),
  IsSemilinearSet.{u_1} (M := M) (⋂₀ ∅)
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)
Cleared hypotheses: hS, hS'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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) (⋂₀ ∅)
⊢ IsSemilinearSet (⋂₀ S)
have 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 a s, IsSemilinearSet s_1), IsSemilinearSet (⋂₀ insert a 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)
Cleared hypotheses: hS, hS'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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)
⊢ IsSemilinearSet (⋂₀ range s)
have apply : ∀ s_1 ∈ range s, IsSemilinearSet s_1
Tactic: apply sInter (finite_range s)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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)
⊢ IsSemilinearSet.{u_1} (M := M) (⋂ i ∈ s, t i)
have rw : IsSemilinearSet (⋂₀ (t '' s))
Tactic: rw [← sInter_image]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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)
⊢ IsSemilinearSet (⋂₀ (t '' s))
have apply : ∀ s_1 ∈ t '' s, IsSemilinearSet s_1
Tactic: apply sInter (hs.image t)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
x y : ι → ℕ
⊢ Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) ↔ x = y
have refine : ∀ (h : Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ)), x = y
Tactic: refine ⟨fun h => ?_, congr_arg toRatVec⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
x y : ι → ℕ
h : Eq (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ)
⊢ x = y
have h₁ : ∀ (i : ι), x i = y i
Tactic: ext i
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
x y : ι → ℕ
⊢ LE.le (α := ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y : ι → ℚ) ↔ x ≤ y
have h : ∀ (a : ι),
  LE.le (α := (fun (a : ι) ↦ ℚ) a) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x a) ((toRatVec : (a : ι → ℕ) → ι → ℚ) y a) ↔
    x a ≤ y a
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
x : ι → ℕ
⊢ LE.le (α := ι → ℚ) (0 : ι → ℚ) ((toRatVec : (a : ι → ℕ) → ι → ℚ) x : ι → ℚ)
have rw : 0 ≤ x
Tactic: rw [← map_zero toRatVec, toRatVec_mono]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
⊢ LinearIndepOn ℚ (M := ι → ℚ) (⇑toRatVec : (a : ι → ℕ) → ι → ℚ) s
have 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
Tactic: rw [LinearIndepOn, ← LinearIndependent.iff_fractionRing ℤ ℚ, ← LinearIndepOn, linearIndepOn_iff'']
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
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
⊢ f i = 0
have 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
Tactic: rw [linearIndepOn_iff_linearIndepOn_finset] at hs
Cleared hypotheses: hs, t, f, ht, hf, heq, i, hi
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
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
⊢ f i = 0
have hs₁ : LinearIndepOn ℕ id (↑t : Set (ι → ℕ))
Tactic: specialize hs t ht
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (hypothesis)
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 i = 0
have hs₁ : ∀ (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
Cleared hypotheses: hs
-- 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
⊢ f i = 0
have specialize : Eq (α := ι → ℕ) (∑ i ∈ t, (Int.toNat ∘ f) i • id i) (∑ i ∈ t, (Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) i • id i)
Tactic: specialize hs (Int.toNat ∘ f) (Int.toNat ∘ (-·) ∘ f) ?_ i hi
-- 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
specialize :
  Eq (α := ι → ℕ) (∑ i ∈ t, (Int.toNat ∘ f) i • id i) (∑ i ∈ t, (Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) i • id i)
⊢ f i = 0
have specialize₁ : ∀ (hs : (Int.toNat ∘ f) i = (Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) i), f i = 0
Tactic: specialize hs (Int.toNat ∘ f) (Int.toNat ∘ (-·) ∘ f) ?_ i hi
Cleared hypotheses: hs
-- 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 (α := ι → ℕ) (∑ i ∈ t, (Int.toNat ∘ f) i • id i) (∑ i ∈ t, (Int.toNat ∘ (fun (x : ℤ) ↦ -x) ∘ f) i • id i)
have 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))
Tactic: simp_rw [← toRatVec_inj, map_sum]