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

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
⊢ IsSlice {x | x ∈ s ∧ x i = a}

Tactic:
intro x

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Add (M i)
s : Set ((i : ι) → M i)
hs : IsSlice s
i : ι
a : M i
x : (i : ι) → M i
⊢ x ∈ {x | x ∈ s ∧ x i = a} →
    ∀ (b c : (i : ι) → M i),
      x + b ∈ {x | x ∈ s ∧ x i = a} → x + c ∈ {x | x ∈ s ∧ x i = a} → x + b + c ∈ {x | x ∈ s ∧ x i = a}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
⊢ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y

Tactic:
intro x

Goal state after:
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
x : M
⊢ x ∈ s → ∀ y ∈ s, x ≤ y → g x ≤ g y
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
⊢ ∀ x ∈ f a, ∀ (y : M), x + y ∈ f a → y ∈ f a

Tactic:
intro x

Goal state after:
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
⊢ x ∈ f a → ∀ (y : M), x + y ∈ f a → y ∈ f a
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α n
⊢ IsSemilinearSet {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}

Tactic:
have := Fintype.ofFinite α

Goal state after:
α : Type u_1
A : Set ℕ
inst✝ : Finite α
n : ℕ
φ : presburger[[↑A]].BoundedFormula α n
this : Fintype α
⊢ IsSemilinearSet {v | φ.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)}
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀' φ ⇔[T] ∀' ψ

Tactic:
simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_all]

Goal state after:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M),
    (∀ (a : ↑M), φ.Realize v (Fin.snoc xs a)) ↔ ∀ (a : ↑M), ψ.Realize v (Fin.snoc xs a)
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ ↑t ⊆ range ⇑f

Tactic:
intro x

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
⊢ x ∈ ↑t → x ∈ range ⇑f
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : (closure L).toFun t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
⊢ t ⊆ range ⇑f

Tactic:
intro x

