mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.addUnit_of_val_addUnits : ∀ {M : Type u_1} [inst : AddMonoid M] {a : AddUnits M} (h : IsAddUnit ↑a), h.addUnit = a
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.inv_rnDeriv' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], μ.AbsolutelyContinuous ν → (ν.rnDeriv μ)⁻¹ =ᵐ[μ] μ.rnDeriv ν
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
orbit_fixingAddSubgroup_compl_subset : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α} {a : α},
  a ∈ s → AddAction.orbit (↥(fixingAddSubgroup M sᶜ)) a ⊆ s
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.L2.integral_inner_eq_sq_eLpNorm : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] (f : ↥(MeasureTheory.Lp E 2 μ)),
  ∫ (a : α), inner 𝕜 (↑↑f a) (↑↑f a) ∂μ = ↑(∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ).toReal
-- Lean.Data.Lsp.Basic
Lean.Lsp.TextDocumentItem.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (languageId : String) (version : ℕ) (text : String),
  sizeOf { uri := uri, languageId := languageId, version := version, text := text } =
    1 + sizeOf uri + sizeOf languageId + sizeOf version + sizeOf text
-- Mathlib.Topology.Algebra.Group.Basic
mem_closure_iff_nhds_zero : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {x : G} {s : Set G},
  x ∈ closure s ↔ ∀ U ∈ nhds 0, ∃ y ∈ s, y - x ∈ U
-- Mathlib.GroupTheory.FinitelyPresentedGroup
AddSubgroup.IsFinitelyNormallyGenerated.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G),
  N.IsFinitelyNormallyGenerated = ∃ S, S.Finite ∧ AddSubgroup.normalClosure S = N
-- Init.Data.List.Scan.Lemmas
List.length_scanl : ∀ {β : Type u_1} {α : Type u_2} {init : β} {as : List α} {f : β → α → β}, (List.scanl f init as).length = as.length + 1
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.constVSub_symm_apply : ∀ {V : Type u_1} {P : Type u_2} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p : P) (x : V),
  (Homeomorph.constVSub p).symm x = -x +ᵥ p
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- A locally-fully-faithful and cover-dense functor preserves compatible families.  -/
CategoryTheory.Functor.IsCoverDense.compatiblePreserving : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (K : CategoryTheory.GrothendieckTopology D)
  (G : CategoryTheory.Functor C D) [G.IsCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K],
  CategoryTheory.CompatiblePreserving K G