awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
simp_rw : IsSemilinearSet.{u_3} (M := ι → ℕ) (⋃ i ∈ S, (⇑f : (a : ι → ℕ) → M) ⁻¹' i)
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' ⋃₀ S)

Tactic:
simp_rw [sUnion_eq_biUnion, preimage_iUnion]

Premises used: Set.sUnion_eq_biUnion, Set.preimage_iUnion
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) (⋃ i ∈ S, (⇑f : (a : ι → ℕ) → M) ⁻¹' i)

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

Premises used: IsSemilinearSet.biUnion, _private.0.Nat.isSemilinearSet_preimage_of_isLinearSet
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
ι : Type u_3
inst : AddCommMonoid M
inst_1 : Finite ι
F : Type u_5
inst_2 : FunLike.{u_5 + 1, u_3 + 1, u_1 + 1} F (ι → ℕ) M
inst_3 : AddMonoidHomClass.{u_5, u_3, u_1} F (ι → ℕ) M
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) (⋃ i ∈ S, (⇑f : (a : ι → ℕ) → M) ⁻¹' i)

Tactic:
exact .biUnion hS fun s hs => isSemilinearSet_preimage_of_isLinearSet (hS' s hs) f
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
rcases :
  ∀ (n : ℕ) (g : (Fin n → ℕ) →+ M) (hg : Eq (α := AddSubmonoid M) (AddMonoidHom.mrange g) ⊤),
    IsSemilinearSet.{u_1} (M := M) ((⇑f : (a : M) → N) ⁻¹' s)
⊢ IsSemilinearSet.{u_1} (M := M) ((⇑f : (a : M) → N) ⁻¹' s)

Tactic:
rcases fg_iff_exists_fin_addMonoidHom.1 (AddMonoid.FG.fg_top (M := M)) with ⟨n, g, hg⟩

Premises used: AddMonoid.FG.fg_top, AddSubmonoid.fg_iff_exists_fin_addMonoidHom, Iff.mp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Eq (α := AddSubmonoid M) (AddMonoidHom.mrange g) ⊤
⊢ Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)

Tactic:
rw [AddMonoidHom.mrange_eq_top] at hg

Premises used: AddMonoidHom.mrange_eq_top
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)
rw :
  IsSemilinearSet (M := M)
    (Set.image (α := Fin n → ℕ) (⇑g : (a : Fin n → ℕ) → M)
      (Set.preimage (β := M) (⇑g : (a : Fin n → ℕ) → M) ((⇑f : (a : M) → N) ⁻¹' s)))
⊢ IsSemilinearSet.{u_1} (M := M) ((⇑f : (a : M) → N) ⁻¹' s)

Tactic:
rw [← image_preimage_eq (f ⁻¹' s) hg]

Premises used: Set.image_preimage_eq, Set.preimage, DFunLike.coe
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)
hs₁ : IsSemilinearSet (M := Fin n → ℕ) (Set.preimage (β := M) (⇑g : (a : Fin n → ℕ) → M) ((⇑f : (a : M) → N) ⁻¹' s))
⊢ IsSemilinearSet (M := M)
    (Set.image (α := Fin n → ℕ) (⇑g : (a : Fin n → ℕ) → M)
      (Set.preimage (β := M) (⇑g : (a : Fin n → ℕ) → M) ((⇑f : (a : M) → N) ⁻¹' s)))

Tactic:
apply image

Premises used: IsSemilinearSet.image
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)
hs₁ : IsSemilinearSet (M := Fin n → ℕ) ((⇑(AddMonoidHom.comp (↑f : M →+ N) g) : (a : Fin n → ℕ) → N) ⁻¹' s)
⊢ IsSemilinearSet (M := Fin n → ℕ) (Set.preimage (β := M) (⇑g : (a : Fin n → ℕ) → M) ((⇑f : (a : M) → N) ⁻¹' s))

Tactic:
rw [← preimage_comp, ← AddMonoidHom.coe_coe, ← AddMonoidHom.coe_comp]

Premises used: AddMonoidHom.coe_coe, Set.preimage_comp, AddMonoidHom.coe_comp
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)
⊢ IsSemilinearSet (M := Fin n → ℕ) ((⇑(AddMonoidHom.comp (↑f : M →+ N) g) : (a : Fin n → ℕ) → N) ⁻¹' s)

Tactic:
Nat.isSemilinearSet_preimage hs _

Premises used: _private.0.Nat.isSemilinearSet_preimage
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
N : Type u_2
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : AddMonoid.FG M
F : Type u_5
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
s : Set N
hs : IsSemilinearSet s
f : F
n : ℕ
g : (Fin n → ℕ) →+ M
hg : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑g : (a : Fin n → ℕ) → M)
⊢ IsSemilinearSet (M := Fin n → ℕ) ((⇑(AddMonoidHom.comp (↑f : M →+ N) g) : (a : Fin n → ℕ) → N) ⁻¹' s)

Tactic:
exact Nat.isSemilinearSet_preimage hs _

Premises used: _private.0.Nat.isSemilinearSet_preimage
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : IsLinearSet s
rcases :
  ∀ (a : M) (t : Set M) (ht : t.Finite),
    ∃ (P : AddSubmonoid M) (s' : Set ↥P),
      P.FG ∧ IsLinearSet s' ∧ a +ᵥ (↑(closure t) : Set M) = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsLinearSet s' ∧ s = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'

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

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P),
    P.FG ∧ IsLinearSet s' ∧ a +ᵥ (↑(closure t) : Set M) = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'

Tactic:
⟨_, _, (fg_iff _).2 ⟨insert a t, rfl, ht.insert a⟩,
    ⟨⟨_, mem_closure_of_mem (mem_insert a t)⟩, _, ht.preimage Subtype.val_injective.injOn, rfl⟩, ?_⟩

Premises used: Iff.mpr, Subtype.val_injective, Function.Injective.injOn, Insert.insert, AddSubmonoid.fg_iff, AddSubmonoid.mem_closure_of_mem, Subtype.mk, And.intro, Exists.intro, Set.mem_insert, Set.Finite.insert, rfl, Set.Finite.preimage
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
refine :
  a +ᵥ (↑(closure t) : Set M) =
    Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) ''
      HVAdd.hVAdd (α := ↥(closure (insert a t)))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) a ⋯)
        (↑(closure
              (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) ⁻¹' t)) :
          Set ↥(closure (insert a t)))
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P),
    P.FG ∧ IsLinearSet s' ∧ a +ᵥ (↑(closure t) : Set M) = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'

Tactic:
refine ⟨_, _, (fg_iff _).2 ⟨insert a t, rfl, ht.insert a⟩,
    ⟨⟨_, mem_closure_of_mem (mem_insert a t)⟩, _, ht.preimage Subtype.val_injective.injOn, rfl⟩, ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
rw :
  a +ᵥ (↑(closure t) : Set M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) a ⋯) : M) +ᵥ
      (↑(closure
            (Set.image (α := ↥(closure (insert a t)))
              (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
              ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t))) :
        Set M)
⊢ a +ᵥ (↑(closure t) : Set M) =
    Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) ''
      HVAdd.hVAdd (α := ↥(closure (insert a t)))
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) a ⋯)
        (↑(closure
              (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) ⁻¹' t)) :
          Set ↥(closure (insert a t)))

Tactic:
rw [← coe_subtype, image_vadd_distrib, subtype_apply, ← coe_map, AddMonoidHom.map_mclosure]

Premises used: AddSubmonoid.coe_map, AddMonoidHom.map_mclosure, Set.image_vadd_distrib, AddSubmonoid.subtype_apply, AddSubmonoid.coe_subtype
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
e_a :
  t =
    Set.image (α := ↥(closure (insert a t))) (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
      ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t)
⊢ a +ᵥ (↑(closure t) : Set M) =
    (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := AddSubmonoid M) (closure (insert a t)) x) a ⋯) : M) +ᵥ
      (↑(closure
            (Set.image (α := ↥(closure (insert a t)))
              (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
              ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t))) :
        Set M)

Tactic:
congr
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
e_a :
  ∀ (x : M),
    x ∈ t ↔
      Membership.mem (γ := Set M)
        (Set.image (α := ↥(closure (insert a t)))
          (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
          ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t))
        x
⊢ t =
    Set.image (α := ↥(closure (insert a t))) (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
      ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t)

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
⊢ x ∈ t ↔
    Membership.mem (γ := Set M)
      (Set.image (α := ↥(closure (insert a t))) (⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M)
        ((⇑(subtype (closure (insert a t))) : (a : ↥(closure (insert a t))) → M) ⁻¹' t))
      x

Tactic:
simpa using mem_closure_of_mem ∘ mem_insert_of_mem a

Premises used: Set.mem_insert_of_mem, AddSubmonoid.mem_closure_of_mem
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
hs : IsSemilinearSet s
rcases :
  ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t),
    ∃ (P : AddSubmonoid M) (s' : Set ↥P),
      P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ s = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'

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

Premises used: rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
choose! :
  ∀ (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),
    ∃ (P : AddSubmonoid M) (s' : Set ↥P),
      P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'

Tactic:
choose! P t hP ht ht' using fun s hs => (hS' s hs).exists_fg_eq_subtypeVal

Premises used: IsLinearSet.exists_fg_eq_subtypeVal
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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
⊢ Finite.{u_1 + 1} (↑S : Type u_1)

Tactic:
haveI : Finite S := hS
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'

Tactic:
⟨⨆ s : S, P s, ⋃ (s : S), AddSubmonoid.inclusion (le_iSup _ s) '' t s.1,
    .iSup _ fun s => hP s s.2, .iUnion fun s => (ht s s.2).isSemilinearSet.image _, ?_⟩

Premises used: iSup, IsSemilinearSet.iUnion, IsSemilinearSet.image, AddSubmonoid.FG.iSup, le_iSup, AddSubmonoid.inclusion, And.intro, Exists.intro, Set.image, IsLinearSet.isSemilinearSet, Subtype.val, DFunLike.coe, Set.iUnion, Subtype.property
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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)
refine :
  ⋃₀ 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)))
⊢ ∃ (P : AddSubmonoid M) (s' : Set ↥P), P.FG ∧ IsSemilinearSet s' ∧ ⋃₀ S = Subtype.val (p := fun (x : M) ↦ x ∈ P) '' s'

Tactic:
refine ⟨⨆ s : S, P s, ⋃ (s : S), AddSubmonoid.inclusion (le_iSup _ s) '' t s.1,
    .iSup _ fun s => hP s s.2, .iUnion fun s => (ht s s.2).isSemilinearSet.image _, ?_⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
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))
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))
⊢ ⋃₀ 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)))

