ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>f.symm.toHom.comp f.toHom = FirstOrder.Language.Hom.id L M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>f : L.Equiv M N<GOAL>f.toHom.comp f.symm.toHom = FirstOrder.Language.Hom.id L N
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>f : L.Equiv M N<VAR>g : L.Equiv N P<GOAL>(g.comp f).symm = f.symm.comp g.symm
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>h : L.Equiv M N<GOAL>Function.Injective fun f => f.comp h
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>N : Type w'<VAR>L.Structure M<VAR>L.Structure N<VAR>P : Type u_1<VAR>L.Structure P<VAR>h : L.Equiv M N<VAR>f g : L.Equiv N P<GOAL>f.comp h = g.comp h ↔ f = g
<VAR>L₁ : FirstOrder.Language<VAR>L₂ : FirstOrder.Language<VAR>S : Type u_3<VAR>L₁.Structure S<VAR>L₂.Structure S<VAR>n : ℕ<VAR>f : L₁.Functions n<GOAL>FirstOrder.Language.Structure.funMap (Sum.inl f) = FirstOrder.Language.Structure.funMap f
<VAR>L₁ : FirstOrder.Language<VAR>L₂ : FirstOrder.Language<VAR>S : Type u_3<VAR>L₁.Structure S<VAR>L₂.Structure S<VAR>n : ℕ<VAR>f : L₂.Functions n<GOAL>FirstOrder.Language.Structure.funMap (Sum.inr f) = FirstOrder.Language.Structure.funMap f
<VAR>L₁ : FirstOrder.Language<VAR>L₂ : FirstOrder.Language<VAR>S : Type u_3<VAR>L₁.Structure S<VAR>L₂.Structure S<VAR>n : ℕ<VAR>R : L₁.Relations n<GOAL>FirstOrder.Language.Structure.RelMap (Sum.inl R) = FirstOrder.Language.Structure.RelMap R
<VAR>L₁ : FirstOrder.Language<VAR>L₂ : FirstOrder.Language<VAR>S : Type u_3<VAR>L₁.Structure S<VAR>L₂.Structure S<VAR>n : ℕ<VAR>R : L₂.Relations n<GOAL>FirstOrder.Language.Structure.RelMap (Sum.inr R) = FirstOrder.Language.Structure.RelMap R
<VAR>M : Type w<VAR>N : Type w'<VAR>FirstOrder.Language.empty.Structure M<VAR>FirstOrder.Language.empty.Structure N<GOAL>Nonempty (FirstOrder.Language.empty.Embedding M N) ↔ Cardinal.lift.{w', w} #M ≤ Cardinal.lift.{w, w'} #N
<VAR>M : Type w<VAR>N : Type w'<VAR>FirstOrder.Language.empty.Structure M<VAR>FirstOrder.Language.empty.Structure N<GOAL>Nonempty (FirstOrder.Language.empty.Equiv M N) ↔ Cardinal.lift.{w', w} #M = Cardinal.lift.{w, w'} #N
<VAR>M : Type w<VAR>N : Type w'<VAR>f : M → N<GOAL>∀ (a : M), (Function.emptyHom f) a = f a
<VAR>M : Type w<VAR>N : Type w'<VAR>f : M ↪ N<GOAL>⇑(Embedding.empty f) = ⇑f
<VAR>M : Type w<VAR>N : Type w'<VAR>f : M ↪ N<GOAL>(Embedding.empty f).toEmbedding = f
<VAR>M : Type w<VAR>N : Type w'<VAR>f : M ≃ N<GOAL>⇑f.empty = ⇑f
<VAR>M : Type w<VAR>N : Type w'<VAR>f : M ≃ N<GOAL>f.empty.toEquiv = f
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>e : M ≃ N<GOAL>∀ {n : ℕ} (f : L.Functions n) (x : Fin n → N), FirstOrder.Language.Structure.funMap f x = e (FirstOrder.Language.Structure.funMap f (⇑e.symm ∘ x))
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>e : M ≃ N<GOAL>∀ {n : ℕ} (r : L.Relations n) (x : Fin n → N), FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r (⇑e.symm ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>e : M ≃ N<GOAL>e.inducedStructureEquiv.toEquiv = e
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>e : M ≃ N<GOAL>⇑e.inducedStructureEquiv = ⇑e
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>e : M ≃ N<GOAL>⇑e.inducedStructureEquiv.symm = ⇑e.symm
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>self : FirstOrder.Language.IsFraisse K<VAR>M N : CategoryTheory.Bundled L.Structure<GOAL>Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>self : FirstOrder.Language.IsFraisse K<GOAL>FirstOrder.Language.Amalgamation K
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>self : FirstOrder.Language.IsFraisse K<VAR>M : CategoryTheory.Bundled L.Structure<GOAL>M ∈ K → FirstOrder.Language.Structure.FG L ↑M
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>self : FirstOrder.Language.IsFraisse K<GOAL>(Quotient.mk' '' K).Countable
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>self : FirstOrder.Language.IsFraisse K<GOAL>FirstOrder.Language.JointEmbedding K
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>self : FirstOrder.Language.IsFraisse K<GOAL>K.Nonempty
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>self : FirstOrder.Language.IsFraisse K<GOAL>FirstOrder.Language.Hereditary K
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>N P : CategoryTheory.Bundled L.Structure<VAR>h : Nonempty (↑N ≃[L] ↑P)<GOAL>N ∈ L.age M ↔ P ∈ L.age M
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>N : Type w<VAR>L.Structure N<VAR>MN : M ↪[L] N<GOAL>L.age M ⊆ L.age N
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>N : Type w<VAR>L.Structure N<VAR>MN : M ≃[L] N<GOAL>L.age M = L.age N
<VAR>L : FirstOrder.Language<VAR>M N : CategoryTheory.Bundled L.Structure<VAR>h : FirstOrder.Language.Structure.FG L ↑M<VAR>MN : Nonempty (↑M ≃[L] ↑N)<GOAL>N ∈ L.age ↑M
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>h : FirstOrder.Language.Hereditary K<VAR>fg : ∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M<VAR>M N : CategoryTheory.Bundled L.Structure<VAR>hn : Nonempty (↑M ≃[L] ↑N)<GOAL>M ∈ K ↔ N ∈ K
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>(L.age M).Nonempty
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>FirstOrder.Language.Hereditary (L.age M)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<GOAL>FirstOrder.Language.JointEmbedding (L.age M)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>h : Countable M<GOAL>(Quotient.mk' '' L.age M).Countable
<VAR>L : FirstOrder.Language<VAR>ι : Type w<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>G : ι → Type (max w 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)<GOAL>L.age (FirstOrder.Language.DirectLimit G f) = ⋃ i, L.age (G i)
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>hn : K.Nonempty<VAR>h : ∀ (M N : CategoryTheory.Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)<VAR>hc : (Quotient.mk' '' K).Countable<VAR>fg : ∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M<VAR>hp : FirstOrder.Language.Hereditary K<VAR>jep : FirstOrder.Language.JointEmbedding K<GOAL>∃ M, FirstOrder.Language.Structure.CG L ↑M ∧ L.age ↑M = K
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>Countable ((l : ℕ) × L.Functions l)<GOAL>(∃ M, Countable ↑M ∧ L.age ↑M = K) ↔ K.Nonempty ∧ (∀ (M N : CategoryTheory.Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧ (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, FirstOrder.Language.Structure.FG L ↑M) ∧ FirstOrder.Language.Hereditary K ∧ FirstOrder.Language.JointEmbedding K
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>M : Type w<VAR>L.Structure M<VAR>Countable ((l : ℕ) × L.Functions l)<VAR>Countable M<VAR>self : FirstOrder.Language.IsFraisseLimit K M<GOAL>L.IsUltrahomogeneous M
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>M : Type w<VAR>L.Structure M<VAR>Countable ((l : ℕ) × L.Functions l)<VAR>Countable M<VAR>self : FirstOrder.Language.IsFraisseLimit K M<GOAL>L.age M = K
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>h : L.IsUltrahomogeneous M<GOAL>FirstOrder.Language.Amalgamation (L.age M)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>Countable M<VAR>h : L.IsUltrahomogeneous M<GOAL>FirstOrder.Language.IsFraisse (L.age M)
<VAR>L : FirstOrder.Language<VAR>K : Set (CategoryTheory.Bundled L.Structure)<VAR>M : Type w<VAR>L.Structure M<VAR>Countable ((l : ℕ) × L.Functions l)<VAR>Countable M<VAR>h : FirstOrder.Language.IsFraisseLimit K M<GOAL>FirstOrder.Language.IsFraisse K
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>self : L.ElementarySubstructure M<GOAL>(↑self).IsElementary
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : L.ElementarySubstructure M<GOAL>(↑S).IsElementary
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : L.ElementarySubstructure M<GOAL>⇑S.subtype = Subtype.val
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>x : M<GOAL>x ∈ ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<GOAL>↑⊤ = Set.univ
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : L.ElementarySubstructure M<VAR>φ : L.Sentence<GOAL>↥S ⊨ φ ↔ M ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : L.ElementarySubstructure M<VAR>T : L.Theory<GOAL>↥S ⊨ T ↔ M ⊨ T
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : L.ElementarySubstructure M<GOAL>↥S ≅[L] M
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (a : M), φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)<GOAL>S.IsElementary
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : L.Substructure M<VAR>htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (a : M), φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)<GOAL>↑(S.toElementarySubstructure htv) = S
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>↑(NumberField.discr K) = Algebra.discr ℚ ⇑(NumberField.integralBasis K)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>NumberField.discr K ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>ι : Type u_2<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι ℤ (NumberField.RingOfIntegers K)<GOAL>Algebra.discr ℤ ⇑b = NumberField.discr K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>L : Type u_2<VAR>Field L<VAR>NumberField L<VAR>f : K ≃ₐ[ℚ] L<GOAL>NumberField.discr K = NumberField.discr L
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>MeasureTheory.volume (Zspan.fundamentalDomain (NumberField.mixedEmbedding.latticeBasis K)) = 2⁻¹ ^ NumberField.InfinitePlace.NrComplexPlaces K * ↑(NNReal.sqrt ‖NumberField.discr K‖₊)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ<GOAL>∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ ↑(FractionalIdeal.absNorm ↑I) * (4 / Real.pi) ^ NumberField.InfinitePlace.NrComplexPlaces K * ↑(FiniteDimensional.finrank ℚ K).factorial / ↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K * √|↑(NumberField.discr K)|
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (4 / Real.pi) ^ NumberField.InfinitePlace.NrComplexPlaces K * ↑(FiniteDimensional.finrank ℚ K).factorial / ↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K * √|↑(NumberField.discr K)|
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>h : 1 < FiniteDimensional.finrank ℚ K<GOAL>4 / 9 * (3 * Real.pi / 4) ^ FiniteDimensional.finrank ℚ K ≤ ↑|NumberField.discr K|
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>h : 1 < FiniteDimensional.finrank ℚ K<GOAL>2 < |NumberField.discr K|
<VAR>A : Type u_2<VAR>Field A<VAR>CharZero A<VAR>p : IntermediateField ℚ A → Prop<VAR>S : Set { F // p F }<VAR>T : Set A<VAR>hT : T.Finite<VAR>h : ∀ F ∈ S, ∃ x ∈ T, ↑F = ℚ⟮x⟯<GOAL>S.Finite
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>N : ℕ<VAR>hK : |NumberField.discr K| ≤ ↑N<GOAL>FiniteDimensional.finrank ℚ K ≤ NumberField.hermiteTheorem.rankOfDiscrBdd N
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>N : ℕ<VAR>hK : |NumberField.discr K| ≤ ↑N<GOAL>NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.hermiteTheorem.boundOfDiscBdd N)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>N : ℕ<VAR>hK : |NumberField.discr K| ≤ ↑N<VAR>a : NumberField.RingOfIntegers K<VAR>h : ℚ⟮↑a⟯ = ⊤<GOAL>(minpoly ℤ ↑a).natDegree ≤ NumberField.hermiteTheorem.rankOfDiscrBdd N
<VAR>A : Type u_2<VAR>Field A<VAR>CharZero A<VAR>N : ℕ<GOAL>{K | {w | w.IsReal}.Nonempty ∧ |NumberField.discr ↥↑K| ≤ ↑N}.Finite
<VAR>A : Type u_2<VAR>Field A<VAR>CharZero A<VAR>N : ℕ<GOAL>{K | {w | w.IsComplex}.Nonempty ∧ |NumberField.discr ↥↑K| ≤ ↑N}.Finite
<VAR>A : Type u_2<VAR>Field A<VAR>CharZero A<VAR>N : ℕ<GOAL>{K | |NumberField.discr ↥↑K| ≤ ↑N}.Finite
<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>K : Type u_1<VAR>Field K<VAR>DecidableEq ι<VAR>DecidableEq ι'<VAR>Fintype ι<VAR>Fintype ι'<VAR>NumberField K<VAR>b : Basis ι ℚ K<VAR>b' : Basis ι' ℚ K<VAR>h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)<VAR>h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (b'.toMatrix (⇑b) i j)<GOAL>Algebra.discr ℚ ⇑b = Algebra.discr ℚ ⇑b'
<VAR>V : Type w'<VAR>FirstOrder.Language.graph.Structure V<GOAL>V ⊨ FirstOrder.Language.Theory.simpleGraph ↔ (Irreflexive fun x y => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]) ∧ Symmetric fun x y => FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]
<VAR>V : Type w'<VAR>FirstOrder.Language.graph.Structure V<VAR>V ⊨ FirstOrder.Language.Theory.simpleGraph<VAR>x y : V<GOAL>(FirstOrder.Language.simpleGraphOfStructure V).Adj x y = FirstOrder.Language.Structure.RelMap FirstOrder.Language.adj ![x, y]
<VAR>V : Type w'<VAR>G : SimpleGraph V<GOAL>FirstOrder.Language.simpleGraphOfStructure V = G
<VAR>V : Type w'<VAR>S : FirstOrder.Language.graph.Structure V<VAR>V ⊨ FirstOrder.Language.Theory.simpleGraph<GOAL>(FirstOrder.Language.simpleGraphOfStructure V).structure = S
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>A : Rep k G<VAR>i j : ℕ<VAR>x : (groupCohomology.resolution k G).X i ⟶ A<GOAL>((groupCohomology.linearYonedaObjResolution A).d i j) x = (groupCohomology.resolution k G).d j i ≫ x
<VAR>k G : Type u<VAR>CommRing k<VAR>Monoid G<VAR>n : ℕ<VAR>A : Rep k G<VAR>f : (Fin n → G) → CoeSort.coe A<VAR>g : Fin (n + 1) → G<GOAL>(inhomogeneousCochains.d n A) f g = (A.ρ (g 0)) (f fun i => g i.succ) + ∑ j : Fin (n + 1), (-1) ^ (↑j + 1) • f (j.contractNth (fun x x_1 => x * x_1) g)
<VAR>k G : Type u<VAR>CommRing k<VAR>n : ℕ<VAR>Group G<VAR>A : Rep k G<GOAL>inhomogeneousCochains.d n A = (Rep.diagonalHomEquiv n A).toModuleIso.inv ≫ (groupCohomology.linearYonedaObjResolution A).d n (n + 1) ≫ (Rep.diagonalHomEquiv (n + 1) A).toModuleIso.hom
<VAR>k G : Type u<VAR>CommRing k<VAR>Group G<VAR>A : Rep k G<VAR>n : ℕ<GOAL>(groupCohomology.inhomogeneousCochains A).d n (n + 1) = inhomogeneousCochains.d n A
<VAR>L : FirstOrder.Language<VAR>L.IsOrdered<GOAL>L.orderLHom.onRelation FirstOrder.Language.leSymb = FirstOrder.Language.leSymb
<GOAL>FirstOrder.Language.order.orderLHom = FirstOrder.Language.LHom.id FirstOrder.Language.order
<VAR>L : FirstOrder.Language<VAR>M : Type w'<VAR>L.IsOrdered<VAR>LE M<VAR>L.Structure M<GOAL>L.OrderedStructure M ↔ L.orderLHom.IsExpansionOn M
<VAR>L : FirstOrder.Language<VAR>M : Type w'<VAR>L.IsOrdered<VAR>L.Structure M<VAR>LE M<VAR>L.OrderedStructure M<VAR>a b : M<GOAL>FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b] ↔ a ≤ b
<VAR>L : FirstOrder.Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>L.IsOrdered<VAR>L.Structure M<VAR>LE M<VAR>L.OrderedStructure M<VAR>t₁ t₂ : L.Term (α ⊕ Fin n)<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(t₁.le t₂).Realize v xs ↔ FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ ≤ FirstOrder.Language.Term.realize (Sum.elim v xs) t₂
<VAR>L : FirstOrder.Language<VAR>α : Type w<VAR>M : Type w'<VAR>n : ℕ<VAR>L.IsOrdered<VAR>L.Structure M<VAR>Preorder M<VAR>L.OrderedStructure M<VAR>t₁ t₂ : L.Term (α ⊕ Fin n)<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>(t₁.lt t₂).Realize v xs ↔ FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ < FirstOrder.Language.Term.realize (Sum.elim v xs) t₂
<VAR>M : Type w'<VAR>LE M<GOAL>M ⊨ FirstOrder.Language.order.noTopOrderSentence ↔ NoTopOrder M
<VAR>M : Type w'<VAR>LE M<VAR>h : NoTopOrder M<GOAL>M ⊨ FirstOrder.Language.order.noTopOrderSentence
<VAR>M : Type w'<VAR>LE M<GOAL>M ⊨ FirstOrder.Language.order.noBotOrderSentence ↔ NoBotOrder M
<VAR>M : Type w'<VAR>LE M<VAR>h : NoBotOrder M<GOAL>M ⊨ FirstOrder.Language.order.noBotOrderSentence
<VAR>M : Type w'<VAR>Preorder M<GOAL>M ⊨ FirstOrder.Language.order.denselyOrderedSentence ↔ DenselyOrdered M
<VAR>M : Type w'<VAR>Preorder M<VAR>h : DenselyOrdered M<GOAL>M ⊨ FirstOrder.Language.order.denselyOrderedSentence
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>N : Type w'<VAR>g : M ≃ N<GOAL>(Equiv.bundledInduced L g).str = g.inducedStructure
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>N : Type w'<VAR>g : M ≃ N<GOAL>↑(Equiv.bundledInduced L g) = N
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>self : T.ModelType<GOAL>↑self ⊨ T
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>self : T.ModelType<GOAL>Nonempty ↑self
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>M : Type w<VAR>L.Structure M<VAR>M ⊨ T<VAR>Nonempty M<GOAL>↑(FirstOrder.Language.Theory.ModelType.of T M) = M
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>L' : FirstOrder.Language<VAR>φ : L →ᴸ L'<VAR>M : (φ.onTheory T).ModelType<GOAL>(FirstOrder.Language.Theory.ModelType.reduct φ M).struc = φ.reduct ↑M
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>L' : FirstOrder.Language<VAR>φ : L →ᴸ L'<VAR>M : (φ.onTheory T).ModelType<GOAL>↑(FirstOrder.Language.Theory.ModelType.reduct φ M) = ↑M
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>L' : FirstOrder.Language<VAR>φ : L →ᴸ L'<VAR>h : φ.Injective<VAR>(n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => φ.onFunction f)<VAR>(n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => φ.onRelation r)<VAR>M : T.ModelType<VAR>Inhabited ↑M<GOAL>↑(FirstOrder.Language.Theory.ModelType.defaultExpansion h M) = ↑M
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>L' : FirstOrder.Language<VAR>φ : L →ᴸ L'<VAR>h : φ.Injective<VAR>(n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => φ.onFunction f)<VAR>(n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => φ.onRelation r)<VAR>M : T.ModelType<VAR>Inhabited ↑M<GOAL>(FirstOrder.Language.Theory.ModelType.defaultExpansion h M).struc = φ.defaultExpansion ↑M
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>M : T.ModelType<VAR>T' : L.Theory<VAR>h : T' ⊆ T<GOAL>(M.subtheoryModel h).struc = M.struc
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>M : T.ModelType<VAR>T' : L.Theory<VAR>h : T' ⊆ T<GOAL>↑(M.subtheoryModel h) = ↑M
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>M : Type w<VAR>L.Structure M<VAR>Nonempty M<VAR>h : M ⊨ T<GOAL>↑h.bundled = M
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>t : L.Term α<GOAL>FirstOrder.Language.Term.relabel id t = t
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>FirstOrder.Language.Term.relabel id = id
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<VAR>t : L.Term α<GOAL>FirstOrder.Language.Term.relabel g (FirstOrder.Language.Term.relabel f t) = FirstOrder.Language.Term.relabel (g ∘ f) t
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → γ<GOAL>FirstOrder.Language.Term.relabel g ∘ FirstOrder.Language.Term.relabel f = FirstOrder.Language.Term.relabel (g ∘ f)
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>g : α ≃ β<GOAL>∀ (a : L.Term α), (FirstOrder.Language.Term.relabelEquiv g) a = FirstOrder.Language.Term.relabel (⇑g) a
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>g : α ≃ β<GOAL>∀ (a : L.Term β), (FirstOrder.Language.Term.relabelEquiv g).symm a = FirstOrder.Language.Term.relabel (⇑g.symm) a
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>γ : Type u_3<GOAL>∀ (a : L.Term (γ ⊕ α)), FirstOrder.Language.Term.constantsVarsEquiv.symm a = a.varsToConstants
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>γ : Type u_3<GOAL>∀ (a : (L.withConstants γ).Term α), FirstOrder.Language.Term.constantsVarsEquiv a = a.constantsToVars
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>t : (L.withConstants γ).Term (α ⊕ β)<GOAL>FirstOrder.Language.Term.constantsVarsEquivLeft t = FirstOrder.Language.Term.relabel (⇑(Equiv.sumAssoc γ α β).symm) t.constantsToVars
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>t : L.Term ((γ ⊕ α) ⊕ β)<GOAL>FirstOrder.Language.Term.constantsVarsEquivLeft.symm t = (FirstOrder.Language.Term.relabel (⇑(Equiv.sumAssoc γ α β)) t).varsToConstants
<VAR>L : FirstOrder.Language<VAR>α : Type u'<GOAL>(FirstOrder.Language.LHom.id L).onTerm = id
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>L'' : FirstOrder.Language<VAR>φ : L' →ᴸ L''<VAR>ψ : L →ᴸ L'<GOAL>(φ.comp ψ).onTerm = φ.onTerm ∘ ψ.onTerm
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>φ : L ≃ᴸ L'<GOAL>∀ (a : L.Term α), (FirstOrder.Language.Lequiv.onTerm φ) a = φ.toLHom.onTerm a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>φ : L ≃ᴸ L'<GOAL>∀ (a : L'.Term α), (FirstOrder.Language.Lequiv.onTerm φ).symm a = φ.invLHom.onTerm a
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>h : n ≤ n<VAR>φ : L.BoundedFormula α n<GOAL>FirstOrder.Language.BoundedFormula.castLE h φ = φ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>k m n : ℕ<VAR>km : k ≤ m<VAR>mn : m ≤ n<VAR>φ : L.BoundedFormula α k<GOAL>FirstOrder.Language.BoundedFormula.castLE mn (FirstOrder.Language.BoundedFormula.castLE km φ) = FirstOrder.Language.BoundedFormula.castLE ⋯ φ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>k m n : ℕ<VAR>km : k ≤ m<VAR>mn : m ≤ n<GOAL>FirstOrder.Language.BoundedFormula.castLE mn ∘ FirstOrder.Language.BoundedFormula.castLE km = FirstOrder.Language.BoundedFormula.castLE ⋯
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>L'' : FirstOrder.Language<VAR>ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)<VAR>fr : (n : ℕ) → L.Relations n → L'.Relations n<VAR>ft' : (n : ℕ) → L'.Term (β ⊕ Fin n) → L''.Term (γ ⊕ Fin n)<VAR>fr' : (n : ℕ) → L'.Relations n → L''.Relations n<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>FirstOrder.Language.BoundedFormula.mapTermRel ft' fr' (fun x => id) (FirstOrder.Language.BoundedFormula.mapTermRel ft fr (fun x => id) φ) = FirstOrder.Language.BoundedFormula.mapTermRel (fun x => ft' x ∘ ft x) (fun x => fr' x ∘ fr x) (fun x => id) φ
<VAR>L : FirstOrder.Language<VAR>α : Type u'<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>FirstOrder.Language.BoundedFormula.mapTermRel (fun x => id) (fun x => id) (fun x => id) φ = φ
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)<VAR>fr : (n : ℕ) → L.Relations n ≃ L'.Relations n<VAR>n : ℕ<GOAL>∀ (a : L'.BoundedFormula β n), (FirstOrder.Language.BoundedFormula.mapTermRelEquiv ft fr).symm a = FirstOrder.Language.BoundedFormula.mapTermRel (fun n => ⇑(ft n).symm) (fun n => ⇑(fr n).symm) (fun x => id) a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>α : Type u'<VAR>β : Type v'<VAR>ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)<VAR>fr : (n : ℕ) → L.Relations n ≃ L'.Relations n<VAR>n : ℕ<GOAL>∀ (a : L.BoundedFormula α n), (FirstOrder.Language.BoundedFormula.mapTermRelEquiv ft fr) a = FirstOrder.Language.BoundedFormula.mapTermRel (fun n => ⇑(ft n)) (fun n => ⇑(fr n)) (fun x => id) a
<VAR>M : Type w<VAR>α : Type u'<VAR>β : Type v'<VAR>n m : ℕ<VAR>g : α → β ⊕ Fin n<VAR>v : β → M<VAR>xs : Fin (n + m) → M<GOAL>Sum.elim v xs ∘ FirstOrder.Language.BoundedFormula.relabelAux g m = Sum.elim (Sum.elim v (xs ∘ Fin.castAdd m) ∘ g) (xs ∘ Fin.natAdd n)
<VAR>α : Type u'<VAR>n : ℕ<VAR>k : ℕ<GOAL>FirstOrder.Language.BoundedFormula.relabelAux Sum.inl k = Sum.map id (Fin.natAdd n)