ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>self : FirstOrder.Ring.CompatibleRing R<VAR>x : Fin 1 → R<GOAL>FirstOrder.Language.Structure.funMap FirstOrder.Ring.negFunc x = -x 0
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>self : FirstOrder.Ring.CompatibleRing R<VAR>x : Fin 0 → R<GOAL>FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc x = 0
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>self : FirstOrder.Ring.CompatibleRing R<VAR>x : Fin 0 → R<GOAL>FirstOrder.Language.Structure.funMap FirstOrder.Ring.oneFunc x = 1
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>self : FirstOrder.Ring.CompatibleRing R<VAR>x : Fin 2 → R<GOAL>FirstOrder.Language.Structure.funMap FirstOrder.Ring.mulFunc x = x 0 * x 1
<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>self : FirstOrder.Ring.CompatibleRing R<VAR>x : Fin 2 → R<GOAL>FirstOrder.Language.Structure.funMap FirstOrder.Ring.addFunc x = x 0 + x 1
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>FirstOrder.Ring.CompatibleRing R<VAR>x y : FirstOrder.Language.ring.Term α<VAR>v : α → R<GOAL>FirstOrder.Language.Term.realize v (x + y) = FirstOrder.Language.Term.realize v x + FirstOrder.Language.Term.realize v y
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>FirstOrder.Ring.CompatibleRing R<VAR>x y : FirstOrder.Language.ring.Term α<VAR>v : α → R<GOAL>FirstOrder.Language.Term.realize v (x * y) = FirstOrder.Language.Term.realize v x * FirstOrder.Language.Term.realize v y
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>FirstOrder.Ring.CompatibleRing R<VAR>x : FirstOrder.Language.ring.Term α<VAR>v : α → R<GOAL>FirstOrder.Language.Term.realize v (-x) = -FirstOrder.Language.Term.realize v x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>FirstOrder.Ring.CompatibleRing R<VAR>v : α → R<GOAL>FirstOrder.Language.Term.realize v 0 = 0
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>Add R<VAR>Mul R<VAR>Neg R<VAR>One R<VAR>Zero R<VAR>FirstOrder.Ring.CompatibleRing R<VAR>v : α → R<GOAL>FirstOrder.Language.Term.realize v 1 = 1
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>s : Setoid M<VAR>self : L.Prestructure s<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x y : Fin n → M<GOAL>x ≈ y → FirstOrder.Language.Structure.funMap f x ≈ FirstOrder.Language.Structure.funMap f y
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>s : Setoid M<VAR>self : L.Prestructure s<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x y : Fin n → M<GOAL>x ≈ y → FirstOrder.Language.Structure.RelMap r x = FirstOrder.Language.Structure.RelMap r y
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>s : Setoid M<VAR>ps : L.Prestructure s<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>(FirstOrder.Language.Structure.funMap f fun i => ⟦x i⟧) = ⟦FirstOrder.Language.Structure.funMap f x⟧
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>s : Setoid M<VAR>ps : L.Prestructure s<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>(FirstOrder.Language.Structure.RelMap r fun i => ⟦x i⟧) ↔ FirstOrder.Language.Structure.RelMap r x
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>s : Setoid M<VAR>ps : L.Prestructure s<VAR>β : Type u_2<VAR>t : L.Term β<VAR>x : β → M<GOAL>FirstOrder.Language.Term.realize (fun i => ⟦x i⟧) t = ⟦FirstOrder.Language.Term.realize x t⟧
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : L.Substructure M<GOAL>N.FG ↔ ∃ S, S.Finite ∧ (FirstOrder.Language.Substructure.closure L).toFun S = N
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : L.Substructure M<GOAL>N.FG ↔ ∃ n s, (FirstOrder.Language.Substructure.closure L).toFun (Set.range s) = N
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<GOAL>⊥.FG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>s : Set M<VAR>hs : s.Finite<GOAL>((FirstOrder.Language.Substructure.closure L).toFun s).FG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>x : M<GOAL>((FirstOrder.Language.Substructure.closure L).toFun {x}).FG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N₁ N₂ : L.Substructure M<VAR>hN₁ : N₁.FG<VAR>hN₂ : N₂.FG<GOAL>(N₁ ⊔ N₂).FG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>f : M →[L] N<VAR>s : L.Substructure M<VAR>hs : s.FG<GOAL>(FirstOrder.Language.Substructure.map f s).FG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>hs : (FirstOrder.Language.Substructure.map f.toHom s).FG<GOAL>s.FG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : L.Substructure M<GOAL>N.CG ↔ ∃ S, S.Countable ∧ (FirstOrder.Language.Substructure.closure L).toFun S = N
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : L.Substructure M<VAR>h : N.FG<GOAL>N.CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : L.Substructure M<GOAL>N.CG ↔ ↑N = ∅ ∨ ∃ s, (FirstOrder.Language.Substructure.closure L).toFun (Set.range s) = N
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<GOAL>⊥.CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>s : Set M<VAR>hs : s.Countable<GOAL>((FirstOrder.Language.Substructure.closure L).toFun s).CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>x : M<GOAL>((FirstOrder.Language.Substructure.closure L).toFun {x}).CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N₁ N₂ : L.Substructure M<VAR>hN₁ : N₁.CG<VAR>hN₂ : N₂.CG<GOAL>(N₁ ⊔ N₂).CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>f : M →[L] N<VAR>s : L.Substructure M<VAR>hs : s.CG<GOAL>(FirstOrder.Language.Substructure.map f s).CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>hs : (FirstOrder.Language.Substructure.map f.toHom s).CG<GOAL>s.CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>Countable ((l : ℕ) × L.Functions l)<VAR>s : L.Substructure M<GOAL>s.CG ↔ Countable ↥s
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>self : FirstOrder.Language.Structure.FG L M<GOAL>⊤.FG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>self : FirstOrder.Language.Structure.CG L M<GOAL>⊤.CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<GOAL>FirstOrder.Language.Structure.FG L M ↔ ⊤.FG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<GOAL>FirstOrder.Language.Structure.FG L M ↔ ∃ S, S.Finite ∧ (FirstOrder.Language.Substructure.closure L).toFun S = ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>h : FirstOrder.Language.Structure.FG L M<VAR>f : M →[L] N<GOAL>f.range.FG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>h : FirstOrder.Language.Structure.FG L M<VAR>f : M →[L] N<VAR>hs : Function.Surjective ⇑f<GOAL>FirstOrder.Language.Structure.FG L N
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<GOAL>FirstOrder.Language.Structure.CG L M ↔ ⊤.CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<GOAL>FirstOrder.Language.Structure.CG L M ↔ ∃ S, S.Countable ∧ (FirstOrder.Language.Substructure.closure L).toFun S = ⊤
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>h : FirstOrder.Language.Structure.CG L M<VAR>f : M →[L] N<GOAL>f.range.CG
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>h : FirstOrder.Language.Structure.CG L M<VAR>f : M →[L] N<VAR>hs : Function.Surjective ⇑f<GOAL>FirstOrder.Language.Structure.CG L N
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>Countable ((l : ℕ) × L.Functions l)<GOAL>FirstOrder.Language.Structure.CG L M ↔ Countable M
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>h : FirstOrder.Language.Structure.FG L M<GOAL>FirstOrder.Language.Structure.CG L M
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>f : M ≃[L] N<GOAL>FirstOrder.Language.Structure.FG L M ↔ FirstOrder.Language.Structure.FG L N
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : L.Substructure M<GOAL>S.FG ↔ FirstOrder.Language.Structure.FG L ↥S
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>N : Type u_2<VAR>L.Structure N<VAR>f : M ≃[L] N<GOAL>FirstOrder.Language.Structure.CG L M ↔ FirstOrder.Language.Structure.CG L N
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : L.Substructure M<GOAL>S.CG ↔ FirstOrder.Language.Structure.CG L ↥S
<VAR>K : Type u_2<VAR>Add K<VAR>Mul K<VAR>Neg K<VAR>Zero K<VAR>One K<VAR>FirstOrder.Ring.CompatibleRing K<VAR>ax : FirstOrder.Field.FieldAxiom<GOAL>K ⊨ ax.toSentence ↔ FirstOrder.Field.FieldAxiom.toProp K ax
<VAR>K : Type u_2<VAR>Add K<VAR>Mul K<VAR>Neg K<VAR>Zero K<VAR>One K<VAR>FirstOrder.Ring.CompatibleRing K<VAR>K ⊨ FirstOrder.Language.Theory.field<VAR>ax : FirstOrder.Field.FieldAxiom<GOAL>FirstOrder.Field.FieldAxiom.toProp K ax
<VAR>L : FirstOrder.Language<VAR>_n : ℕ<VAR>a : L.Relations _n<GOAL>(FirstOrder.Language.LHom.id L).onRelation a = id a
<VAR>L : FirstOrder.Language<VAR>_n : ℕ<VAR>a : L.Functions _n<GOAL>(FirstOrder.Language.LHom.id L).onFunction a = id a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>_n : ℕ<VAR>val : L.Functions _n<GOAL>FirstOrder.Language.LHom.sumInl.onFunction val = Sum.inl val
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>_n : ℕ<VAR>val : L.Relations _n<GOAL>FirstOrder.Language.LHom.sumInl.onRelation val = Sum.inl val
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>_n : ℕ<VAR>val : L'.Functions _n<GOAL>FirstOrder.Language.LHom.sumInr.onFunction val = Sum.inr val
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>_n : ℕ<VAR>val : L'.Relations _n<GOAL>FirstOrder.Language.LHom.sumInr.onRelation val = Sum.inr val
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>L.IsAlgebraic<VAR>L.IsRelational<VAR>n : ℕ<VAR>a : L.Relations n<GOAL>(FirstOrder.Language.LHom.ofIsEmpty L L').onRelation a = ⋯.elim a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>L.IsAlgebraic<VAR>L.IsRelational<VAR>n : ℕ<VAR>a : L.Functions n<GOAL>(FirstOrder.Language.LHom.ofIsEmpty L L').onFunction a = ⋯.elim a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>F G : L →ᴸ L'<VAR>h_fun : F.onFunction = G.onFunction<VAR>h_rel : F.onRelation = G.onRelation<GOAL>F = G
<VAR>L' : FirstOrder.Language<VAR>c f₁ f₂ : Type u<VAR>r₁ r₂ : Type v<VAR>F G : FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂ →ᴸ L'<VAR>h0 : ∀ (c_1 : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Constants), F.onFunction c_1 = G.onFunction c_1<VAR>h1 : ∀ (f : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions 1), F.onFunction f = G.onFunction f<VAR>h2 : ∀ (f : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Functions 2), F.onFunction f = G.onFunction f<VAR>h1' : ∀ (r : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations 1), F.onRelation r = G.onRelation r<VAR>h2' : ∀ (r : (FirstOrder.Language.mk₂ c f₁ f₂ r₁ r₂).Relations 2), F.onRelation r = G.onRelation r<GOAL>F = G
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>L'' : FirstOrder.Language<VAR>g : L' →ᴸ L''<VAR>f : L →ᴸ L'<VAR>_n : ℕ<VAR>F : L.Functions _n<GOAL>(g.comp f).onFunction F = g.onFunction (f.onFunction F)
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>L'' : FirstOrder.Language<VAR>g : L' →ᴸ L''<VAR>f : L →ᴸ L'<GOAL>∀ (x : ℕ) (R : L.Relations x), (g.comp f).onRelation R = g.onRelation (f.onRelation R)
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>F : L →ᴸ L'<GOAL>(FirstOrder.Language.LHom.id L').comp F = F
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>F : L →ᴸ L'<GOAL>F.comp (FirstOrder.Language.LHom.id L) = F
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>L'' : FirstOrder.Language<VAR>L3 : FirstOrder.Language<VAR>F : L'' →ᴸ L3<VAR>G : L' →ᴸ L''<VAR>H : L →ᴸ L'<GOAL>(F.comp G).comp H = F.comp (G.comp H)
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>L'' : FirstOrder.Language<VAR>ψ : L'' →ᴸ L'<VAR>_n : ℕ<GOAL>∀ (a : L.Functions _n ⊕ L''.Functions _n), (ϕ.sumElim ψ).onFunction a = Sum.elim (fun f => ϕ.onFunction f) (fun f => ψ.onFunction f) a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>L'' : FirstOrder.Language<VAR>ψ : L'' →ᴸ L'<VAR>_n : ℕ<GOAL>∀ (a : L.Relations _n ⊕ L''.Relations _n), (ϕ.sumElim ψ).onRelation a = Sum.elim (fun f => ϕ.onRelation f) (fun f => ψ.onRelation f) a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>L'' : FirstOrder.Language<VAR>ψ : L'' →ᴸ L'<GOAL>(ϕ.sumElim ψ).comp FirstOrder.Language.LHom.sumInl = ϕ
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>L'' : FirstOrder.Language<VAR>ψ : L'' →ᴸ L'<GOAL>(ϕ.sumElim ψ).comp FirstOrder.Language.LHom.sumInr = ψ
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<GOAL>FirstOrder.Language.LHom.sumInl.sumElim FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.id (L.sum L')
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>L'' : FirstOrder.Language<VAR>ψ : L'' →ᴸ L'<VAR>L3 : FirstOrder.Language<VAR>θ : L' →ᴸ L3<GOAL>θ.comp (ϕ.sumElim ψ) = (θ.comp ϕ).sumElim (θ.comp ψ)
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>L₁ : FirstOrder.Language<VAR>L₂ : FirstOrder.Language<VAR>ψ : L₁ →ᴸ L₂<VAR>_n : ℕ<GOAL>∀ (a : L.Functions _n ⊕ L₁.Functions _n), (ϕ.sumMap ψ).onFunction a = Sum.map (fun f => ϕ.onFunction f) (fun f => ψ.onFunction f) a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>L₁ : FirstOrder.Language<VAR>L₂ : FirstOrder.Language<VAR>ψ : L₁ →ᴸ L₂<VAR>_n : ℕ<GOAL>∀ (a : L.Relations _n ⊕ L₁.Relations _n), (ϕ.sumMap ψ).onRelation a = Sum.map (fun f => ϕ.onRelation f) (fun f => ψ.onRelation f) a
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>L₁ : FirstOrder.Language<VAR>L₂ : FirstOrder.Language<VAR>ψ : L₁ →ᴸ L₂<GOAL>(ϕ.sumMap ψ).comp FirstOrder.Language.LHom.sumInl = FirstOrder.Language.LHom.sumInl.comp ϕ
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>L₁ : FirstOrder.Language<VAR>L₂ : FirstOrder.Language<VAR>ψ : L₁ →ᴸ L₂<GOAL>(ϕ.sumMap ψ).comp FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.sumInr.comp ψ
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>self : ϕ.Injective<VAR>n : ℕ<GOAL>Function.Injective fun f => ϕ.onFunction f
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>self : ϕ.Injective<VAR>n : ℕ<GOAL>Function.Injective fun R => ϕ.onRelation R
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>M : Type u_1<VAR>L.Structure M<VAR>L'.Structure M<VAR>self : ϕ.IsExpansionOn M<VAR>n : ℕ<VAR>R : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>M : Type u_1<VAR>L.Structure M<VAR>L'.Structure M<VAR>self : ϕ.IsExpansionOn M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>M : Type u_1<VAR>L.Structure M<VAR>L'.Structure M<VAR>ϕ.IsExpansionOn M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<VAR>M : Type u_1<VAR>L.Structure M<VAR>L'.Structure M<VAR>ϕ.IsExpansionOn M<VAR>n : ℕ<VAR>R : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>(L.sum L').Structure M<VAR>FirstOrder.Language.LHom.sumInl.IsExpansionOn M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.funMap (Sum.inl f) x = FirstOrder.Language.Structure.funMap f x
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>(L'.sum L).Structure M<VAR>FirstOrder.Language.LHom.sumInr.IsExpansionOn M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.funMap (Sum.inr f) x = FirstOrder.Language.Structure.funMap f x
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<GOAL>FirstOrder.Language.LHom.sumInl.Injective
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<GOAL>FirstOrder.Language.LHom.sumInr.Injective
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>ϕ : L →ᴸ L'<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>h : ϕ.Injective<VAR>M : Type u_1<VAR>Inhabited M<VAR>L.Structure M<GOAL>ϕ.IsExpansionOn M
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>self : L ≃ᴸ L'<GOAL>self.toLHom.comp self.invLHom = FirstOrder.Language.LHom.id L'
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>self : L ≃ᴸ L'<GOAL>self.invLHom.comp self.toLHom = FirstOrder.Language.LHom.id L
<VAR>L : FirstOrder.Language<GOAL>(FirstOrder.Language.LEquiv.refl L).invLHom = FirstOrder.Language.LHom.id L
<VAR>L : FirstOrder.Language<GOAL>(FirstOrder.Language.LEquiv.refl L).toLHom = FirstOrder.Language.LHom.id L
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>e : L ≃ᴸ L'<GOAL>e.symm.toLHom = e.invLHom
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>e : L ≃ᴸ L'<GOAL>e.symm.invLHom = e.toLHom
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>L'' : FirstOrder.Language<VAR>e : L ≃ᴸ L'<VAR>e' : L' ≃ᴸ L''<GOAL>(e.trans e').toLHom = e'.toLHom.comp e.toLHom
<VAR>L : FirstOrder.Language<VAR>L' : FirstOrder.Language<VAR>L'' : FirstOrder.Language<VAR>e : L ≃ᴸ L'<VAR>e' : L' ≃ᴸ L''<GOAL>(e.trans e').invLHom = e.invLHom.comp e'.invLHom
<VAR>α : Type u'<GOAL>(FirstOrder.Language.constantsOn α).Constants = α
<VAR>α : Type u'<GOAL>(FirstOrder.Language.constantsOn α).card = Cardinal.mk α
<VAR>M : Type w<VAR>α : Type u'<VAR>β : Type v'<VAR>f : α → β<VAR>fα : α → M<VAR>fβ : β → M<VAR>h : fβ ∘ f = fα<GOAL>(FirstOrder.Language.LHom.constantsOnMap f).IsExpansionOn M
<VAR>L : FirstOrder.Language<VAR>α : Type w'<GOAL>(L.withConstants α).card = Cardinal.lift.{w', max u v} L.card + Cardinal.lift.{max u v, w'} (Cardinal.mk α)
<VAR>L : FirstOrder.Language<VAR>α : Type w'<VAR>_n : ℕ<VAR>val : L.Functions _n<GOAL>(L.lhomWithConstants α).onFunction val = Sum.inl val
<VAR>L : FirstOrder.Language<VAR>α : Type w'<VAR>_n : ℕ<VAR>val : L.Relations _n<GOAL>(L.lhomWithConstants α).onRelation val = Sum.inl val
<VAR>L : FirstOrder.Language<VAR>α : Type w'<GOAL>(L.lhomWithConstants α).Injective
<VAR>L : FirstOrder.Language<VAR>α : Type w'<VAR>ie : IsEmpty α<GOAL>(FirstOrder.Language.LEquiv.addEmptyConstants L α).toLHom = L.lhomWithConstants α
<VAR>L : FirstOrder.Language<VAR>α : Type w'<VAR>ie : IsEmpty α<GOAL>(FirstOrder.Language.LEquiv.addEmptyConstants L α).invLHom = (FirstOrder.Language.LHom.id L).sumElim (FirstOrder.Language.LHom.ofIsEmpty (FirstOrder.Language.constantsOn α) L)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type w'<VAR>(L.withConstants α).Structure M<VAR>(L.lhomWithConstants α).IsExpansionOn M<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.funMap (Sum.inl f) x = FirstOrder.Language.Structure.funMap f x
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type w'<VAR>(L.withConstants α).Structure M<VAR>(L.lhomWithConstants α).IsExpansionOn M<VAR>n : ℕ<VAR>R : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap (Sum.inl R) x = FirstOrder.Language.Structure.RelMap R x
<VAR>L : FirstOrder.Language<VAR>α : Type w'<VAR>β : Type u_1<VAR>f : α → β<GOAL>(L.lhomWithConstantsMap f).comp FirstOrder.Language.LHom.sumInl = L.lhomWithConstants β
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>α : Type u_1<VAR>(FirstOrder.Language.constantsOn α).Structure M<VAR>a : α<VAR>x : Fin 0 → M<GOAL>FirstOrder.Language.Structure.funMap (Sum.inr a) x = ↑(L.con a)
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>L.Structure M<VAR>A : Set M<VAR>a : ↑A<GOAL>↑(L.con a) = ↑a
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>SecondCountableTopology E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : α → ℝ≥0<VAR>hf : Measurable f<VAR>g : α → E<GOAL>AEMeasurable g (μ.withDensity fun x => ↑(f x)) ↔ AEMeasurable (fun x => ↑(f x) • g x) μ
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>self : M ↪ₑ[L] N<VAR>n : ℕ<VAR>φ : L.Formula (Fin n)<VAR>x : Fin n → M<GOAL>φ.Realize (↑self ∘ x) ↔ φ.Realize x
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪ₑ[L] N<VAR>α : Type u_5<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>v : α → M<VAR>xs : Fin n → M<GOAL>φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪ₑ[L] N<VAR>α : Type u_5<VAR>φ : L.Formula α<VAR>x : α → M<GOAL>φ.Realize (⇑f ∘ x) ↔ φ.Realize x
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪ₑ[L] N<VAR>φ : L.Sentence<GOAL>M ⊨ φ ↔ N ⊨ φ
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪ₑ[L] N<VAR>T : L.Theory<GOAL>M ⊨ T ↔ N ⊨ T
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪ₑ[L] N<GOAL>M ≅[L] N
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : M ↪ₑ[L] N<GOAL>Function.Injective ⇑φ
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : M ↪ₑ[L] N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<GOAL>φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : M ↪ₑ[L] N<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>φ : M ↪ₑ[L] N<VAR>c : L.Constants<GOAL>φ ↑c = ↑c
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪ₑ[L] N<GOAL>f.toEmbedding.toHom = f.toHom
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪ₑ[L] N<GOAL>⇑f.toHom = ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f : M ↪ₑ[L] N<GOAL>⇑f.toEmbedding = ⇑f
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<GOAL>Function.Injective DFunLike.coe
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : M ↪ₑ[L] N<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>L.Structure M<VAR>L.Structure N<VAR>f g : M ↪ₑ[L] N<GOAL>f = g ↔ ∀ (x : M), f x = g x
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>L.Structure M<VAR>x : M<GOAL>(FirstOrder.Language.ElementaryEmbedding.refl L M) x = x
<VAR>L : FirstOrder.Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>L.Structure M<VAR>L.Structure N<VAR>L.Structure P<VAR>g : N ↪ₑ[L] P<VAR>f : M ↪ₑ[L] N<VAR>x : M<GOAL>(g.comp f) x = g (f x)