Tactic:
simp_rw [sUnion_eq_iUnion, image_iUnion, image_image, AddSubmonoid.coe_inclusion,
    fun s : S => ht' s s.2]

Premises used: Set.image_image, Set.sUnion_eq_iUnion, Set.image_iUnion, Subtype.val, Subtype.property, AddSubmonoid.coe_inclusion
-- 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₁' : 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₂'
⊢ ∃ (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₂'

Tactic:
rcases hs₁.exists_fg_eq_subtypeVal with ⟨P₁, s₁', hP₁, 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
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₁')
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
⊢ ∃ (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⟩

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₁' : 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

Tactic:
⟨P₁ ⊔ P₂, (AddSubmonoid.inclusion le_sup_left) '' s₁',
    (AddSubmonoid.inclusion le_sup_right) '' s₂', hP₁.sup hP₂, hs₁'.image _, ?_, hs₂'.image _, ?_⟩

Premises used: le_sup_left, IsSemilinearSet.image, le_sup_right, AddSubmonoid.inclusion, Max.max, And.intro, Exists.intro, Set.image, DFunLike.coe, AddSubmonoid.FG.sup
-- 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_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₁')
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 ⋯) : (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

Tactic:
refine ⟨P₁ ⊔ P₂, (AddSubmonoid.inclusion le_sup_left) '' s₁',
    (AddSubmonoid.inclusion le_sup_right) '' s₂', hP₁.sup hP₂, hs₁'.image _, ?_, hs₂'.image _, ?_⟩
-- 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_1 :
  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