awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
P : (s : Set M) → AddSubmonoid M
t : (s : Set M) → Set ↥(P s)
hP : ∀ (s : Set M) (hs : s ∈ S), (P s).FG
ht : ∀ (s : Set M) (hs : s ∈ S), IsLinearSet (t s)
ht' : ∀ (s : Set M) (hs : s ∈ S), s = Subtype.val (p := fun (x : M) ↦ x ∈ P s) '' t s
this : Finite.{u_1 + 1} (↑S : Type u_1)
simp_rw :
  Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
    (Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
      (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
      (⋃ (s : (↑S : Type u_1)),
        Set.image (α := ↥(P (↑s : Set M)))
          (⇑(AddSubmonoid.inclusion ⋯ : ↥(P (↑s : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
            (a : ↥(P (↑s : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
          (t (↑s : Set M))))
⊢ ⋃₀ S =
    Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
      (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
      (⋃ (s : (↑S : Type u_1)),
        Set.image (α := ↥(P (↑s : Set M)))
          (⇑(AddSubmonoid.inclusion ⋯ : ↥(P (↑s : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
            (a : ↥(P (↑s : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
          (t (↑s : Set M)))
have simp_rw₁ : Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
  (⋃ (i : (↑S : Type u_1)),
    Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
      (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
      (Set.image (α := ↥(P (↑i : Set M)))
        (⇑(AddSubmonoid.inclusion sorry : ↥(P (↑i : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
          (a : ↥(P (↑i : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
        (t (↑i : Set M))))
Tactic: simp_rw [sUnion_eq_iUnion, image_iUnion, image_image, AddSubmonoid.coe_inclusion,
    fun s : S => ht' s s.2]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
P : (s : Set M) → AddSubmonoid M
t : (s : Set M) → Set ↥(P s)
hP : ∀ (s : Set M) (hs : s ∈ S), (P s).FG
ht : ∀ (s : Set M) (hs : s ∈ S), IsLinearSet (t s)
ht' : ∀ (s : Set M) (hs : s ∈ S), s = Subtype.val (p := fun (x : M) ↦ x ∈ P s) '' t s
this : Finite.{u_1 + 1} (↑S : Type u_1)
simp_rw :
  Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
    (Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
      (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
      (⋃ (s : (↑S : Type u_1)),
        Set.image (α := ↥(P (↑s : Set M)))
          (⇑(AddSubmonoid.inclusion ⋯ : ↥(P (↑s : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
            (a : ↥(P (↑s : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
          (t (↑s : Set M))))
simp_rw₁ :
  Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
    (⋃ (i : (↑S : Type u_1)),
      Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
        (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
        (Set.image (α := ↥(P (↑i : Set M)))
          (⇑(AddSubmonoid.inclusion ⋯ : ↥(P (↑i : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
            (a : ↥(P (↑i : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
          (t (↑i : Set M))))
⊢ ⋃₀ S =
    Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
      (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
      (⋃ (s : (↑S : Type u_1)),
        Set.image (α := ↥(P (↑s : Set M)))
          (⇑(AddSubmonoid.inclusion ⋯ : ↥(P (↑s : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
            (a : ↥(P (↑s : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
          (t (↑s : Set M)))
have simp_rw₂ : Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
  (⋃ (i : (↑S : Type u_1)),
    (fun (x : ↥(P (↑i : Set M))) ↦
        (↑(((AddSubmonoid.inclusion sorry : ↥(P (↑i : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
                (a : ↥(P (↑i : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
              x) :
          M)) ''
      t (↑i : Set M))
Tactic: simp_rw [sUnion_eq_iUnion, image_iUnion, image_image, AddSubmonoid.coe_inclusion,
    fun s : S => ht' s s.2]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
P : (s : Set M) → AddSubmonoid M
t : (s : Set M) → Set ↥(P s)
hP : ∀ (s : Set M) (hs : s ∈ S), (P s).FG
ht : ∀ (s : Set M) (hs : s ∈ S), IsLinearSet (t s)
ht' : ∀ (s : Set M) (hs : s ∈ S), s = Subtype.val (p := fun (x : M) ↦ x ∈ P s) '' t s
this : Finite.{u_1 + 1} (↑S : Type u_1)
simp_rw :
  Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
    (Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
      (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
      (⋃ (s : (↑S : Type u_1)),
        Set.image (α := ↥(P (↑s : Set M)))
          (⇑(AddSubmonoid.inclusion ⋯ : ↥(P (↑s : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
            (a : ↥(P (↑s : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
          (t (↑s : Set M))))
simp_rw₁ :
  Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
    (⋃ (i : (↑S : Type u_1)),
      Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
        (Subtype.val (p := fun (x : M) ↦
          Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
        (Set.image (α := ↥(P (↑i : Set M)))
          (⇑(AddSubmonoid.inclusion ⋯ : ↥(P (↑i : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
            (a : ↥(P (↑i : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
          (t (↑i : Set M))))
simp_rw₂ :
  Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
    (⋃ (i : (↑S : Type u_1)),
      (fun (x : ↥(P (↑i : Set M))) ↦
          (↑(((AddSubmonoid.inclusion ⋯ : ↥(P (↑i : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
                  (a : ↥(P (↑i : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
                x) :
            M)) ''
        t (↑i : Set M))
⊢ ⋃₀ S =
    Set.image (α := ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
      (Subtype.val (p := fun (x : M) ↦
        Membership.mem (γ := AddSubmonoid M) (⨆ (s : (↑S : Type u_1)), P (↑s : Set M)) x))
      (⋃ (s : (↑S : Type u_1)),
        Set.image (α := ↥(P (↑s : Set M)))
          (⇑(AddSubmonoid.inclusion ⋯ : ↥(P (↑s : Set M)) →+ ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M))) :
            (a : ↥(P (↑s : Set M))) → ↥(⨆ (s : (↑S : Type u_1)), P (↑s : Set M)))
          (t (↑s : Set M)))
have simp_rw₃ : Eq.{u_1 + 1} (α := Set M) (⋃ (i : (↑S : Type u_1)), (↑i : Set M))
  (⋃ (i : (↑S : Type u_1)), (fun (a : ↥(P (↑i : Set M))) ↦ (↑a : M)) '' t (↑i : Set M))
Tactic: simp_rw [sUnion_eq_iUnion, image_iUnion, image_image, AddSubmonoid.coe_inclusion,
    fun s : S => ht' s s.2]
-- 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₂
⊢ ∃ (P : AddSubmonoid M) (s₁' : Set ↥P) (s₂' : Set ↥P),
    P.FG ∧
      IsSemilinearSet s₁' ∧
        s₁ = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁' ∧
          IsSemilinearSet s₂' ∧ s₂ = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂'
have rcases : ∀ (P₁ : AddSubmonoid M) (s₁' : Set ↥P₁) (hP₁ : P₁.FG) (hs₁' : IsSemilinearSet s₁')
  (hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁')),
  ∃ (P : AddSubmonoid M) (s₁'_1 : Set ↥P) (s₂' : Set ↥P),
    P.FG ∧
      IsSemilinearSet s₁'_1 ∧
        Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁' = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁'_1 ∧
          IsSemilinearSet s₂' ∧ s₂ = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂'
Tactic: rcases hs₁.exists_fg_eq_subtypeVal with ⟨P₁, s₁', hP₁, hs₁', rfl⟩
Cleared hypotheses: s₁, hs₁
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
s₂ : Set M
hs₂ : IsSemilinearSet s₂
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁')
⊢ ∃ (P : AddSubmonoid M) (s₁'_1 : Set ↥P) (s₂' : Set ↥P),
    P.FG ∧
      IsSemilinearSet s₁'_1 ∧
        Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁' = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁'_1 ∧
          IsSemilinearSet s₂' ∧ s₂ = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂'
have rcases : ∀ (P₂ : AddSubmonoid M) (s₂' : Set ↥P₂) (hP₂ : P₂.FG) (hs₂' : IsSemilinearSet s₂')
  (hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂')),
  ∃ (P : AddSubmonoid M) (s₁'_1 : Set ↥P) (s₂'_1 : Set ↥P),
    P.FG ∧
      IsSemilinearSet s₁'_1 ∧
        Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁' = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁'_1 ∧
          IsSemilinearSet s₂'_1 ∧
            Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂' = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂'_1
Tactic: rcases hs₂.exists_fg_eq_subtypeVal with ⟨P₂, s₂', hP₂, hs₂', rfl⟩
Cleared hypotheses: s₂, 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₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂')
⊢ ∃ (P : AddSubmonoid M) (s₁'_1 : Set ↥P) (s₂'_1 : Set ↥P),
    P.FG ∧
      IsSemilinearSet s₁'_1 ∧
        Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁' = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁'_1 ∧
          IsSemilinearSet s₂'_1 ∧
            Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂' = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂'_1
have refine_1 : Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁' =
  Set.image (α := ↥(P₁ ⊔ P₂)) (Subtype.val (p := fun (x : M) ↦ x ∈ P₁ ⊔ P₂))
    ((⇑(AddSubmonoid.inclusion sorry) : (a : ↥P₁) → ↥(P₁ ⊔ P₂)) '' s₁')
Tactic: refine ⟨P₁ ⊔ P₂, (AddSubmonoid.inclusion le_sup_left) '' s₁',
    (AddSubmonoid.inclusion le_sup_right) '' s₂', hP₁.sup hP₂, hs₁'.image _, ?_, hs₂'.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₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂')
refine_1 :
  Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁' =
    Set.image (α := ↥(P₁ ⊔ P₂)) (Subtype.val (p := fun (x : M) ↦ x ∈ P₁ ⊔ P₂))
      ((⇑(AddSubmonoid.inclusion ⋯) : (a : ↥P₁) → ↥(P₁ ⊔ P₂)) '' s₁')
⊢ ∃ (P : AddSubmonoid M) (s₁'_1 : Set ↥P) (s₂'_1 : Set ↥P),
    P.FG ∧
      IsSemilinearSet s₁'_1 ∧
        Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁' = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁'_1 ∧
          IsSemilinearSet s₂'_1 ∧
            Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂' = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂'_1
have refine_2 : Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂' =
  Set.image (α := ↥(P₁ ⊔ P₂)) (Subtype.val (p := fun (x : M) ↦ x ∈ P₁ ⊔ P₂))
    ((⇑(AddSubmonoid.inclusion sorry) : (a : ↥P₂) → ↥(P₁ ⊔ P₂)) '' s₂')
Tactic: refine ⟨P₁ ⊔ P₂, (AddSubmonoid.inclusion le_sup_left) '' s₁',
    (AddSubmonoid.inclusion le_sup_right) '' s₂', hP₁.sup hP₂, hs₁'.image _, ?_, hs₂'.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₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂')
⊢ Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁' =
    Set.image (α := ↥(P₁ ⊔ P₂)) (Subtype.val (p := fun (x : M) ↦ x ∈ P₁ ⊔ P₂))
      ((⇑(AddSubmonoid.inclusion ⋯) : (a : ↥P₁) → ↥(P₁ ⊔ P₂)) '' s₁')
have refine_1 : Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁' =
  (fun (x : ↥P₁) ↦ (↑((AddSubmonoid.inclusion sorry : (a : ↥P₁) → ↥(P₁ ⊔ P₂)) x) : M)) '' s₁'
Tactic: simp_rw [image_image, AddSubmonoid.coe_inclusion]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₁) '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂')
⊢ Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂' =
    Set.image (α := ↥(P₁ ⊔ P₂)) (Subtype.val (p := fun (x : M) ↦ x ∈ P₁ ⊔ P₂))
      ((⇑(AddSubmonoid.inclusion ⋯) : (a : ↥P₂) → ↥(P₁ ⊔ P₂)) '' s₂')
have refine_2 : Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂' =
  (fun (x : ↥P₂) ↦ (↑((AddSubmonoid.inclusion sorry : (a : ↥P₂) → ↥(P₁ ⊔ P₂)) x) : M)) '' s₂'
Tactic: simp_rw [image_image, AddSubmonoid.coe_inclusion]
-- 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₂
⊢ IsSemilinearSet (s₁ ∩ s₂)
have haveI : ∀ (this : Fintype ι), IsSemilinearSet (s₁ ∩ s₂)
Tactic: haveI := Fintype.ofFinite ι
-- 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₂
this : Fintype ι
⊢ IsSemilinearSet (s₁ ∩ s₂)
have rw : ∀ (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₂)
Tactic: rw [isLinearSet_iff_exists_matrix] at hs₁ hs₂
Cleared hypotheses: hs₁, hs₂, this
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
s₁ s₂ : Set (ι → ℕ)
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₂)
have rcases : ∀ (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ),
  IsSemilinearSet ({x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), u + A *ᵥ x_1 = x} ∩ s₂)
Tactic: rcases hs₁ with ⟨u, n, A, 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₂ : ∃ (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₂)
have rcases : ∀ (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})
Tactic: rcases hs₂ with ⟨v, m, B, rfl⟩
Cleared hypotheses: s₂, hs₂
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
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})
have simp_rw : IsSemilinearSet.{u_3} (M := ι → ℕ) {a : ι → ℕ | ∃ (a_1 : Fin n → ℕ) (b : Fin m → ℕ), u + A *ᵥ a_1 = a ∧ v + B *ᵥ b = a}
Tactic: simp_rw [← setOf_and, exists_and_exists_comm]
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
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}
have refine : 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: refine IsSemilinearSet.proj' (IsSemilinearSet.proj' ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic (goal)
Goal:
ι : Type u_3
inst : Finite ι
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}
have h : ∀ (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: 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)
-- 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₂
⊢ IsSemilinearSet (s₁ ∩ s₂)
have haveI : ∀ (this : Fintype ι), IsSemilinearSet (s₁ ∩ s₂)
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]
-- 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₂)
⊢ IsSemilinearSet (s₁ ∩ s₂)
have 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₂)
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: 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₂)
⊢ IsSemilinearSet (s₁ ∩ s₂)
have 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₂)
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₁, 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₂)
⊢ IsSemilinearSet (s₁ ∩ s₂)
have 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})
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₂