awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
s : ι → Set M
hs : ∀ (i : ι), IsSemilinearSet (s i)
apply : ∀ s_1 ∈ range s, IsSemilinearSet s_1
⊢ IsSemilinearSet (⋃₀ range s)

Tactic:
apply sUnion (finite_range s)

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

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

Tactic:
rw [← sUnion_image]

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

Tactic:
apply sUnion (hs.image t)

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

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

Tactic:
biUnion s.finite_toSet ht

Premises used: IsSemilinearSet.biUnion, Finset.finite_toSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : s.Finite
rw : IsSemilinearSet.{u_1} (M := M) (⋃ x ∈ s, {x})
⊢ IsSemilinearSet s

Tactic:
rw [← biUnion_of_singleton s]

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : s.Finite
apply : ∀ i ∈ s, IsSemilinearSet (M := M) {i}
⊢ IsSemilinearSet.{u_1} (M := M) (⋃ x ∈ s, {x})

Tactic:
apply biUnion hs

Premises used: IsSemilinearSet.biUnion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : s.Finite
⊢ ∀ i ∈ s, IsSemilinearSet (M := M) {i}

Tactic:
simp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
hs : IsSemilinearSet s
rcases : ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t), IsSemilinearSet (a +ᵥ ⋃₀ S)
⊢ IsSemilinearSet (a +ᵥ s)

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

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
rw : IsSemilinearSet.{u_1} (M := M) (⋃ s ∈ S, a +ᵥ s)
⊢ IsSemilinearSet (a +ᵥ ⋃₀ S)

Tactic:
rw [vadd_set_sUnion]

Premises used: Set.vadd_set_sUnion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet.{u_1} (M := M) (⋃ s ∈ S, a +ᵥ s)

Tactic:
biUnion hS fun s hs => ((hS' s hs).vadd a).isSemilinearSet

Premises used: IsSemilinearSet.biUnion, IsLinearSet.vadd, IsLinearSet.isSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet.{u_1} (M := M) (⋃ s ∈ S, a +ᵥ s)

Tactic:
exact biUnion hS fun s hs => ((hS' s hs).vadd a).isSemilinearSet

Premises used: IsSemilinearSet.biUnion, IsLinearSet.vadd, IsLinearSet.isSemilinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
rcases : ∀ (S₁ : Set (Set M)) (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.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s₂ : Set M
hs₂ : IsSemilinearSet s₂
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
rcases : ∀ (S₂ : Set (Set M)) (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.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
simp_rw : IsSemilinearSet.{u_1} (M := M) (⋃ s ∈ S₁, ⋃ t ∈ S₂, s + t)
⊢ IsSemilinearSet (⋃₀ S₁ + ⋃₀ S₂)

Tactic:
simp_rw [sUnion_add, add_sUnion]

Premises used: Set.add_sUnion, Set.sUnion_add
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet.{u_1} (M := M) (⋃ s ∈ S₁, ⋃ t ∈ S₂, s + t)

Tactic:
biUnion hS₁ fun s₁ hs₁ => biUnion hS₂ fun s₂ hs₂ =>
    ((hS₁' s₁ hs₁).add (hS₂' s₂ hs₂)).isSemilinearSet

Premises used: IsSemilinearSet.biUnion, IsLinearSet.isSemilinearSet, IsLinearSet.add
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet.{u_1} (M := M) (⋃ s ∈ S₁, ⋃ t ∈ S₂, s + t)

Tactic:
exact biUnion hS₁ fun s₁ hs₁ => biUnion hS₂ fun s₂ hs₂ =>
    ((hS₁' s₁ hs₁).add (hS₂' s₂ hs₂)).isSemilinearSet

Premises used: IsSemilinearSet.biUnion, IsLinearSet.isSemilinearSet, IsLinearSet.add
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
s : Set M
hs : IsSemilinearSet s
f : F
rcases :
  ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t),
    IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' ⋃₀ S)
⊢ IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)

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

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
simp_rw : IsSemilinearSet.{u_2} (M := N) (⋃ i ∈ S, (⇑f : (a : M) → N) '' i)
⊢ IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' ⋃₀ S)

Tactic:
simp_rw [sUnion_eq_biUnion, image_iUnion]

Premises used: Set.sUnion_eq_biUnion, Set.image_iUnion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet.{u_2} (M := N) (⋃ i ∈ S, (⇑f : (a : M) → N) '' i)

Tactic:
biUnion hS fun s hs => ((hS' s hs).image f).isSemilinearSet

Premises used: IsSemilinearSet.biUnion, IsLinearSet.isSemilinearSet, IsLinearSet.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
F : Type u_5
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : FunLike F M N
inst_3 : AddMonoidHomClass F M N
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet.{u_2} (M := N) (⋃ i ∈ S, (⇑f : (a : M) → N) '' i)

Tactic:
exact biUnion hS fun s hs => ((hS' s hs).image f).isSemilinearSet

Premises used: IsSemilinearSet.biUnion, IsLinearSet.isSemilinearSet, IsLinearSet.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
s : Set M
F : Type u_6
inst_2 : EquivLike F M N
inst_3 : AddEquivClass F M N
f : F
mp : IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s) → IsSemilinearSet s
mpr : IsSemilinearSet s → IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)
⊢ IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s) ↔ IsSemilinearSet s

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
s : Set M
F : Type u_6
inst_2 : EquivLike F M N
inst_3 : AddEquivClass F M N
f : F
h : IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)
⊢ IsSemilinearSet.{u_1} (M := M)
    (image.{u_2, u_1} (α := N) (⇑(AddEquiv.symm (↑f : M ≃+ N)) : (a : N) → M) ((⇑f : (a : M) → N) '' s))

Tactic:
h.image (f : M ≃+ N).symm

Premises used: IsSemilinearSet.image, AddEquivClass.toAddEquiv, AddEquiv.symm
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
s : Set M
F : Type u_6
inst_2 : EquivLike F M N
inst_3 : AddEquivClass F M N
f : F
h : IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)
h₁ : s = image.{u_2, u_1} (α := N) (⇑(AddEquiv.symm (↑f : M ≃+ N)) : (a : N) → M) ((⇑f : (a : M) → N) '' s)
⊢ IsSemilinearSet s

Tactic:
convert! h.image (f : M ≃+ N).symm

Premises used: IsSemilinearSet.image, AddEquivClass.toAddEquiv, AddEquiv.symm
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
s : Set M
F : Type u_6
inst_2 : EquivLike F M N
inst_3 : AddEquivClass F M N
f : F
h : IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)
⊢ s = image.{u_2, u_1} (α := N) (⇑(AddEquiv.symm (↑f : M ≃+ N)) : (a : N) → M) ((⇑f : (a : M) → N) '' s)

Tactic:
simp [image_image]

Premises used: Set.image_image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
s : Set M
F : Type u_6
inst_2 : EquivLike F M N
inst_3 : AddEquivClass F M N
f : F
h : IsSemilinearSet s
⊢ IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)

Tactic:
h.image f

Premises used: IsSemilinearSet.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
s : Set M
F : Type u_6
inst_2 : EquivLike F M N
inst_3 : AddEquivClass F M N
f : F
h : IsSemilinearSet s
⊢ IsSemilinearSet.{u_2} (M := N) ((⇑f : (a : M) → N) '' s)

Tactic:
exact h.image f

Premises used: IsSemilinearSet.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
⊢ IsSemilinearSet (M := ι → M) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s)

Tactic:
hs.image (LinearMap.funLeft ℕ M Sum.inl)

Premises used: IsSemilinearSet.image, Sum.inl, LinearMap.funLeft, Nat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
h :
  Eq (α := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}
    ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s)
⊢ IsSemilinearSet (M := ι → M) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}

Tactic:
convert! hs.image (LinearMap.funLeft ℕ M Sum.inl)

Premises used: IsSemilinearSet.image, Sum.inl, LinearMap.funLeft, Nat
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
h :
  ∀ (x : ι → M),
    Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x ↔
      Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x
⊢ Eq (α := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}
    ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s)

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
x : ι → M
h :
  Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x →
    Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x
h₁ :
  Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x →
    Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x
⊢ Membership.mem (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s} x ↔
    Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
x : ι → M
y : κ → M
hy : Sum.elim x y ∈ s
⊢ Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x

Tactic:
⟨Sum.elim x y, hy, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl, Sum.elim
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
x : ι → M
y : κ → M
hy : Sum.elim x y ∈ s
⊢ Membership.mem (γ := Set (ι → M)) ((⇑(LinearMap.funLeft ℕ M Sum.inl) : (a : ι ⊕ κ → M) → ι → M) '' s) x

Tactic:
exact ⟨Sum.elim x y, hy, rfl⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
y : ι ⊕ κ → M
hy : y ∈ s
⊢ Membership.mem (α := ι → M) (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}
    ((LinearMap.funLeft ℕ M Sum.inl : (a : ι ⊕ κ → M) → ι → M) y : ι → M)

Tactic:
⟨y ∘ Sum.inr, ?_⟩

Premises used: Set.Mem, setOf, Function.comp, Sum.inr, Exists.intro
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
y : ι ⊕ κ → M
hy : y ∈ s
h : Sum.elim ((LinearMap.funLeft ℕ M Sum.inl : (a : ι ⊕ κ → M) → ι → M) y) (y ∘ Sum.inr) ∈ s
⊢ Membership.mem (α := ι → M) (γ := Set (ι → M)) {x : ι → M | ∃ (y : κ → M), Sum.elim x y ∈ s}
    ((LinearMap.funLeft ℕ M Sum.inl : (a : ι ⊕ κ → M) → ι → M) y : ι → M)

Tactic:
refine ⟨y ∘ Sum.inr, ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
y : ι ⊕ κ → M
hy : y ∈ s
⊢ Sum.elim ((LinearMap.funLeft ℕ M Sum.inl : (a : ι ⊕ κ → M) → ι → M) y) (y ∘ Sum.inr) ∈ s

Tactic:
simpa [LinearMap.funLeft]

Premises used: LinearMap.funLeft
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
ι : Type u_3
κ : Type u_4
inst : AddCommMonoid M
p : (ι → M) → (κ → M) → Prop
⊢ IsSemilinearSet (M := ι ⊕ κ → M) {x : ι ⊕ κ → M | p (x ∘ Sum.inl) (x ∘ Sum.inr)} →
    IsSemilinearSet (M := ι → M) {x : ι → M | ∃ (y : κ → M), p x y}

Tactic:
proj

Premises used: Set.Mem, setOf, IsSemilinearSet.proj, Sum.elim
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : IsLinearSet s
rcases : ∀ (a : M) (t : Set M) (ht : t.Finite), IsSemilinearSet (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M)
⊢ IsSemilinearSet (↑(closure s) : Set M)

Tactic:
rcases hs with ⟨a, t, ht, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ ({a} ∪ t).Finite

Tactic:
simp [ht]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
h : (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M) = {0} ∪ (a +ᵥ (↑(closure ({a} ∪ t)) : Set M))
⊢ IsSemilinearSet (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M)

Tactic:
convert! (IsSemilinearSet.singleton 0).union (isSemilinearSet ⟨a, { a } ∪ t, by simp [ht], rfl⟩)

Premises used: IsSemilinearSet.singleton, And.intro, Exists.intro, IsLinearSet.isSemilinearSet, Union.union, Singleton.singleton, OfNat.ofNat, IsSemilinearSet.union, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
h : ∀ (x : M), x ∈ (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M) ↔ x ∈ {0} ∪ (a +ᵥ (↑(closure ({a} ∪ t)) : Set M))
⊢ (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M) = {0} ∪ (a +ᵥ (↑(closure ({a} ∪ t)) : Set M))

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
h :
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x ↔
    x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
⊢ x ∈ (↑(closure (a +ᵥ (↑(closure t) : Set M))) : Set M) ↔ x ∈ {0} ∪ (a +ᵥ (↑(closure ({a} ∪ t)) : Set M))

Tactic:
simp only [SetLike.mem_coe, singleton_union, mem_insert_iff, mem_vadd_set, vadd_eq_add]

Premises used: Set.mem_vadd_set, Set.singleton_union, SetLike.mem_coe, vadd_eq_add, Set.mem_insert_iff
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
h :
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x →
    x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
h₁ :
  (x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x) →
    Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x
⊢ Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x ↔
    x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x

Tactic:
constructor
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 x : M
hx : x ∈ a +ᵥ (↑(closure t) : Set M)
h :
  ∀ (x : M) (hx : x ∈ (↑(closure t) : Set M)),
    Eq.{u_1 + 1} (α := M) ((fun (x : M) ↦ a +ᵥ x) x) 0 ∨
      ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = (fun (x : M) ↦ a +ᵥ x) x
⊢ x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x

Tactic:
rcases hx with ⟨x, hx, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 x : M
hx : x ∈ (↑(closure t) : Set M)
⊢ Eq.{u_1 + 1} (α := M) ((fun (x : M) ↦ a +ᵥ x) x) 0 ∨
    ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = (fun (x : M) ↦ a +ᵥ x) x

Tactic:
Or.inr ⟨x, closure_mono (subset_insert _ _) hx, rfl⟩

Premises used: And.intro, Exists.intro, Set.subset_insert, Or.inr, rfl, AddSubmonoid.closure_mono
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 x : M
hx : x ∈ (↑(closure t) : Set M)
⊢ Eq.{u_1 + 1} (α := M) ((fun (x : M) ↦ a +ᵥ x) x) 0 ∨
    ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = (fun (x : M) ↦ a +ᵥ x) x

Tactic:
exact Or.inr ⟨x, closure_mono (subset_insert _ _) hx, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
⊢ Eq.{u_1 + 1} (α := M) 0 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = 0

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
⊢ Eq.{u_1 + 1} (α := M) 0 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = 0

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 x y : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) x
hy : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) y
ih₁ : x = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = x
ih₂ : y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = y
h :
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0 →
    0 + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = 0 + y
h₁ :
  ∀ (x : M) (hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x),
    Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x) →
      a + x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + y
⊢ x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = x + y

Tactic:
rcases ih₁ with rfl | ⟨x, hx, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) y
ih₂ : y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = y
hx : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0
⊢ 0 + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = 0 + y

Tactic:
simpa
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 y : M
hy : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) y
ih₂ : y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = y
x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
h :
  Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0 →
    a + x + 0 = 0 ∨ ∃ (y : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y ∧ a + y = a + x + 0
h₁ :
  ∀ (y : M) (hy : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y),
    Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + y) →
      a + x + (a + y) = 0 ∨
        ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + (a + y)
⊢ a + x + y = 0 ∨ ∃ (y_1 : M), Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) y_1 ∧ a + y_1 = a + x + y

Tactic:
rcases ih₂ with rfl | ⟨y, hy, rfl⟩

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x_1 x : M
hx : Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x
hx_1 : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) (a + x)
hy : Membership.mem (γ := AddSubmonoid M) (closure (a +ᵥ (↑(closure t) : Set M))) 0
⊢ a + x = a + x + 0

Tactic:
simp