mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
hs : ∀ (f g : (ι → ℕ) → ℕ), ∑ i ∈ t, f i • id i = ∑ i ∈ t, g i • id i → ∀ i ∈ t, f i = g i
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
⊢ f i = 0

Tactic:
]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
hs : ∀ (f g : (ι → ℕ) → ℕ), ∑ i ∈ t, f i • id i = ∑ i ∈ t, g i • id i → ∀ i ∈ t, f i = g i
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
⊢ f i = 0
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ (RelMap R fun a ↦ Structure.Sigma.mk f i (x a)) = RelMap R x

Tactic:
]

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ (RelMap R fun a ↦ Structure.Sigma.mk f i (x a)) = RelMap R x
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g h : M ≃ₚ[L] N
le_fg : f.dom ≤ g.dom
eq_fg : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion le_fg)) = f.cod.subtype.comp f.toEquiv.toEmbedding
le_gh : g.dom ≤ h.dom
eq_gh : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh)) = g.cod.subtype.comp g.toEquiv.toEmbedding
⊢ h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh))).comp (inclusion le_fg)

Tactic:
]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g h : M ≃ₚ[L] N
le_fg : f.dom ≤ g.dom
eq_fg : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion le_fg)) = f.cod.subtype.comp f.toEquiv.toEmbedding
le_gh : g.dom ≤ h.dom
eq_gh : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh)) = g.cod.subtype.comp g.toEquiv.toEmbedding
⊢ h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh))).comp (inclusion le_fg)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ RelMap R (unify f (fun a ↦ Structure.Sigma.mk f i (x a)) i ⋯) = RelMap R x

Tactic:
]

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ RelMap R (unify f (fun a ↦ Structure.Sigma.mk f i (x a)) i ⋯) = RelMap R x
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
n : ℕ
R : L.Relations n
i : ι
x : Fin n → G i
⊢ RelMap R x = RelMap R x

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
hs : ∀ (f g : (ι → ℕ) → ℕ), ∑ i ∈ t, f i • id i = ∑ i ∈ t, g i • id i → ∀ i ∈ t, f i = g i
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
⊢ ∑ x ∈ t, (toRatVec ((Int.toNat ∘ f) x • id x) - toRatVec ((Int.toNat ∘ (fun x ↦ -x) ∘ f) x • id x)) =
    ∑ i ∈ t, f i • toRatVec i

Tactic:
]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
hs : ∀ (f g : (ι → ℕ) → ℕ), ∑ i ∈ t, f i • id i = ∑ i ∈ t, g i • id i → ∀ i ∈ t, f i = g i
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
⊢ ∑ x ∈ t, (toRatVec ((Int.toNat ∘ f) x • id x) - toRatVec ((Int.toNat ∘ (fun x ↦ -x) ∘ f) x • id x)) =
    ∑ i ∈ t, f i • toRatVec i
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ ∃ (dom_le_dom : f.symm.dom ≤ g.symm.dom) (cod_le_cod : f.symm.cod ≤ g.symm.cod),
    ∀ (x : ↥f.symm.dom), (inclusion cod_le_cod) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion dom_le_dom) x)

Tactic:
]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
⊢ ∃ (dom_le_dom : f.symm.dom ≤ g.symm.dom) (cod_le_cod : f.symm.cod ≤ g.symm.cod),
    ∀ (x : ↥f.symm.dom), (inclusion cod_le_cod) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion dom_le_dom) x)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
⊢ Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f ((Quotient.out ∘ x) a).fst i ⋯) ((Quotient.out ∘ x) a).snd)

Tactic:
]

Goal state after:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
⊢ Quotient.out (x a) ≈ Structure.Sigma.mk f i ((f ((Quotient.out ∘ x) a).fst i ⋯) ((Quotient.out ∘ x) a).snd)
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.toEquiv.symm x)) = (inclusion ⋯) (f.toEquiv (f.toEquiv.symm x))

Tactic:
]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
hfg : f ≤ g
x : ↥f.symm.dom
⊢ g.toEquiv ((inclusion ⋯) (f.toEquiv.symm x)) = (inclusion ⋯) (f.toEquiv (f.toEquiv.symm x))
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i
⊢ (f (Quotient.out (x a)).fst i ⋯) (Quotient.out (x a)).snd =
    (f (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst i this)
      (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).snd

pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i
⊢ (Quotient.out (x a)).fst ∈ range fun a ↦ (Quotient.out (x a)).fst

Tactic:
]

Goal state after:
L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i
⊢ (f (Quotient.out (x a)).fst i ⋯) (Quotient.out (x a)).snd =
    (f (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst i this)
      (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).snd

L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
α : Type u_1
inst✝ : Finite α
x : α → DirectLimit G f
i : ι
hi : i ∈ upperBounds (range fun a ↦ (Quotient.out (x a)).fst)
a : α
r : ((Quotient.out ∘ x) a).fst ≤ i
this : (Structure.Sigma.mk f i ((f (Quotient.out (x a)).fst i r) (Quotient.out (x a)).snd)).fst ≤ i
⊢ (Quotient.out (x a)).fst ∈ range fun a ↦ (Quotient.out (x a)).fst
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f.symm.symm ≤ g.symm

Tactic:
]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f.symm ≤ g
⊢ f.symm.symm ≤ g.symm
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hs : (Int.toNat ∘ f) i = (Int.toNat ∘ (fun x ↦ -x) ∘ f) i
hi : i ∈ t
⊢ (f i).toNat = (-f i).toNat

Tactic:
]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hs : (Int.toNat ∘ f) i = (Int.toNat ∘ (fun x ↦ -x) ∘ f) i
hi : i ∈ t
⊢ (f i).toNat = (-f i).toNat
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g.symm.symm

Tactic:
]

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
g : N ≃ₚ[L] M
h : f ≤ g.symm
⊢ f.symm ≤ g.symm.symm
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ ⊤ ≤ span ℚ (⇑toRatVec '' (hs.periods ∪ range ⇑(Pi.basisFun ℕ ι)))

Tactic:
]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ ⊤ ≤ span ℚ (⇑toRatVec '' (hs.periods ∪ range ⇑(Pi.basisFun ℕ ι)))
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i : ι
x y : G i
h : (setoid G f) (Structure.Sigma.mk f i x) (Structure.Sigma.mk f i y)
⊢ x = y

Tactic:
]

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i : ι
x y : G i
h : (setoid G f) (Structure.Sigma.mk f i x) (Structure.Sigma.mk f i y)
⊢ x = y
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ span ℚ (⇑toRatVec '' range ⇑(Pi.basisFun ℕ ι)) = ⊤

Tactic:
]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
⊢ span ℚ (⇑toRatVec '' range ⇑(Pi.basisFun ℕ ι)) = ⊤
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i : ι
n✝ : ℕ
F : L.Functions n✝
x : Fin n✝ → G i
⊢ (funMap F fun a ↦ ⟦Structure.Sigma.mk f i (x a)⟧) = funMap F ((fun a ↦ ⟦Structure.Sigma.mk f i a⟧) ∘ x)

Tactic:
]

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i : ι
n✝ : ℕ
F : L.Functions n✝
x : Fin n✝ → G i
⊢ (funMap F fun a ↦ ⟦Structure.Sigma.mk f i (x a)⟧) = funMap F ((fun a ↦ ⟦Structure.Sigma.mk f i a⟧) ∘ x)
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
dom_f : L.Substructure M
cod_f : L.Substructure N
equiv_f : ↥dom_f ≃[L] ↥cod_f
h_dom : { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom = g.dom
h :
  ∀ (x : M) (h : x ∈ { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := dom_f, cod := cod_f, toEquiv := equiv_f } = g

Tactic:
cases h_dom

Goal state after:
case refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } = g
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
⊢ ∑ i, (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i ≤ ∑ x, toRatVec ↑x

Tactic:
]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
⊢ ∑ i, (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i ≤ ∑ x, toRatVec ↑x
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (setoid G f) (Structure.Sigma.mk f j ((f i j hij) x)) (Structure.Sigma.mk f i x)

Tactic:
]

Goal state after:
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
i j : ι
hij : i ≤ j
x : G i
⊢ (setoid G f) (Structure.Sigma.mk f j ((f i j hij) x)) (Structure.Sigma.mk f i x)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
hi : i ∈ Finset.univ
⊢ (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i ≤ hs.basis i

Tactic:
]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
hi : i ∈ Finset.univ
⊢ (hs.basis.repr (toRatVec x - toRatVec hs.base)) i • hs.basis i ≤ hs.basis i
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) =
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding

Tactic:
]

Goal state after:
case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) =
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case hb
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
hi : i ∈ Finset.univ
⊢ 0 ≤ toRatVec ↑i

Tactic:
]

Goal state after:
case hb
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
i : ↑hs.basisSet
hi : i ∈ Finset.univ
⊢ 0 ≤ toRatVec ↑i
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case h
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : (Substructure.closure L).toFun ↑A = S
i : ι
y : ↥A → G i
eq_y : (fun a ↦ ↑a) = fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧
⊢ (Substructure.closure L).toFun (⇑(of L ι G f i).toHom '' range y) = S

Tactic:
]

Goal state after:
case h
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : (Substructure.closure L).toFun ↑A = S
i : ι
y : ↥A → G i
eq_y : (fun a ↦ ↑a) = fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧
⊢ (Substructure.closure L).toFun (⇑(of L ι G f i).toHom '' range y) = S
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
n : ℕ
⊢ ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base + toRatVec (n • ↑i))) i⌋ =
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ + ↑n

Tactic:
]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
n : ℕ
⊢ ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base + toRatVec (n • ↑i))) i⌋ =
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ + ↑n
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.le_gf
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : g.dom ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion h)) =
      g.cod.subtype.comp g.toEquiv.toEmbedding

Tactic:
]

Goal state after:
case refl.le_gf
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : g.dom ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion h)) =
      g.cod.subtype.comp g.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
f : (ι → ℕ) → ℕ
x : ι → ℕ
i : ↑hs.basisSet
⊢ ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base + toRatVec (∑ i, f ↑↑i • ↑↑i))) i⌋ =
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ + ↑(f ↑i)

Tactic:
]

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
f : (ι → ℕ) → ℕ
x : ι → ℕ
i : ↑hs.basisSet
⊢ ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base + toRatVec (∑ i, f ↑↑i • ↑↑i))) i⌋ =
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) i⌋ + ↑(f ↑i)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case h
L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : (Substructure.closure L).toFun ↑A = S
i : ι
y : ↥A → G i
eq_y : (fun a ↦ ↑a) = fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧
⊢ S = S

Tactic:
]

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
⊢ ∃ i T, Substructure.map (of L ι G f i).toHom T = S

Tactic:
let ⟨A, A_closure⟩ := S_fg
  let ⟨i, y, eq_y⟩ := exists_quotient_mk'_sigma_mk'_eq G _ (fun a : A ↦ a.1)
  use i
  use Substructure.closure L (range y)
  rw [Substructure.map_closure]
  simp only [Embedding.coe_toHom, of_apply]
  rw [← image_univ, image_image, image_univ, ← eq_y,
    Subtype.range_coe_subtype, Finset.setOfPred_mem, A_closure]

Goal state after: