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
G : Type u_6
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
inst_4 : FunLike.{u_6 + 1, u_3 + 1, u_1 + 1} G (ι → ℕ) M
inst_5 : AddMonoidHomClass.{u_6, u_3, u_1} G (ι → ℕ) M
a b : M
f : F
g : G
x y z : ι → ℕ
hx : HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M) = HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)
hy :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M)
hz :
  HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) z : M)
conv_lhs :
  HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
      ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
      ((g : (a : ι → ℕ) → M) z : M)
hs :
  HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
      ((g : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
      ((g : (a : ι → ℕ) → M) z : M)
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) a ((f : (a : ι → ℕ) → M) x : M)) ((f : (a : ι → ℕ) → M) y : M))
      ((f : (a : ι → ℕ) → M) z : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (β := M) (HAdd.hAdd (β := M) b ((g : (a : ι → ℕ) → M) x : M)) ((g : (a : ι → ℕ) → M) y : M))
      ((g : (a : ι → ℕ) → M) z : M)

Tactic:
conv_lhs => rw [hy, ← hx, add_right_comm _ (g y) (f z), hz, add_right_comm _ (g z)]

Premises used: add_right_comm, 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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
rcases :
  ∀ (n : ℕ) (h : (Fin n → ℕ) →+ M) (hh : Eq (α := AddSubmonoid M) (AddMonoidHom.mrange h) ⊤),
    IsSemilinearSet.{u_1} (M := M)
      {x : M | HAdd.hAdd (β := N) a ((f : (a : M) → N) x : N) = HAdd.hAdd (β := N) b ((g : (a : M) → N) x : N)}
⊢ IsSemilinearSet.{u_1} (M := M)
    {x : M | HAdd.hAdd (β := N) a ((f : (a : M) → N) x : N) = HAdd.hAdd (β := N) b ((g : (a : M) → N) x : N)}

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

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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Eq (α := AddSubmonoid M) (AddMonoidHom.mrange h) ⊤
⊢ Function.Surjective (α := Fin n → ℕ) (β := M) (⇑h : (a : Fin n → ℕ) → M)

Tactic:
rw [AddMonoidHom.mrange_eq_top] at hh

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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑h : (a : Fin n → ℕ) → M)
rw :
  IsSemilinearSet (M := M)
    (image (α := Fin n → ℕ) (⇑h : (a : Fin n → ℕ) → M)
      {a_1 : Fin n → ℕ |
        HAdd.hAdd (β := N) a ((f : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N) =
          HAdd.hAdd (β := N) b ((g : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N)})
⊢ IsSemilinearSet.{u_1} (M := M)
    {x : M | HAdd.hAdd (β := N) a ((f : (a : M) → N) x : N) = HAdd.hAdd (β := N) b ((g : (a : M) → N) x : N)}

Tactic:
rw [← image_preimage_eq { x | a + f x = b + g x } hh, preimage_setOf_eq]

Premises used: setOf, Set.image_preimage_eq, Set.preimage_setOf_eq, HAdd.hAdd, Eq, 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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑h : (a : Fin n → ℕ) → M)
hs :
  IsSemilinearSet (M := Fin n → ℕ)
    {a_1 : Fin n → ℕ |
      HAdd.hAdd (β := N) a ((f : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N) =
        HAdd.hAdd (β := N) b ((g : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N)}
⊢ IsSemilinearSet (M := M)
    (image (α := Fin n → ℕ) (⇑h : (a : Fin n → ℕ) → M)
      {a_1 : Fin n → ℕ |
        HAdd.hAdd (β := N) a ((f : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N) =
          HAdd.hAdd (β := N) b ((g : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N)})

Tactic:
apply IsSemilinearSet.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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑h : (a : Fin n → ℕ) → M)
⊢ IsSemilinearSet (M := Fin n → ℕ)
    {a_1 : Fin n → ℕ |
      HAdd.hAdd (β := N) a ((f : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N) =
        HAdd.hAdd (β := N) b ((g : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N)}

Tactic:
Nat.isSemilinearSet_setOf_eq a b (AddMonoidHom.comp f h) (AddMonoidHom.comp g h)

Premises used: setOf, AddMonoidHom.comp, _private.0.Nat.isSemilinearSet_setOf_eq
-- 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
G : Type u_6
inst_3 : FunLike F M N
inst_4 : AddMonoidHomClass F M N
inst_5 : FunLike G M N
inst_6 : AddMonoidHomClass G M N
a b : N
f : F
g : G
n : ℕ
h : (Fin n → ℕ) →+ M
hh : Function.Surjective (α := Fin n → ℕ) (β := M) (⇑h : (a : Fin n → ℕ) → M)
⊢ IsSemilinearSet (M := Fin n → ℕ)
    {a_1 : Fin n → ℕ |
      HAdd.hAdd (β := N) a ((f : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N) =
        HAdd.hAdd (β := N) b ((g : (a : M) → N) ((h : (a : Fin n → ℕ) → M) a_1 : M) : N)}

Tactic:
exact Nat.isSemilinearSet_setOf_eq a b (AddMonoidHom.comp f h) (AddMonoidHom.comp g h)

Premises used: AddMonoidHom.comp, _private.0.Nat.isSemilinearSet_setOf_eq
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
κ : Type u_4
inst : Fintype κ
u v : ι → ℕ
A B : Matrix ι κ ℕ
⊢ IsSemilinearSet.{u_4} (M := κ → ℕ) {x : κ → ℕ | u + A *ᵥ x = v + B *ᵥ x}

Tactic:
isSemilinearSet_setOf_eq u v A.mulVecLin B.mulVecLin

Premises used: Multiset.sum, Multiset.foldr, dotProduct, setOf, Matrix.mulVecLin, Matrix.mulVec, Finset.sum, _private.0.Nat.isSemilinearSet_setOf_eq
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
simp_rw :
  (∃ (a : M) (P : AddSubmonoid M),
      (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
    ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
⊢ IsLinearSet s ↔
    ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M),
      s = HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → M))

Tactic:
simp_rw [isLinearSet_iff_exists_fg_eq_vadd, fg_iff_exists_fin_addMonoidHom,
    ← AddMonoidHom.coe_mrange]

Premises used: AddSubmonoid.fg_iff_exists_fin_addMonoidHom, isLinearSet_iff_exists_fg_eq_vadd, AddMonoidHom.coe_mrange
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a :
  ∀ (a : M),
    (∃ (P : AddSubmonoid M), (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
      ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
⊢ (∃ (a : M) (P : AddSubmonoid M),
      (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
    ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)

Tactic:
congr! with a
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
⊢ (∃ (P : AddSubmonoid M), (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
    ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)

Tactic:
⟨fun ⟨P, ⟨n, f, hf⟩, hs⟩ => ⟨n, f, ?_⟩, fun ⟨n, f, hs⟩ => ⟨_, ⟨n, f, rfl⟩, ?_⟩⟩

Premises used: Exists, AddMonoidHom.mrange, _private.0.isLinearSet_iff_exists_fin_addMonoidHom.match_4, HVAdd.hVAdd, And, SetLike.coe, _private.0.isLinearSet_iff_exists_fin_addMonoidHom.match_3, And.intro, Iff.intro, Exists.intro, Eq, rfl
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
a₁ :
  (∃ (P : AddSubmonoid M), (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) →
    ∀ (P : AddSubmonoid M) (n : ℕ) (f : (Fin n → ℕ) →+ M) (hf : AddMonoidHom.mrange f = P) (hs : s = a +ᵥ (↑P : Set M)),
      s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
a₂ :
  (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)) →
    ∀ (n : ℕ) (f : (Fin n → ℕ) →+ M) (hs : s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)),
      s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
⊢ (∃ (P : AddSubmonoid M), (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)) ↔
    ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)

Tactic:
refine ⟨fun ⟨P, ⟨n, f, hf⟩, hs⟩ => ⟨n, f, ?_⟩, fun ⟨n, f, hs⟩ => ⟨_, ⟨n, f, rfl⟩, ?_⟩⟩
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
h : ∃ (P : AddSubmonoid M), (∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = P) ∧ s = a +ᵥ (↑P : Set M)
P : AddSubmonoid M
n : ℕ
f : (Fin n → ℕ) →+ M
hf : AddMonoidHom.mrange f = P
hs a₁ : s = a +ᵥ (↑P : Set M)
a₂ a₃ : a +ᵥ (↑P : Set M) = a +ᵥ (↑P : Set M)
⊢ s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)

Tactic:
rw [hf, hs]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
M : Type u_1
inst : AddCommMonoid M
s : Set M
a : M
h : ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
n : ℕ
f : (Fin n → ℕ) →+ M
hs : s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
a₁ a₂ : a +ᵥ (↑(AddMonoidHom.mrange f) : Set M) = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)
⊢ s = a +ᵥ (↑(AddMonoidHom.mrange f) : Set M)

Tactic:
rw [hs]
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
rw :
  (∃ (a : ι → ℕ) (n : ℕ) (f : (Fin n → ℕ) →+ ι → ℕ),
      s = HVAdd.hVAdd (β := Set (ι → ℕ)) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))) ↔
    ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
⊢ IsLinearSet s ↔
    ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}

Tactic:
rw [isLinearSet_iff_exists_fin_addMonoidHom]

Premises used: isLinearSet_iff_exists_fin_addMonoidHom
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
⊢ (∃ (a : ι → ℕ) (n : ℕ) (f : (Fin n → ℕ) →+ ι → ℕ),
      s = HVAdd.hVAdd (β := Set (ι → ℕ)) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))) ↔
    ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}

Tactic:
exists₂_congr fun v n => ⟨fun ⟨f, hf⟩ => ⟨f.toNatLinearMap.toMatrix', ?_⟩, fun ⟨A, hA⟩ =>
    ⟨A.mulVecLin, ?_⟩⟩

Premises used: _private.0.Nat.isLinearSet_iff_exists_matrix.match_2, AddMonoidHomClass.toAddMonoidHom, setOf, Exists, AddMonoidHom.toNatLinearMap, LinearMap.toMatrix', HVAdd.hVAdd, exists₂_congr, _private.0.Nat.isLinearSet_iff_exists_matrix.match_1, Matrix.mulVecLin, HAdd.hAdd, Iff.intro, Exists.intro, Set.range, Matrix.mulVec, Eq, DFunLike.coe
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
refine_1 :
  ∀ (v : ι → ℕ) (n : ℕ),
    (∃ (f : (Fin n → ℕ) →+ ι → ℕ),
        s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))) →
      ∀ (f : (Fin n → ℕ) →+ ι → ℕ)
        (hf : s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))),
        s =
          {x : ι → ℕ |
            ∃ (x_1 : Fin n → ℕ),
              v + (LinearMap.toMatrix' : (a : (Fin n → ℕ) →ₗ[ℕ] ι → ℕ) → Matrix ι (Fin n) ℕ) f.toNatLinearMap *ᵥ x_1 =
                x}
refine_2 :
  ∀ (v : ι → ℕ) (n : ℕ),
    (∃ (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}) →
      ∀ (A : Matrix ι (Fin n) ℕ) (hA : s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}),
        s =
          HVAdd.hVAdd (β := Set (ι → ℕ)) v
            (range (ι := Fin n → ℕ) (⇑(↑A.mulVecLin : (Fin n → ℕ) →+ ι → ℕ) : (a : Fin n → ℕ) → ι → ℕ))
⊢ (∃ (a : ι → ℕ) (n : ℕ) (f : (Fin n → ℕ) →+ ι → ℕ),
      s = HVAdd.hVAdd (β := Set (ι → ℕ)) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))) ↔
    ∃ (v : ι → ℕ) (n : ℕ) (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}

Tactic:
refine exists₂_congr fun v n => ⟨fun ⟨f, hf⟩ => ⟨f.toNatLinearMap.toMatrix', ?_⟩, fun ⟨A, hA⟩ =>
    ⟨A.mulVecLin, ?_⟩⟩

Premises used: exists₂_congr, Iff.intro
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
h :
  ∃ (f : (Fin n → ℕ) →+ ι → ℕ),
    s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))
f : (Fin n → ℕ) →+ ι → ℕ
hf : s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))
refine_1 :
  ∀ (x : ι → ℕ),
    x ∈ s ↔
      Membership.mem (γ := Set (ι → ℕ))
        {x : ι → ℕ |
          ∃ (x_1 : Fin n → ℕ),
            v + (LinearMap.toMatrix' : (a : (Fin n → ℕ) →ₗ[ℕ] ι → ℕ) → Matrix ι (Fin n) ℕ) f.toNatLinearMap *ᵥ x_1 = x}
        x
⊢ s =
    {x : ι → ℕ |
      ∃ (x_1 : Fin n → ℕ),
        v + (LinearMap.toMatrix' : (a : (Fin n → ℕ) →ₗ[ℕ] ι → ℕ) → Matrix ι (Fin n) ℕ) f.toNatLinearMap *ᵥ x_1 = x}

Tactic:
ext
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
h : ∃ (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
A : Matrix ι (Fin n) ℕ
hA : s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
refine_2 :
  ∀ (x : ι → ℕ),
    x ∈ s ↔
      x ∈
        HVAdd.hVAdd (β := Set (ι → ℕ)) v
          (range (ι := Fin n → ℕ) (⇑(↑A.mulVecLin : (Fin n → ℕ) →+ ι → ℕ) : (a : Fin n → ℕ) → ι → ℕ))
⊢ s =
    HVAdd.hVAdd (β := Set (ι → ℕ)) v
      (range (ι := Fin n → ℕ) (⇑(↑A.mulVecLin : (Fin n → ℕ) →+ ι → ℕ) : (a : Fin n → ℕ) → ι → ℕ))

Tactic:
ext
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
h :
  ∃ (f : (Fin n → ℕ) →+ ι → ℕ),
    s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))
f : (Fin n → ℕ) →+ ι → ℕ
hf : s = HVAdd.hVAdd (β := Set (ι → ℕ)) v (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → ι → ℕ))
x : ι → ℕ
⊢ x ∈ s ↔
    Membership.mem (γ := Set (ι → ℕ))
      {x : ι → ℕ |
        ∃ (x_1 : Fin n → ℕ),
          v + (LinearMap.toMatrix' : (a : (Fin n → ℕ) →ₗ[ℕ] ι → ℕ) → Matrix ι (Fin n) ℕ) f.toNatLinearMap *ᵥ x_1 = x}
      x

Tactic:
simp [*, mem_vadd_set]

Premises used: Set.mem_vadd_set
-- Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
Goal:
ι : Type u_3
s : Set (ι → ℕ)
v : ι → ℕ
n : ℕ
h : ∃ (A : Matrix ι (Fin n) ℕ), s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
A : Matrix ι (Fin n) ℕ
hA : s = {x : ι → ℕ | ∃ (x_1 : Fin n → ℕ), v + A *ᵥ x_1 = x}
x : ι → ℕ
⊢ x ∈ s ↔
    x ∈
      HVAdd.hVAdd (β := Set (ι → ℕ)) v
        (range (ι := Fin n → ℕ) (⇑(↑A.mulVecLin : (Fin n → ℕ) →+ ι → ℕ) : (a : Fin n → ℕ) → ι → ℕ))

Tactic:
simp [*, mem_vadd_set]

Premises used: Set.mem_vadd_set
-- 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
s : Set M
hs : IsLinearSet s
f : F
rw :
  ∀
    (hs :
      ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M),
        s = HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → M)))
    (f : F), IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' s)
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' s)

Tactic:
rw [isLinearSet_iff_exists_fin_addMonoidHom] at hs

Premises used: isLinearSet_iff_exists_fin_addMonoidHom
-- 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
s : Set M
hs :
  ∃ (a : M) (n : ℕ) (f : (Fin n → ℕ) →+ M),
    s = HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑f : (a : Fin n → ℕ) → M))
f : F
rcases :
  ∀ (a : M) (n : ℕ) (g : (Fin n → ℕ) →+ M),
    IsSemilinearSet.{u_3} (M := ι → ℕ)
      ((⇑f : (a : ι → ℕ) → M) ⁻¹' HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑g : (a : Fin n → ℕ) → M)))
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' s)

Tactic:
rcases hs with ⟨a, n, g, rfl⟩

Premises used: rfl
-- 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
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
simp :
  IsSemilinearSet.{u_3} (M := ι → ℕ)
    {x : ι → ℕ |
      ∃ (a_1 : Fin n → ℕ), HAdd.hAdd (β := M) a ((g : (a : Fin n → ℕ) → M) a_1 : M) = (f : (a : ι → ℕ) → M) x}
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    {x : ι → ℕ |
      Membership.mem (α := M) (HVAdd.hVAdd (β := Set M) a (range (ι := Fin n → ℕ) (⇑g : (a : Fin n → ℕ) → M)))
        ((f : (a : ι → ℕ) → M) x : M)}

Tactic:
simp only [mem_vadd_set, mem_range, vadd_eq_add, exists_exists_eq_and]

Premises used: Set.mem_range, Set.mem_vadd_set, exists_exists_eq_and, vadd_eq_add
-- 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
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
a₁ :
  IsSemilinearSet.{u_3} (M := ι ⊕ Fin n → ℕ)
    {x : ι ⊕ Fin n → ℕ |
      HAdd.hAdd (β := M) a ((g : (a : Fin n → ℕ) → M) (x ∘ Sum.inr) : M) = (f : (a : ι → ℕ) → M) (x ∘ Sum.inl)}
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ)
    {x : ι → ℕ |
      ∃ (a_1 : Fin n → ℕ), HAdd.hAdd (β := M) a ((g : (a : Fin n → ℕ) → M) a_1 : M) = (f : (a : ι → ℕ) → M) x}

Tactic:
apply IsSemilinearSet.proj'

Premises used: IsSemilinearSet.proj'
-- 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
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
⊢ IsSemilinearSet.{u_3} (M := ι ⊕ Fin n → ℕ)
    {x : ι ⊕ Fin n → ℕ |
      HAdd.hAdd (β := M) a
          ((g.comp
                  (LinearMap.toAddMonoidHom (modM₁ := Pi.Function.module (ι ⊕ Fin n) ℕ ℕ)
                    (LinearMap.funLeft ℕ ℕ Sum.inr)) :
                (a : ι ⊕ Fin n → ℕ) → M)
              x :
            M) =
        HAdd.hAdd (α := M) (β := M) (0 : M)
          ((AddMonoidHom.comp (↑f : (ι → ℕ) →+ M)
                  (LinearMap.toAddMonoidHom (modM₁ := Pi.Function.module (ι ⊕ Fin n) ℕ ℕ)
                    (LinearMap.funLeft ℕ ℕ Sum.inl)) :
                (a : ι ⊕ Fin n → ℕ) → M)
              x :
            M)}

Tactic:
isSemilinearSet_setOf_eq a 0 (g.comp (LinearMap.funLeft ℕ ℕ Sum.inr).toAddMonoidHom)
      ((f : (ι → ℕ) →+ M).comp (LinearMap.funLeft ℕ ℕ Sum.inl).toAddMonoidHom)

Premises used: LinearMap.toAddMonoidHom, AddMonoidHomClass.toAddMonoidHom, Sum.inl, Sum.inr, LinearMap.funLeft, Nat, OfNat.ofNat, AddMonoidHom.comp, _private.0.Nat.isSemilinearSet_setOf_eq
-- 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
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
h :
  ∀ (x : ι ⊕ Fin n → ℕ),
    (f : (a : ι → ℕ) → M) (x ∘ Sum.inl) =
      HAdd.hAdd (α := M) (β := M) (0 : M)
        ((AddMonoidHom.comp (↑f : (ι → ℕ) →+ M)
                (LinearMap.toAddMonoidHom (modM₁ := Pi.Function.module (ι ⊕ Fin n) ℕ ℕ)
                  (LinearMap.funLeft ℕ ℕ Sum.inl)) :
              (a : ι ⊕ Fin n → ℕ) → M)
            x :
          M)
⊢ IsSemilinearSet.{u_3} (M := ι ⊕ Fin n → ℕ)
    {x : ι ⊕ Fin n → ℕ |
      HAdd.hAdd (β := M) a ((g : (a : Fin n → ℕ) → M) (x ∘ Sum.inr) : M) = (f : (a : ι → ℕ) → M) (x ∘ Sum.inl)}

Tactic:
convert!
    isSemilinearSet_setOf_eq a 0 (g.comp (LinearMap.funLeft ℕ ℕ Sum.inr).toAddMonoidHom)
      ((f : (ι → ℕ) →+ M).comp (LinearMap.funLeft ℕ ℕ Sum.inl).toAddMonoidHom)

Premises used: LinearMap.toAddMonoidHom, AddMonoidHomClass.toAddMonoidHom, Sum.inl, Sum.inr, LinearMap.funLeft, Nat, OfNat.ofNat, AddMonoidHom.comp, _private.0.Nat.isSemilinearSet_setOf_eq
-- 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
a : M
n : ℕ
g : (Fin n → ℕ) →+ M
x : ι ⊕ Fin n → ℕ
⊢ (f : (a : ι → ℕ) → M) (x ∘ Sum.inl) =
    HAdd.hAdd (α := M) (β := M) (0 : M)
      ((AddMonoidHom.comp (↑f : (ι → ℕ) →+ M)
              (LinearMap.toAddMonoidHom (modM₁ := Pi.Function.module (ι ⊕ Fin n) ℕ ℕ) (LinearMap.funLeft ℕ ℕ Sum.inl)) :
            (a : ι ⊕ Fin n → ℕ) → M)
          x :
        M)

Tactic:
simp [LinearMap.funLeft]

Premises used: LinearMap.funLeft
-- 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
s : Set M
hs : IsSemilinearSet s
f : F
rcases :
  ∀ (S : Set (Set M)) (hS : S.Finite) (hS' : ∀ t ∈ S, IsLinearSet t),
    IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' ⋃₀ S)
⊢ IsSemilinearSet.{u_3} (M := ι → ℕ) ((⇑f : (a : ι → ℕ) → M) ⁻¹' s)

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

Premises used: rfl