Goal state after:
L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
t : Set N
h1 : t.Countable
h2 : (closure L).toFun t = Substructure.map f.toHom s
hf : Function.Injective ⇑f.toHom
x : N
⊢ x ∈ t → x ∈ range ⇑f
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := ⋯
f f' : M →[L] N
h : g f = g f'
⊢ EqOn (⇑f) (⇑f') S

Tactic:
intro x

Goal state after:
L : Language
M : Type u_1
inst✝² : L.Structure M
N : Type u_2
inst✝¹ : L.Structure N
inst✝ : Countable N
h✝ : FG L M
S : Set M
finite_S : S.Finite
closure_S : (closure L).toFun S = ⊤
g : (M →[L] N) → ↑S → N := fun f ↦ ⇑f ∘ Subtype.val
f f' : M →[L] N
h : g f = g f'
x : M
⊢ x ∈ S → f x = f' x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
t : Finset ι
ih : ∀ t_1 ⊂ t, ∀ {s : Set (ι → ℕ)}, IsSlice s → ∀ (a : ι → ℕ), (∀ x ∈ s, ∀ i ∉ t_1, x i = a i) → IsSemilinearSet s
s : Set (ι → ℕ)
hs : IsSlice s
a : ι → ℕ
ht : ∀ x ∈ s, ∀ i ∉ t, x i = a i
hs' : s.Nonempty
x : ι → ℕ
hx : x ∈ s
hx' : IsSemilinearSet {y | y ∈ s ∧ x ≤ y}
⊢ s = {y | y ∈ s ∧ x ≤ y} ∪ ⋃ i ∈ t, ⋃ j ∈ Finset.range (x i), {y | y ∈ s ∧ y i = j}

Tactic:
ext y
    simp only [Finset.mem_range, mem_union, mem_ofPred_eq, mem_iUnion, Pi.le_def]
    grind

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

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Finite ι
F : Type u_5
G : Type u_6
inst✝³ : FunLike F (ι → ℕ) M
inst✝² : AddMonoidHomClass F (ι → ℕ) M
inst✝¹ : FunLike G (ι → ℕ) M
inst✝ : AddMonoidHomClass G (ι → ℕ) M
a b : M
f : F
g : G
⊢ IsSlice {x | a + f x = b + g x}

Tactic:
intro x

Goal state after:
M : Type u_1
ι : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Finite ι
F : Type u_5
G : Type u_6
inst✝³ : FunLike F (ι → ℕ) M
inst✝² : AddMonoidHomClass F (ι → ℕ) M
inst✝¹ : FunLike G (ι → ℕ) M
inst✝ : AddMonoidHomClass G (ι → ℕ) M
a b : M
f : F
g : G
x : ι → ℕ
⊢ x ∈ {x | a + f x = b + g x} →
    ∀ (b_1 c : ι → ℕ),
      x + b_1 ∈ {x | a + f x = b + g x} → x + c ∈ {x | a + f x = b + g x} → x + b_1 + c ∈ {x | a + f x = b + g x}
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
T : L.Theory
hT : T.IsUniversal
N : Type u_1
inst✝¹ : L.Structure N
inst✝ : N ⊨ T
f : M ↪[L] N
⊢ M ⊨ T

Tactic:
by
  simp only [model_iff]
  refine fun φ hφ => (hT.isUniversal_of_mem hφ).realize_embedding f (?_)
  rw [Subsingleton.elim (f ∘ default) default, Subsingleton.elim (f ∘ default) default]
  exact Theory.realize_sentence_of_mem T hφ

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✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : IsDirectedOrder ι
x✝⁴ x✝³ x✝² : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ι
x : G i
j : ι
y : G j
x✝¹ :
  match ⟨i, x⟩ with
  | ⟨i, x⟩ =>
    match ⟨j, y⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
k : ι
z : G k
x✝ :
  match ⟨j, y⟩ with
  | ⟨i, x⟩ =>
    match ⟨k, z⟩ with
    | ⟨j, y⟩ => ∃ k, ∃ (ik : i ≤ k) (jk : j ≤ k), (f i k ik) x = (f j k jk) y
ij : ι
hiij : i ≤ ij
hjij : j ≤ ij
hij : (f i ij hiij) x = (f j ij hjij) y
jk : ι
hjjk : j ≤ jk
hkjk : k ≤ jk
hjk : (f j jk hjjk) y = (f k jk hkjk) z
ijk : ι
hijijk : ij ≤ ijk
hjkijk : jk ≤ ijk
⊢ (f j ijk ⋯) y = (f k ijk ⋯) z

Tactic:
rw [← DirectedSystem.map_map _ hkjk hjkijk, ← hjk, DirectedSystem.map_map]

Goal state after:
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
h : f ≤ g
⊢ ∀ (x : ↥f.dom), (inclusion ⋯) (f.toEquiv x) = g.toEquiv ((inclusion ⋯) x)

Tactic:
intro x

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ (inclusion ⋯) (f.toEquiv x) = g.toEquiv ((inclusion ⋯) 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 : M ≃ₚ[L] N
hfg : f ≤ g
⊢ ∀ (x : ↥f.symm.dom), (inclusion ⋯) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion ⋯) x)

Tactic:
intro x

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
⊢ (inclusion ⋯) (f.symm.toEquiv x) = g.symm.toEquiv ((inclusion ⋯) 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 : M ≃ₚ[L] N
g : N ≃ₚ[L] M
⊢ f.symm ≤ g → f ≤ g.symm

Tactic:
by intro h; rw [← f.symm_symm]; exact monotone_symm h

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
⊢ hs.fundamentalDomain ⊆ Iic (hs.base + ∑ i, ↑i)

Tactic:
intro x

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
this : Fintype ι
x : ι → ℕ
⊢ x ∈ hs.fundamentalDomain → x ∈ Iic (hs.base + ∑ i, ↑i)
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case mp
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_eq : { dom := dom_f, cod := cod_f, toEquiv := equiv_f } = g
⊢ ∃ (h_dom : { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom = g.dom),
    ∀ (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, ⋯⟩)

Tactic:
cases h_eq

Goal state after:
case mp.refl
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure 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 = { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom),
    ∀ (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⟩) =
        { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.cod.subtype
          ({ dom := dom_f, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, ⋯⟩)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| ∑ x_1,
    (⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋.toNat • toRatVec ↑x_1 -
      (-⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋).toNat • toRatVec ↑x_1)

Tactic:
2,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| fun x_1 ↦
    ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋.toNat • toRatVec ↑x_1 -
      (-⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋).toNat • toRatVec ↑x_1
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| toRatVec x - ∑ x_1, ((hs.floor x x_1).toNat • toRatVec ↑x_1 - (-hs.floor x x_1).toNat • toRatVec ↑x_1)

Tactic:
2,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| ∑ x_1, ((hs.floor x x_1).toNat • toRatVec ↑x_1 - (-hs.floor x x_1).toNat • toRatVec ↑x_1)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| ∑ x_1, ((hs.floor x x_1).toNat • toRatVec ↑x_1 - (-hs.floor x x_1).toNat • toRatVec ↑x_1)

Tactic:
2,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| fun x_1 ↦ (hs.floor x x_1).toNat • toRatVec ↑x_1 - (-hs.floor x x_1).toNat • toRatVec ↑x_1
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
2,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| ∑ x_1,
    (Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1) • toRatVec ↑x_1 +
      ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋ • toRatVec ↑x_1)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| ∑ x_1,
    (Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1) • toRatVec ↑x_1 +
      ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋ • toRatVec ↑x_1)

Tactic:
2,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
| fun x_1 ↦
    Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1) • toRatVec ↑x_1 +
      ⌊(hs.basis.repr (toRatVec x - toRatVec hs.base)) x_1⌋ • toRatVec ↑x_1
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 : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x ↦ H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
⊢ X ⊆ ↑F.dom

Tactic:
intro x

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝¹ : Countable ↑X
x✝ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x ↦ H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x : M
⊢ x ∈ X → x ∈ ↑F.dom
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 ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
⊢ Function.Surjective ⇑F

Tactic:
intro x

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 ι
P : Type u₁
inst✝² : L.Structure P
g✝ : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g✝ j) ((f i j hij) x) = (g✝ i) x
G' : ι → Type w'
inst✝¹ : (i : ι) → L.Structure (G' i)
f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j
g : (i : ι) → G i ≃[L] G' i
inst✝ : DirectedSystem G' fun i j h ↦ ⇑(f' i j h)
H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)
U : (i : ι) → G i ↪[L] DirectLimit G' f' := fun i ↦ (of L ι G' f' i).comp (g i).toEmbedding
F : DirectLimit G f ↪[L] DirectLimit G' f' := lift L ι G f U ⋯
x : DirectLimit G' f'
⊢ ∃ a, F a = x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
2,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
| ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
2,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : x ∈ hs.fundamentalDomain
| fun i ↦ Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) 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
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
⊢ X ⊆ ↑F.dom

Tactic:
intro x

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
ext_dom : L.IsExtensionPair M N
ext_cod : L.IsExtensionPair N M
X : Set M
X_count : X.Countable
X_gen : (closure L).toFun X = ⊤
Y : Set N
Y_count : Y.Countable
Y_gen : (closure L).toFun Y = ⊤
x✝³ : Countable ↑X
x✝² : Encodable ↑X
x✝¹ : Countable ↑Y
x✝ : Encodable ↑Y
D : ↑X ⊕ ↑Y → Order.Cofinal (L.FGEquiv M N) :=
  fun p ↦ Sum.recOn p (fun x ↦ ext_dom.definedAtLeft ↑x) fun y ↦ ext_cod.definedAtRight ↑y
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x : M
⊢ x ∈ X → x ∈ ↑F.dom
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✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
⊢ ∀ (x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯),
    ∃ y, (liftInclusion S) y = (liftInclusion S) x

Tactic:
intro x

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✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
x : DirectLimit (fun i ↦ ↥(S i)) fun x x_1 h ↦ Substructure.inclusion ⋯
⊢ ∃ y, (liftInclusion S) y = (liftInclusion S) x
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
⊢ ↑s ⊆ ↑(DirectLimit.of L ι G f i).toHom.range

Tactic:
intro x

Goal state after:
case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
x : DirectLimit G f
⊢ x ∈ ↑s → x ∈ ↑(DirectLimit.of L ι G f i).toHom.range
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
⊢ ∀ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}), ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
f : PartialIso α β
a : α
h : ¬∃ b, (a, b) ∈ ↑f
x : β
⊢ x ∈ Finset.image Prod.snd ({p ∈ ↑f | p.1 < a}) → ∀ y ∈ Finset.image Prod.snd ({p ∈ ↑f | a < p.1}), x < y
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case refine_2.refine_1
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ ∀ (T0 : Finset L[[α]].Sentence), ↑T0 ⊆ {φ | T.typesWith φ ∈ F} → IsSatisfiable ↑T0

Tactic:
intro x

Goal state after:
case refine_2.refine_1
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
x : Finset L[[α]].Sentence
⊢ ↑x ⊆ {φ | T.typesWith φ ∈ F} → IsSatisfiable ↑x
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
⊢ sumInv {p, q, r} = (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹

Tactic:
by
  simp only [sumInv, insert_eq_cons, add_assoc, map_cons, sum_cons,
    map_singleton, sum_singleton]

Goal state after: