mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The precomposition with a localization functor gives fully faithful functors
between functor categories.  -/
CategoryTheory.Localization.fullyFaithfulWhiskeringLeft : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [L.IsLocalization W] →
              (E : Type u_4) →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} E] →
                  ((CategoryTheory.Functor.whiskeringLeft C D E).obj L).FullyFaithful
-- Std.Async.TCP
_private.Std.Async.TCP.0.Std.Async.TCP.Socket.Server.ofNative : Std.Internal.UV.TCP.Socket → Std.Async.TCP.Socket.Server
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.wikidataIdParser.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Array.Lemmas
Array.filterMap_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → Option γ} {xs : Array α},
  Array.filterMap g (Array.map f xs) = Array.filterMap (g ∘ f) xs
-- Mathlib.Order.BoundedOrder.Basic
Prod.instOrderBot.eq_1 : ∀ (α : Type u) (β : Type v) [inst : LE α] [inst_1 : LE β] [inst_2 : OrderBot α] [inst_3 : OrderBot β],
  Prod.instOrderBot α β = { toBot := inferInstance, bot_le := ⋯ }
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Given `f : α → β` with `β` a group, the canonical map `List (α × Bool) → β`  -/
FreeGroup.Lift.aux : {α : Type u} → {β : Type v} → [Group β] → (α → β) → List (α × Bool) → β
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddLeftCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddLeftCancelMonoid α],
  OrderDual.instAddLeftCancelMonoid = { toAddMonoid := OrderDual.instAddMonoid, toIsLeftCancelAdd := ⋯ }
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAtFilter.isEquivalent_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {L : Filter (𝕜 × 𝕜)},
  HasDerivAtFilter f f' L → f' ≠ 0 → Asymptotics.IsEquivalent L (fun p => f p.1 - f p.2) fun p => (p.1 - p.2) • f'
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.GoTo.left : ExistsAndEq.GoTo
-- Mathlib.MeasureTheory.Measure.Prod
/-- Two finite measures on a product are equal iff they are equal on products of sets.  -/
MeasureTheory.Measure.ext_prod_iff : ∀ {α : Type u_4} {β : Type u_5} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure (α × β)}
  [MeasureTheory.IsFiniteMeasure μ],
  μ = ν ↔ ∀ {s : Set α} {t : Set β}, MeasurableSet s → MeasurableSet t → μ (s ×ˢ t) = ν (s ×ˢ t)
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.Context.paramNamePrefix : Lean.MetavarContext.LevelMVarToParam.Context → Lean.Name
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.isoClosure_respectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
  P.isoClosure.RespectsIso
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.glue.eq_1 : ∀ {α : Type u} {β : α → Type v} (r : Std.DTreeMap.Internal.Impl α β) (hr : r.Balanced)
  (hl_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr_2 : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size),
  Std.DTreeMap.Internal.Impl.leaf.glue r hl_2 hr hlr_2 = r
-- Lean.Widget.UserWidget
/-- Registers a widget module. Its type must implement `Lean.Widget.ToModule`.  -/
Lean.Widget.widgetModuleAttrImpl : Lean.AttributeImpl
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffAt_of_subsingleton : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  {n : WithTop ℕ∞} [Subsingleton F], ContDiffAt 𝕜 n f x
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
catalan_two : catalan 2 = 2
-- Std.Time.Format.DateFormat
/-- Full day-period strings for the `b` pattern (AM, PM, noon, midnight).
Used by `bbbb`. Per TR35, AM/PM here are lowercase ("ante meridiem" / "post meridiem").
 -/
Std.Time.DateFormatSymbols.dayPeriodLong : Std.Time.DateFormatSymbols → Std.Time.DayPeriodSymbols
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α},
  Std.DHashMap.Const.get! (m₁.diff m₂) k = if k ∈ m₂ then default else Std.DHashMap.Const.get! m₁ k
-- Mathlib.Data.Num.Prime
/-- Returns the smallest prime factor of `n ≠ 1`.  -/
PosNum.minFac : PosNum → PosNum
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.forget_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.SimplicialObject.Split C}
  (Φ : X ⟶ Y), (CategoryTheory.SimplicialObject.Split.forget C).map Φ = Φ.F
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.preimage_ofSnowflaking_ball : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoMetricSpace X] (x : X) {r : ℝ},
  0 ≤ r →
    ⇑Metric.Snowflaking.ofSnowflaking ⁻¹' Metric.ball x r = Metric.ball (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
/-- A property of objects `P` is inherited from the target of morphisms satisfying `Q` if
whenever `P` holds for `Y` and `f : X ⟶ Y` is a `Q`-morphism, then `P` holds for `X`.  -/
CategoryTheory.ObjectProperty.InheritedFromTarget : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Algebra.Regular.Opposite
isRightRegular_op : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsRightRegular (MulOpposite.op a) ↔ IsLeftRegular a
-- Init.Data.Array.GetLit
Array.toListLitAux : {α : Type u_1} → (xs : Array α) → (n : ℕ) → xs.size = n → (i : ℕ) → i ≤ xs.size → List α → List α
-- Lean.ProjFns
Lean.ProjectionFunctionInfo.mk.inj : ∀ {ctorName : Lean.Name} {numParams i : ℕ} {fromClass : Bool} {ctorName_1 : Lean.Name} {numParams_1 i_1 : ℕ}
  {fromClass_1 : Bool},
  { ctorName := ctorName, numParams := numParams, i := i, fromClass := fromClass } =
      { ctorName := ctorName_1, numParams := numParams_1, i := i_1, fromClass := fromClass_1 } →
    ctorName = ctorName_1 ∧ numParams = numParams_1 ∧ i = i_1 ∧ fromClass = fromClass_1
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.mapAddHom_apply : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] {X Y : C} (f : X ⟶ Y),
  F.mapAddHom f = F.map f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_subset : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s t : Set α}, s⁻¹ ⊆ t ↔ s ⊆ t⁻¹
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.instProperSpace : ProperSpace UpperHalfPlane
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β k}, k ∉ m₁ → (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
-- Mathlib.Data.EReal.Operations
/-- `-a < b` if and only if `-b < a` on `EReal`.  -/
EReal.lt_neg_comm : ∀ {a b : EReal}, a < -b ↔ b < -a
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActivateNextGuardResult.next.sizeOf_spec : ∀ (guard : Lean.Expr) (pending : List Lean.Meta.Grind.TheoremGuard),
  sizeOf (Lean.Meta.Grind.ActivateNextGuardResult.next guard pending) = 1 + sizeOf guard + sizeOf pending
-- Mathlib.Order.Hom.Basic
OrderHom.curry_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α × β →o γ) (x : α) (y : β), ((OrderHom.curry f) x) y = f (x, y)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.iSup_ucs_le_genWeightSpace_zero : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L], ⨆ k, LieSubmodule.ucs k ⊥ ≤ LieModule.genWeightSpace M 0
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.q_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E ≠ ⊥ → RatFunc.Luroth.q✝ E ≠ 0
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_add : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Add R] (a b : QuaternionAlgebra R c₁ c₂ c₃), (a + b).imJ = a.imJ + b.imJ
-- Mathlib.Probability.Moments.Basic
/-- **Chernoff bound** on the lower tail of a real random variable.  -/
ProbabilityTheory.measure_le_le_exp_mul_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ}
  [MeasureTheory.IsFiniteMeasure μ] (ε : ℝ),
  t ≤ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      μ.real {ω | X ω ≤ ε} ≤ Real.exp (-t * ε) * ProbabilityTheory.mgf X μ t
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.map_proj_nhds : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {E : B → Type u_5}
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  (x : Bundle.TotalSpace F E), Filter.map Bundle.TotalSpace.proj (nhds x) = nhds x.proj
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.instFullModuleCatFunctor : ∀ (R : Type (u + 1)) [inst : Ring R], (CondensedMod.LocallyConstant.functor R).Full
-- Init.Data.List.Lemmas
List.dropLast_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, (l₁ ++ l₂).dropLast = if l₂.isEmpty = true then l₁.dropLast else l₁ ++ l₂.dropLast
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_mul : ∀ (x : ENNReal) (y z : ℝ), x ^ (y * z) = (x ^ y) ^ z
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
UniqueMDiffOn.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (s : Set M), UniqueMDiff[s] = ∀ x ∈ s, UniqueMDiffAt[s] x
-- Mathlib.CategoryTheory.Presentable.Type
HasCardinalLT.Set.instIsCardinalFiltered : ∀ (X : Type u) (κ : Cardinal.{u}) [inst : Fact κ.IsRegular], CategoryTheory.IsCardinalFiltered (HasCardinalLT.Set X κ) κ
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.SeparatingRight.eq_zero_of_mulVec_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Finite m]
  [inst_2 : Fintype n], M.SeparatingRight → ∀ {v : n → R}, M.mulVec v = 0 → v = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termI₃ : Lean.ParserDescr
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
/-- One direction of the **Borel-Cantelli lemma**
(sometimes called the "*first* Borel-Cantelli lemma"):
if `(s i)` is a countable family of sets such that `∑' i, μ (s i)` is finite,
then a.e. all points belong to finitely many sets of the family.  -/
MeasureTheory.ae_finite_setOfPred_mem : ∀ {α : Type u_1} {ι : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] [Countable ι] {μ : F} {s : ι → Set α},
  ∑' (i : ι), μ (s i) ≠ ⊤ → ∀ᵐ (x : α) ∂μ, {i | x ∈ s i}.Finite
-- Mathlib.Order.CompleteLattice.Basic
iSup_of_empty' : ∀ {α : Type u_8} {ι : Sort u_9} [inst : SupSet α] [IsEmpty ι] (f : ι → α), iSup f = sSup ∅
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasStrictFDerivAt_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F},
  HasStrictFDerivAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p
-- Mathlib.Topology.Category.TopCat.Limits.Cofiltered
/-- Given a *compatible* collection of topological bases for the factors in a cofiltered limit
which contain `Set.univ` and are closed under intersections, the induced *naive* collection
of sets in the limit is, in fact, a topological basis.
 -/
TopCat.isTopologicalBasis_cofiltered_limit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [CategoryTheory.IsCofiltered J]
  (F : CategoryTheory.Functor J TopCat) (C : CategoryTheory.Limits.Cone F) (hC : CategoryTheory.Limits.IsLimit C)
  (T : (j : J) → Set (Set ↑(F.obj j))),
  (∀ (j : J), TopologicalSpace.IsTopologicalBasis (T j)) →
    (∀ (i : J), Set.univ ∈ T i) →
      (∀ (i : J) (U1 U2 : Set ↑(F.obj i)), U1 ∈ T i → U2 ∈ T i → U1 ∩ U2 ∈ T i) →
        (∀ (i j : J) (f : i ⟶ j), ∀ V ∈ T j, ⇑(CategoryTheory.ConcreteCategory.hom (F.map f)) ⁻¹' V ∈ T i) →
          TopologicalSpace.IsTopologicalBasis
            {U | ∃ j, ∃ V ∈ T j, U = ⇑(CategoryTheory.ConcreteCategory.hom (C.π.app j)) ⁻¹' V}
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- A functor from `C` to `D`  -/
CategoryTheory.HasForget₂.forget₂ : {C : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} C} →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} →
          {inst_2 : CategoryTheory.ConcreteCategory C FC} →
            {D : Type u_3} →
              {inst_3 : CategoryTheory.Category.{v_2, u_3} D} →
                {FD : outParam (D → D → Type u_4)} →
                  {CD : outParam (D → Type w)} →
                    {inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))} →
                      {inst_5 : CategoryTheory.ConcreteCategory D FD} →
                        [self : CategoryTheory.HasForget₂ C D] → CategoryTheory.Functor C D
-- Mathlib.Order.Concept
Concept.isExtent_extent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r), Order.IsExtent r c.extent
-- Mathlib.NumberTheory.RamificationInertia.Valuation
IsDedekindDomain.HeightOneSpectrum.valuation_liesOver : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) {B : Type u_4} [inst : CommRing A] [inst_1 : IsDedekindDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDedekindDomain B] [inst_4 : Algebra A B] [Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra K L] [inst_9 : Algebra A K] [inst_10 : IsFractionRing A K]
  [inst_11 : Algebra A L] [IsScalarTower A K L] [inst_13 : Algebra B L] [inst_14 : IsFractionRing B L]
  [IsScalarTower A B L] (v : IsDedekindDomain.HeightOneSpectrum A) (w : IsDedekindDomain.HeightOneSpectrum B)
  [w.asIdeal.LiesOver v.asIdeal] (x : K),
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ^ v.asIdeal.ramificationIdx' w.asIdeal =
    (IsDedekindDomain.HeightOneSpectrum.valuation L w) ((algebraMap K L) x)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.laplacian_eq_sum : ∀ {ι : Type u_1} {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E] [inst_5 : Fintype ι]
  (b : OrthonormalBasis ι ℝ E) (f : SchwartzMap E F),
  Laplacian.laplacian f = ∑ i, LineDeriv.lineDerivOp (b i) (LineDeriv.lineDerivOp (b i) f)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
cfcₙHom_nnreal_eq_restrict : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : PartialOrder A] [inst_3 : StarRing A]
  [inst_4 : StarOrderedRing A] [inst_5 : Module ℝ A] [IsSemitopologicalRing A] [inst_7 : IsScalarTower ℝ A A]
  [inst_8 : SMulCommClass ℝ A A] [T2Space A] [inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_11 : NonnegSpectrumClass ℝ A] {a : A} (ha : 0 ≤ a),
  cfcₙHom ha = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯
-- Mathlib.Analysis.Complex.CanonicalDecomposition
Complex.canonicalFactor_def : ∀ (R : ℝ) (w : ℂ), Complex.canonicalFactor R w = fun z => (↑R ^ 2 - (starRingEnd ℂ) w * z) / (↑R * (z - w))
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoOpPushout f g).inv
      (CategoryTheory.Limits.pullback.fst f g) =
    (CategoryTheory.Limits.pushout.inl f.unop g.unop).op
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.eq_1 : ∀ (R : Type u) (X : Type v) [inst : CommRing R], FreeLieAlgebra R X = Quot (FreeLieAlgebra.Rel R X)
-- Batteries.Lean.PersistentHashMap
/-- Variant of `ofArray` which accepts a function that combines values of duplicated
keys.
 -/
Lean.PersistentHashMap.ofArrayWith : {α : Type u_1} →
  [inst : BEq α] → [inst_1 : Hashable α] → {β : Type u_2} → Array (α × β) → (α → β → β → β) → Lean.PersistentHashMap α β
-- Mathlib.RingTheory.Localization.Module
LinearMap.extendScalarsOfIsLocalization_apply : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (f : M →ₗ[A] N),
  LinearMap.extendScalarsOfIsLocalization S A (↑R f) = f
-- Mathlib.Order.Sublattice
Sublattice.top_prod_top : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β], ⊤.prod ⊤ = ⊤
-- Init.Data.UInt.Lemmas
USize.ofFin_sub : ∀ (a b : Fin USize.size), USize.ofFin (a - b) = USize.ofFin a - USize.ofFin b
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMap'_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData),
  CategoryTheory.ShortComplex.homologyMap' (CategoryTheory.CategoryStruct.id S) h h =
    CategoryTheory.CategoryStruct.id h.left.H
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.algebraMap_C_mem_adicCompletionIntegers : ∀ (K : Type u_2) [inst : Field K] (x : K),
  ((LaurentSeries.LaurentSeriesRingEquiv K).toRingHom.comp HahnSeries.C) x ∈
    IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers (RatFunc K) (Polynomial.idealX K)
-- Mathlib.Order.Booleanisation
/-- The order on `Booleanisation α` is as follows: For `a b : α`,
* `a ≤ b` iff `a ≤ b` in `α`
* `a ≤ bᶜ` iff `a` and `b` are disjoint in `α`
* `aᶜ ≤ bᶜ` iff `b ≤ a` in `α`
* `¬ aᶜ ≤ b`  -/
Booleanisation.LE : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → Booleanisation α → Booleanisation α → Prop
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.labelledStar.sizeOf_spec : ∀ (id : ℕ), sizeOf (Lean.Meta.RefinedDiscrTree.Key.labelledStar id) = 1 + sizeOf id
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- The monad induced by the Eilenberg-Moore adjunction is the original monad.  -/
CategoryTheory.Adjunction.adjToMonadIso : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → (T : CategoryTheory.Monad C) → T.adj.toMonad ≅ T
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_sub : ∀ {α : Type u_1} [inst : Sub α] (a b : α), SymAlg.sym (a - b) = SymAlg.sym a - SymAlg.sym b
-- Init.Data.String.Decode
ByteArray.utf8Size_utf8DecodeChar : ∀ {b : ByteArray} {i : ℕ} {h : (b.utf8DecodeChar? i).isSome = true},
  (b.utf8DecodeChar i h).utf8Size = b[i].utf8ByteSize ⋯
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.mem_span_repr_support : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (m : M), m ∈ Submodule.span R (⇑b '' ↑(b.repr m).support)
-- Mathlib.Data.EReal.Basic
EReal.coe_toENNReal : ∀ {x : EReal}, 0 ≤ x → ↑x.toENNReal = x
-- Mathlib.Analysis.Calculus.Deriv.Basic
DifferentiableWithinAt.hasDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x → HasDerivWithinAt f (derivWithin f s x) s x
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.stepBound_pos_iff : ∀ {n : ℕ}, 0 < SzemerediRegularity.stepBound n ↔ 0 < n
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.nonempty_indParallelPairPresentation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)},
  CategoryTheory.Limits.IsIndObject A →
    CategoryTheory.Limits.IsIndObject B → ∀ (f g : A ⟶ B), Nonempty (CategoryTheory.IndParallelPairPresentation f g)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_iff_isSome_getKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∈ t ↔ (t.getKey? a).isSome = true
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNormClass.mk : ∀ {F : Type u_6} {α : outParam (Type u_7)} [inst : AddGroup α] [inst_1 : FunLike F α ℝ]
  [toNonarchAddGroupSeminormClass : NonarchAddGroupSeminormClass F α],
  (∀ (f : F) {a : α}, f a = 0 → a = 0) → NonarchAddGroupNormClass F α
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.exists_dual_map_eq_bot_of_notMem : ∀ {R : Type u_3} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  {x : M}, x ∉ p → Module.Projective R (M ⧸ p) → ∃ f, f x ≠ 0 ∧ Submodule.map f p = ⊥
-- Mathlib.ModelTheory.ElementaryMaps
/-- An elementary embedding of first-order structures is an embedding that commutes with the
realizations of formulas.  -/
FirstOrder.Language.ElementaryEmbedding : (L : FirstOrder.Language) → (M : Type u_1) → (N : Type u_2) → [L.Structure M] → [L.Structure N] → Type (max u_1 u_2)
-- Mathlib.Algebra.Order.Module.Field
smul_inv_lt_iff_of_neg : ∀ {𝕜 : Type u_1} {G : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup G] [inst_4 : PartialOrder G] [IsOrderedAddMonoid G] [inst_6 : Module 𝕜 G] {a : 𝕜} {b₁ b₂ : G}
  [PosSMulStrictMono 𝕜 G], a < 0 → (b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.mem_lift_of_roots_mem_range : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits →
    f.Monic → ∀ {S : Type u_4} [inst_2 : Ring S] (i : S →+* R), (∀ a ∈ f.roots, a ∈ i.range) → f ∈ Polynomial.lifts i
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.simplicialCosimplicialEquiv_functor_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : (CategoryTheory.Functor SimplexCategoryᵒᵖ C)ᵒᵖ}
  (η : X ⟶ Y) (x : SimplexCategory),
  ((CategoryTheory.simplicialCosimplicialEquiv C).functor.map η).app x = (η.unop.app (Opposite.op x)).op
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instDiv : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : Group γ] → [IsTopologicalGroup γ] → Div (α →ₘ[μ] γ)
-- Mathlib.Computability.StateTransition
StateTransition.EvalsTo.mk.injEq : ∀ {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} (steps : ℕ)
  (evals_in_steps : (flip bind f)^[steps] (some a) = b) (steps_1 : ℕ)
  (evals_in_steps_1 : (flip bind f)^[steps_1] (some a) = b),
  ({ steps := steps, evals_in_steps := evals_in_steps } = { steps := steps_1, evals_in_steps := evals_in_steps_1 }) =
    (steps = steps_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.keys_insertIfNew_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : BEq α]
  [Std.TransCmp cmp] [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys)