ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<GOAL>(FirstOrder.Language.Substructure.closure L).closed ↑S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>s : Set M<GOAL>(FirstOrder.Language.Substructure.closure L).toFun s ≤ S ↔ s ⊆ ↑S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s t : Set M<VAR>h : s ⊆ t<GOAL>(FirstOrder.Language.Substructure.closure L).toFun s ≤ (FirstOrder.Language.Substructure.closure L).toFun t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>s : Set M<VAR>h₁ : s ⊆ ↑S<VAR>h₂ : S ≤ (FirstOrder.Language.Substructure.closure L).toFun s<GOAL>(FirstOrder.Language.Substructure.closure L).toFun s = S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<GOAL>↑((FirstOrder.Language.Substructure.closure L).toFun s) = Set.range (FirstOrder.Language.Term.realize Subtype.val)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<VAR>x : M<GOAL>x ∈ (FirstOrder.Language.Substructure.closure L).toFun s ↔ ∃ t, FirstOrder.Language.Term.realize Subtype.val t = x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<GOAL>Cardinal.lift.{max u w, w} (Cardinal.mk ↥((FirstOrder.Language.Substructure.closure L).toFun s)) ≤ Cardinal.mk (L.Term ↑s)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<GOAL>Cardinal.lift.{u, w} (Cardinal.mk ↥((FirstOrder.Language.Substructure.closure L).toFun s)) ≤ max Cardinal.aleph0 (Cardinal.lift.{u, w} (Cardinal.mk ↑s) + Cardinal.lift.{w, u} (Cardinal.mk ((i : ℕ) × L.Functions i)))
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<VAR>Countable ((l : ℕ) × L.Functions l)<VAR>h : s.Countable<GOAL>Countable ↥((FirstOrder.Language.Substructure.closure L).toFun s)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<VAR>p : M → Prop<VAR>x : M<VAR>h : x ∈ (FirstOrder.Language.Substructure.closure L).toFun s<VAR>Hs : ∀ x ∈ s, p x<VAR>Hfun : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f (setOf p)<GOAL>p x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : (FirstOrder.Language.Substructure.closure L).toFun s = ⊤<VAR>Hs : ∀ x ∈ s, p x<VAR>Hfun : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f (setOf p)<GOAL>p x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<GOAL>(FirstOrder.Language.Substructure.closure L).toFun ↑S = S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>(FirstOrder.Language.Substructure.closure L).toFun ∅ = ⊥
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>(FirstOrder.Language.Substructure.closure L).toFun Set.univ = ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s t : Set M<GOAL>(FirstOrder.Language.Substructure.closure L).toFun (s ∪ t) = (FirstOrder.Language.Substructure.closure L).toFun s ⊔ (FirstOrder.Language.Substructure.closure L).toFun t
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>ι : Sort u_3<VAR>s : ι → Set M<GOAL>(FirstOrder.Language.Substructure.closure L).toFun (⋃ i, s i) = ⨆ i, (FirstOrder.Language.Substructure.closure L).toFun (s i)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Hom M N<VAR>S : L.Substructure N<GOAL>↑(FirstOrder.Language.Substructure.comap φ S) = ⇑φ ⁻¹' ↑S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>S : L.Substructure N<VAR>f : L.Hom M N<VAR>x : M<GOAL>x ∈ FirstOrder.Language.Substructure.comap f S ↔ f x ∈ S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>L.Structure P<VAR>S : L.Substructure P<VAR>g : L.Hom N P<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.comap g S) = FirstOrder.Language.Substructure.comap (g.comp f) S
<VAR>L : FirstOrder.Language<VAR>P : Type u_2<VAR>L.Structure P<VAR>S : L.Substructure P<GOAL>FirstOrder.Language.Substructure.comap (FirstOrder.Language.Hom.id L P) S = S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : L.Hom M N<VAR>S : L.Substructure M<GOAL>↑(FirstOrder.Language.Substructure.map φ S) = ⇑φ '' ↑S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>S : L.Substructure M<VAR>y : N<GOAL>y ∈ FirstOrder.Language.Substructure.map f S ↔ ∃ x ∈ S, f x = y
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>S : L.Substructure M<VAR>x : M<VAR>hx : x ∈ S<GOAL>f x ∈ FirstOrder.Language.Substructure.map f S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>S : L.Substructure M<VAR>x : ↥S<GOAL>f ↑x ∈ FirstOrder.Language.Substructure.map f S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>L.Structure P<VAR>S : L.Substructure M<VAR>g : L.Hom N P<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.map g (FirstOrder.Language.Substructure.map f S) = FirstOrder.Language.Substructure.map (g.comp f) S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>S : L.Substructure M<VAR>T : L.Substructure N<GOAL>FirstOrder.Language.Substructure.map f S ≤ T ↔ S ≤ FirstOrder.Language.Substructure.comap f T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>GaloisConnection (FirstOrder.Language.Substructure.map f) (FirstOrder.Language.Substructure.comap f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>S : L.Substructure M<VAR>T : L.Substructure N<VAR>f : L.Hom M N<GOAL>S ≤ FirstOrder.Language.Substructure.comap f T → FirstOrder.Language.Substructure.map f S ≤ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>S : L.Substructure M<VAR>T : L.Substructure N<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.map f S ≤ T → S ≤ FirstOrder.Language.Substructure.comap f T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>S : L.Substructure M<VAR>f : L.Hom M N<GOAL>S ≤ FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>S : L.Substructure N<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S) ≤ S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>Monotone (FirstOrder.Language.Substructure.map f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>Monotone (FirstOrder.Language.Substructure.comap f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>S : L.Substructure M<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S)) = FirstOrder.Language.Substructure.map f S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>S : L.Substructure N<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S)) = FirstOrder.Language.Substructure.comap f S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>S T : L.Substructure M<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.map f (S ⊔ T) = FirstOrder.Language.Substructure.map f S ⊔ FirstOrder.Language.Substructure.map f T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>ι : Sort u_3<VAR>f : L.Hom M N<VAR>s : ι → L.Substructure M<GOAL>FirstOrder.Language.Substructure.map f (iSup s) = ⨆ i, FirstOrder.Language.Substructure.map f (s i)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>S T : L.Substructure N<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.comap f (S ⊓ T) = FirstOrder.Language.Substructure.comap f S ⊓ FirstOrder.Language.Substructure.comap f T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>ι : Sort u_3<VAR>f : L.Hom M N<VAR>s : ι → L.Substructure N<GOAL>FirstOrder.Language.Substructure.comap f (iInf s) = ⨅ i, FirstOrder.Language.Substructure.comap f (s i)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.map f ⊥ = ⊥
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>FirstOrder.Language.Substructure.comap f ⊤ = ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<GOAL>FirstOrder.Language.Substructure.map (FirstOrder.Language.Hom.id L M) S = S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>s : Set M<GOAL>FirstOrder.Language.Substructure.map f ((FirstOrder.Language.Substructure.closure L).toFun s) = (FirstOrder.Language.Substructure.closure L).toFun (⇑f '' s)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>s : Set M<VAR>f : L.Hom M N<GOAL>(FirstOrder.Language.Substructure.closure L).toFun (⇑f '' s) = FirstOrder.Language.Substructure.map f ((FirstOrder.Language.Substructure.closure L).toFun s)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<VAR>S : L.Substructure M<GOAL>FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S) = S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Surjective (FirstOrder.Language.Substructure.comap f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective (FirstOrder.Language.Substructure.map f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<VAR>S T : L.Substructure M<GOAL>FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S ⊓ FirstOrder.Language.Substructure.map f T) = S ⊓ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>ι : Type u_3<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<VAR>S : ι → L.Substructure M<GOAL>FirstOrder.Language.Substructure.comap f (⨅ i, FirstOrder.Language.Substructure.map f (S i)) = iInf S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<VAR>S T : L.Substructure M<GOAL>FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S ⊔ FirstOrder.Language.Substructure.map f T) = S ⊔ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>ι : Type u_3<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<VAR>S : ι → L.Substructure M<GOAL>FirstOrder.Language.Substructure.comap f (⨆ i, FirstOrder.Language.Substructure.map f (S i)) = iSup S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<VAR>S T : L.Substructure M<GOAL>FirstOrder.Language.Substructure.map f S ≤ FirstOrder.Language.Substructure.map f T ↔ S ≤ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Injective ⇑f<GOAL>StrictMono (FirstOrder.Language.Substructure.map f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Surjective ⇑f<VAR>S : L.Substructure N<GOAL>FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S) = S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective (FirstOrder.Language.Substructure.map f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective (FirstOrder.Language.Substructure.comap f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Surjective ⇑f<VAR>S T : L.Substructure N<GOAL>FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S ⊓ FirstOrder.Language.Substructure.comap f T) = S ⊓ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>ι : Type u_3<VAR>f : L.Hom M N<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → L.Substructure N<GOAL>FirstOrder.Language.Substructure.map f (⨅ i, FirstOrder.Language.Substructure.comap f (S i)) = iInf S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Surjective ⇑f<VAR>S T : L.Substructure N<GOAL>FirstOrder.Language.Substructure.map f (FirstOrder.Language.Substructure.comap f S ⊔ FirstOrder.Language.Substructure.comap f T) = S ⊔ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>ι : Type u_3<VAR>f : L.Hom M N<VAR>hf : Function.Surjective ⇑f<VAR>S : ι → L.Substructure N<GOAL>FirstOrder.Language.Substructure.map f (⨆ i, FirstOrder.Language.Substructure.comap f (S i)) = iSup S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Surjective ⇑f<VAR>S T : L.Substructure N<GOAL>FirstOrder.Language.Substructure.comap f S ≤ FirstOrder.Language.Substructure.comap f T ↔ S ≤ T
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>hf : Function.Surjective ⇑f<GOAL>StrictMono (FirstOrder.Language.Substructure.comap f)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<GOAL>⇑S.subtype = Subtype.val
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>⇑FirstOrder.Language.Substructure.topEquiv = Subtype.val
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u_3<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → ↥⊤<VAR>xs : Fin n → ↥⊤<GOAL>φ.Realize v xs ↔ φ.Realize (Subtype.val ∘ v) (Subtype.val ∘ xs)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u_3<VAR>φ : L.Formula α<VAR>v : α → ↥⊤<GOAL>φ.Realize v ↔ φ.Realize (Subtype.val ∘ v)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>s : Set M<VAR>p : (x : M) → x ∈ (FirstOrder.Language.Substructure.closure L).toFun s → Prop<VAR>Hs : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>Hfun : ∀ {n : ℕ} (f : L.Functions n), FirstOrder.Language.ClosedUnder f {x | ∃ (hx : x ∈ (FirstOrder.Language.Substructure.closure L).toFun s), p x hx}<VAR>x : M<VAR>hx : x ∈ (FirstOrder.Language.Substructure.closure L).toFun s<GOAL>p x hx
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>L' : FirstOrder.Language<VAR>L'.Structure M<VAR>φ : L →ᴸ L'<VAR>φ.IsExpansionOn M<VAR>x : M<VAR>S : L'.Substructure M<GOAL>x ∈ φ.substructureReduct S ↔ x ∈ S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>L' : FirstOrder.Language<VAR>L'.Structure M<VAR>φ : L →ᴸ L'<VAR>φ.IsExpansionOn M<VAR>S : L'.Substructure M<GOAL>↑(φ.substructureReduct S) = ↑S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>A : Set M<VAR>h : A ⊆ ↑S<VAR>x : M<GOAL>x ∈ S.withConstants h ↔ x ∈ S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>A : Set M<VAR>h : A ⊆ ↑S<GOAL>↑(S.withConstants h) = ↑S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>A : Set M<VAR>h : A ⊆ ↑S<GOAL>(L.lhomWithConstants ↑A).substructureReduct (S.withConstants h) = S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A s : Set M<GOAL>A ⊆ ↑((FirstOrder.Language.Substructure.closure (L.withConstants ↑A)).toFun s)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A s : Set M<GOAL>(FirstOrder.Language.Substructure.closure (L.withConstants ↑A)).toFun s = ((FirstOrder.Language.Substructure.closure L).toFun (A ∪ s)).withConstants ⋯
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>p : L.Substructure M<GOAL>∀ (a : ↥p), (f.domRestrict p) a = f ↑a
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>p : L.Substructure N<VAR>f : L.Hom M N<VAR>h : ∀ (c : M), f c ∈ p<VAR>c : M<GOAL>↑((FirstOrder.Language.Hom.codRestrict p f h) c) = f c
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>L.Structure P<VAR>f : L.Hom M N<VAR>g : L.Hom N P<VAR>p : L.Substructure P<VAR>h : ∀ (b : N), g b ∈ p<GOAL>(FirstOrder.Language.Hom.codRestrict p g h).comp f = FirstOrder.Language.Hom.codRestrict p (g.comp f) ⋯
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>p : L.Substructure N<VAR>h : ∀ (b : M), f b ∈ p<GOAL>p.subtype.toHom.comp (FirstOrder.Language.Hom.codRestrict p f h) = f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>↑f.range = Set.range ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>x : N<GOAL>x ∈ f.range ↔ ∃ y, f y = x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>f.range = FirstOrder.Language.Substructure.map f ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>x : M<GOAL>f x ∈ f.range
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>(FirstOrder.Language.Hom.id L M).range = ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>L.Structure P<VAR>f : L.Hom M N<VAR>g : L.Hom N P<GOAL>(g.comp f).range = FirstOrder.Language.Substructure.map g f.range
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>L.Structure P<VAR>f : L.Hom M N<VAR>g : L.Hom N P<GOAL>(g.comp f).range ≤ g.range
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>p : L.Substructure N<GOAL>f.range ≤ p ↔ FirstOrder.Language.Substructure.comap f p = ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Hom M N<VAR>p : L.Substructure M<GOAL>FirstOrder.Language.Substructure.map f p ≤ f.range
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : L.Hom M N<VAR>s : Set M<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑((FirstOrder.Language.Substructure.closure L).toFun s)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : L.Hom M N<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>s : Set M<VAR>hs : (FirstOrder.Language.Substructure.closure L).toFun s = ⊤<VAR>f g : L.Hom M N<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<VAR>p : L.Substructure M<VAR>x : ↥p<GOAL>(f.domRestrict p) x = f ↑x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>p : L.Substructure N<VAR>f : L.Embedding M N<VAR>h : ∀ (c : M), f c ∈ p<VAR>x : M<GOAL>↑((FirstOrder.Language.Embedding.codRestrict p f h) x) = f x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>p : L.Substructure N<VAR>f : L.Embedding M N<VAR>h : ∀ (c : M), f c ∈ p<VAR>x : M<GOAL>(FirstOrder.Language.Embedding.codRestrict p f h) x = ⟨f x, ⋯⟩
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>L.Structure P<VAR>f : L.Embedding M N<VAR>g : L.Embedding N P<VAR>p : L.Substructure P<VAR>h : ∀ (b : N), g b ∈ p<GOAL>(FirstOrder.Language.Embedding.codRestrict p g h).comp f = FirstOrder.Language.Embedding.codRestrict p (g.comp f) ⋯
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<VAR>p : L.Substructure N<VAR>h : ∀ (b : M), f b ∈ p<GOAL>p.subtype.comp (FirstOrder.Language.Embedding.codRestrict p f h) = f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<VAR>p : L.Substructure M<VAR>x : ↥p<GOAL>↑((f.substructureEquivMap p) x) = f ↑x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<VAR>s : L.Substructure M<GOAL>(FirstOrder.Language.Substructure.map f.toHom s).subtype.comp (f.substructureEquivMap s).toEmbedding = f.comp s.subtype
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<VAR>x : M<GOAL>↑(f.equivRange x) = f x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Embedding M N<GOAL>f.toHom.range.subtype.comp f.equivRange.toEmbedding = f
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type u_1<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>f.toHom.range = ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<GOAL>FirstOrder.Language.Substructure.inclusion ⋯ = FirstOrder.Language.Embedding.refl L ↥S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S T : L.Substructure M<VAR>h : S ≤ T<GOAL>⇑(FirstOrder.Language.Substructure.inclusion h) = Set.inclusion h
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>S : L.Substructure M<GOAL>S.subtype.toHom.range = S
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>i : ι<VAR>x : G i<VAR>h : i ≤ i<GOAL>(f i i h) x = x
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>i j k : ι<VAR>hij : i ≤ j<VAR>hjk : j ≤ k<VAR>x : G i<GOAL>(f j k hjk) ((f i j hij) x) = (f i k ⋯) x
<VAR>L : FirstOrder.Language<VAR>G' : ℕ → Type w<VAR>(i : ℕ) → L.Structure (G' i)<VAR>f' : (n : ℕ) → G' n ↪[L] G' (n + 1)<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>⇑(FirstOrder.Language.DirectedSystem.natLERec f' m n h) = fun a => Nat.leRecOn h (fun k => ⇑(f' k)) a
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>α : Type u_1<VAR>i : ι<VAR>x : α → G i<GOAL>FirstOrder.Language.DirectLimit.unify f (fun a => FirstOrder.Language.Structure.Sigma.mk f i (x a)) i ⋯ = x