awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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_2 :
  Subtype.val (p := fun (x : M) ↦ x ∈ P₂) '' s₂' =
    (fun (x : ↥P₂) ↦ (↑((AddSubmonoid.inclusion ⋯ : (a : ↥P₂) → ↥(P₁ ⊔ P₂)) x) : M)) '' 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₂')

Tactic:
simp_rw [image_image, AddSubmonoid.coe_inclusion]

Premises used: Set.image_image, AddSubmonoid.coe_inclusion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
haveI : ∀ (this : Fintype ι), IsSemilinearSet (s₁ ∩ s₂)
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
haveI := Fintype.ofFinite ι
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsLinearSet s₁
hs₂ : IsLinearSet s₂
this : Fintype ι
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₂)
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
rw [isLinearSet_iff_exists_matrix] at hs₁ hs₂

Premises used: Nat.isLinearSet_iff_exists_matrix
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 ι
rcases :
  ∀ (u : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ),
    IsSemilinearSet ({x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), u + A *ᵥ x_1 = x} ∩ s₂)
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
rcases hs₁ with ⟨u, n, A, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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) ℕ
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})
⊢ IsSemilinearSet ({x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), u + A *ᵥ x_1 = x} ∩ s₂)

Tactic:
rcases hs₂ with ⟨v, m, B, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
simp_rw :
  IsSemilinearSet.{u_3} (M := ι → ℕ)
    {a : ι → ℕ | ∃ (a_1 : Fin n → ℕ) (b : Fin m → ℕ), u + A *ᵥ a_1 = a ∧ v + B *ᵥ b = a}
⊢ 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:
simp_rw [← setOf_and, exists_and_exists_comm]

Premises used: Set.setOf_and, exists_and_exists_comm
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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}

Tactic:
IsSemilinearSet.proj' (IsSemilinearSet.proj' ?_)

Premises used: IsSemilinearSet.proj'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
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}
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    {a : ι → ℕ | ∃ (a_1 : Fin n → ℕ) (b : Fin m → ℕ), u + A *ᵥ a_1 = a ∧ v + B *ᵥ b = a}

Tactic:
refine IsSemilinearSet.proj' (IsSemilinearSet.proj' ?_)

Premises used: IsSemilinearSet.proj'
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 → ℕ |
      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:
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)

Premises used: Matrix.fromBlocks, Matrix.fromCols, Nat.isSemilinearSet_setOf_mulVec_eq, OfNat.ofNat, Sum.elim
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
this : Fintype ι
u : ι → ℕ
n : ℕ
A : Matrix ι (Fin n) ℕ
v : ι → ℕ
m : ℕ
B : Matrix ι (Fin m) ℕ
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)
⊢ 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:
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)

Premises used: Matrix.fromBlocks, Matrix.fromCols, Nat.isSemilinearSet_setOf_mulVec_eq, OfNat.ofNat, Sum.elim
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
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:
simp [fromBlocks_mulVec, fromCols_mulVec, ← Sum.elim_add_add, Sum.elim_eq_iff]

Premises used: Sum.elim_eq_iff, Matrix.fromBlocks_mulVec, Sum.elim_add_add, Matrix.fromCols_mulVec
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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}
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)
⊢ 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]

Premises used: Nat.isLinearSet_iff_exists_matrix, Set.setOf_and, exists_and_exists_comm, Sum.elim_eq_iff, Matrix.fromBlocks_mulVec, Sum.elim_add_add, IsSemilinearSet.proj', Matrix.fromCols_mulVec, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s₁ s₂ : Set (ι → ℕ)
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
rcases : ∀ (S₁ : Set (Set (ι → ℕ))) (hS₁ : S₁.Finite) (hS₁' : ∀ t ∈ S₁, IsLinearSet t), IsSemilinearSet (⋃₀ S₁ ∩ s₂)
⊢ IsSemilinearSet (s₁ ∩ s₂)

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

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
inst : Finite ι
s₂ : Set (ι → ℕ)
hs₂ : IsSemilinearSet s₂
S₁ : Set (Set (ι → ℕ))
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
rcases : ∀ (S₂ : Set (Set (ι → ℕ))) (hS₂ : S₂.Finite) (hS₂' : ∀ t ∈ S₂, IsLinearSet t), IsSemilinearSet (⋃₀ S₁ ∩ ⋃₀ S₂)
⊢ IsSemilinearSet (⋃₀ S₁ ∩ s₂)

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

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
rw : IsSemilinearSet.{u_3} (M := ι → ℕ) (⋃ p ∈ S₁ ×ˢ S₂, p.1 ∩ p.2)
⊢ IsSemilinearSet (⋃₀ S₁ ∩ ⋃₀ S₂)

Tactic:
rw [sUnion_inter_sUnion]

Premises used: Set.sUnion_inter_sUnion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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.{u_3} (M := ι → ℕ) (⋃ p ∈ S₁ ×ˢ S₂, p.1 ∩ p.2)

Tactic:
.biUnion (hS₁.prod hS₂) fun s hs =>
    isSemilinearSet_inter_of_isLinearSet (hS₁' _ hs.1) (hS₂' _ hs.2)

Premises used: IsSemilinearSet.biUnion, Prod.fst, And.right, Set.Finite.prod, And.left, Prod.snd, _private.0.Nat.isSemilinearSet_inter_of_isLinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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.{u_3} (M := ι → ℕ) (⋃ p ∈ S₁ ×ˢ S₂, p.1 ∩ p.2)

Tactic:
exact .biUnion (hS₁.prod hS₂) fun s hs =>
    isSemilinearSet_inter_of_isLinearSet (hS₁' _ hs.1) (hS₂' _ hs.2)
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
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₂')
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
rcases hs₁.exists_fg_eq_subtypeVal₂ hs₂ with ⟨P, s₁', s₂', hP, hs₁', rfl, hs₂', rfl⟩

Premises used: IsSemilinearSet.exists_fg_eq_subtypeVal₂, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₂')
rw : IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' (s₁' ∩ s₂'))
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁' ∩ Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')

Tactic:
rw [← image_inter Subtype.val_injective]

Premises used: Subtype.val_injective, Set.image_inter
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₂')
apply : IsSemilinearSet (s₁' ∩ s₂')
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' (s₁' ∩ s₂'))

Tactic:
apply image (f := P.subtype)

Premises used: AddSubmonoid.subtype, IsSemilinearSet.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₂')
⊢ ∃ (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

Premises used: AddSubmonoid.fg_iff_exists_fin_addMonoidHom, AddMonoid.fg_def, AddMonoid.fg_iff_addSubmonoid_fg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₂')
hP₁ : ∃ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P), Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤
⊢ IsSemilinearSet s₁'

Tactic:
rw [← AddMonoid.fg_iff_addSubmonoid_fg, AddMonoid.fg_def, fg_iff_exists_fin_addMonoidHom] at hP

Premises used: AddSubmonoid.fg_iff_exists_fin_addMonoidHom, AddMonoid.fg_def, AddMonoid.fg_iff_addSubmonoid_fg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₂')
hP₁ : ∃ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P), Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤
hs₁'₁ : IsSemilinearSet s₁'
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₁')

Tactic:
rw [← AddMonoid.fg_iff_addSubmonoid_fg, AddMonoid.fg_def, fg_iff_exists_fin_addMonoidHom] at hP

Premises used: AddSubmonoid.fg_iff_exists_fin_addMonoidHom, AddMonoid.fg_def, AddMonoid.fg_iff_addSubmonoid_fg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₂')
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₁')
⊢ IsSemilinearSet s₂'

Tactic:
rw [← AddMonoid.fg_iff_addSubmonoid_fg, AddMonoid.fg_def, fg_iff_exists_fin_addMonoidHom] at hP

Premises used: AddSubmonoid.fg_iff_exists_fin_addMonoidHom, AddMonoid.fg_def, AddMonoid.fg_iff_addSubmonoid_fg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₂')
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₂'
⊢ IsSemilinearSet (Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s₂')

Tactic:
rw [← AddMonoid.fg_iff_addSubmonoid_fg, AddMonoid.fg_def, fg_iff_exists_fin_addMonoidHom] at hP

Premises used: AddSubmonoid.fg_iff_exists_fin_addMonoidHom, AddMonoid.fg_def, AddMonoid.fg_iff_addSubmonoid_fg
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₂')
rcases :
  ∀ (n : ℕ) (f : (Fin n → ℕ) →+ ↥P) (hf : Eq (α := AddSubmonoid ↥P) (AddMonoidHom.mrange f) ⊤),
    IsSemilinearSet (s₁' ∩ s₂')
⊢ IsSemilinearSet (s₁' ∩ s₂')

Tactic:
rcases hP with ⟨n, f, hf⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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) ⊤
⊢ Function.Surjective (α := Fin n → ℕ) (β := ↥P) (⇑f : (a : Fin n → ℕ) → ↥P)

Tactic:
rw [AddMonoidHom.mrange_eq_top] at hf

Premises used: AddMonoidHom.mrange_eq_top
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)
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₂'))
⊢ IsSemilinearSet (s₁' ∩ s₂')

Tactic:
rw [← image_preimage_eq (s₁' ∩ s₂') hf, preimage_inter]

Premises used: Set.preimage_inter, Set.image_preimage_eq, Inter.inter
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₁' ∩ (⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')
⊢ 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:
apply image

Premises used: IsSemilinearSet.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₁')
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₂')

Tactic:
apply Nat.isSemilinearSet_inter

Premises used: _private.0.Nat.isSemilinearSet_inter
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 s₁'
⊢ IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₁')

Tactic:
apply Nat.isSemilinearSet_preimage

Premises used: _private.0.Nat.isSemilinearSet_preimage
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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 s₂'
⊢ IsSemilinearSet (M := Fin n → ℕ) ((⇑f : (a : Fin n → ℕ) → ↥P) ⁻¹' s₂')

Tactic:
apply Nat.isSemilinearSet_preimage

Premises used: _private.0.Nat.isSemilinearSet_preimage
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₁'

Tactic:
assumption
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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₂'

Tactic:
assumption
-- 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 : Set M), Membership.mem (γ := Set (Set M)) ∅ s → IsSemilinearSet s
⊢ IsSemilinearSet.{u_1} (M := M) (⋂₀ ∅)

Tactic:
simp