mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.isPreconnected_of_subsingleton : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [Subsingleton J], CategoryTheory.IsPreconnected J
-- Mathlib.Algebra.Category.FGModuleCat.Basic
instFiniteCarrier : ∀ {R : Type u} [inst : Ring R] (M : FGModuleCat R), Module.Finite R ↑M
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.whiskering_obj_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (H : CategoryTheory.Functor C D) (F : CategoryTheory.Functor SimplexCategoryᵒᵖ C) {X Y : SimplexCategoryᵒᵖ}
  (f : X ⟶ Y), (((CategoryTheory.SimplicialObject.whiskering C D).obj H).obj F).map f = H.map (F.map f)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.piFinTwo_symm_apply : ∀ (α : Fin 2 → Type u_3) [inst : (i : Fin 2) → PseudoEMetricSpace (α i)] (p : α 0 × α 1) (i : Fin (1 + 1)),
  (IsometryEquiv.piFinTwo α).symm p i = Fin.cons p.1 (Fin.cons p.2 finZeroElim) i
-- Mathlib.Data.Fintype.Card
Fintype.card_of_subtype : ∀ {α : Type u_1} {p : α → Prop} (s : Finset α),
  (∀ (x : α), x ∈ s ↔ p x) → ∀ [inst : Fintype { x // p x }], Fintype.card { x // p x } = s.card
-- Mathlib.LinearAlgebra.Dual.Defs
LinearMap.dualMap_apply' : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] (f : M₁ →ₗ[R] M₂) (g : Module.Dual R M₂),
  f.dualMap g = g ∘ₗ f
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.id_edge : ∀ {X : SSet.Truncated 2} (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })),
  (SSet.Truncated.Edge.id x).edge =
    (CategoryTheory.ConcreteCategory.hom
        (X.map (SimplexCategory.Truncated.σ₂ 0 SSet.Truncated.Edge._proof_3 SSet.Truncated.Edge._proof_1).op))
      x
-- Init.Data.UInt.Basic
/-- Converts an `Int` to a `UInt8` by taking the (non-negative remainder of the division by `2 ^ 8`.  -/
UInt8.ofInt : ℤ → UInt8
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPFst_comp_swap : pointedToTwoPFst.comp TwoP.swap = pointedToTwoPSnd
-- Mathlib.Tactic.ClickSuggestions
/-- Compute the suggestions. Use `token` for the output.  -/
Mathlib.Tactic.ClickSuggestions.generateSuggestions : Lean.SubExpr.GoalsLocation →
  Option Lean.Name → ProofWidgets.RefreshToken → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM Unit
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeUnopOfIsClosedUnderColimitsOfShapeOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] (Q : CategoryTheory.ObjectProperty Cᵒᵖ)
  [Q.IsClosedUnderColimitsOfShape Jᵒᵖ], Q.unop.IsClosedUnderLimitsOfShape J
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insert_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β}, Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl k = some v
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.support_weights_restrict : ∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [IsDomain K] (w : Convexity.StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0)
  [inst_4 : DecidablePred fun x => x ∈ s], (w.restrict s hs).weights.support = {x ∈ w.weights.support | x ∈ s}
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.linear_topEquiv : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P],
  (AffineSubspace.topEquiv k V P).linear = (LinearEquiv.ofEq ⊤.direction ⊤ ⋯).trans Submodule.topEquiv
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.startsWith_string_empty : ∀ {s : String.Slice}, s.startsWith "" = true
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.isFiniteMeasure : ∀ (T : ℝ) [hT : Fact (0 < T)], MeasureTheory.IsFiniteMeasure MeasureTheory.volume
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.TopSort.State.result : Lean.Elab.Term.ToDepElimPattern.TopSort.State → Array Lean.Expr
-- Mathlib.MeasureTheory.Measure.GiryMonad
Measurable.measure_of_isPiSystem_of_isProbabilityMeasure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : α → MeasureTheory.Measure β}
  [∀ (a : α), MeasureTheory.IsProbabilityMeasure (μ a)] {S : Set (Set β)},
  mβ = MeasurableSpace.generateFrom S → IsPiSystem S → (∀ s ∈ S, Measurable fun a => (μ a) s) → Measurable μ
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.not_isCyclic_units_of_mul_coprime : ∀ (m n : ℕ), Odd m → m ≠ 1 → Odd n → n ≠ 1 → m.Coprime n → ¬IsCyclic (ZMod (m * n))ˣ
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf_obj_V : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (A : CategoryTheory.Endofunctor.Algebra F),
  ((CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf adj).obj A).V = A.a
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.homToEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) {Z : C} (f : Z ⟶ X),
  α.homToEquiv f = CategoryTheory.CategoryStruct.comp f α.hom
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.isNilpotent_of_ker_le_center`.

---

The preimage of a nilpotent group is nilpotent if the kernel of the homomorphism is contained
in the center.  -/
isNilpotent_of_ker_le_center : ∀ {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] (f : G →* H),
  f.ker ≤ Subgroup.center G → ∀ [Group.IsNilpotent H], Group.IsNilpotent G
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.continuous_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (S : Submodule R M), Continuous ⇑S.mkQ
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.continuousOn_fderiv_of_isOpen : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → IsOpen s → 1 ≤ n → ContinuousOn (fderiv 𝕜 f) s
-- Init.Prelude
/-- Converts a natural number to a 32-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than `2^32`.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.ofNatLT : (n : ℕ) → n < UInt32.size → UInt32
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.instCoeSortType : CoeSort FinBddDistLat (Type u_1)
-- Mathlib.Order.SuccPred.Limit
/-- Given `i < j` with `i` a predecessor pre-limit, `IsSuccPrelimit.mid` picks an arbitrary element
strictly between `i` and `j`.  -/
Order.IsPredPrelimit.mid : {α : Type u_1} → [inst : Preorder α] → {i j : α} → Order.IsPredPrelimit i → i < j → ↑(Set.Ioo i j)
-- Mathlib.Tactic.FailIfNoProgress
_private.Mathlib.Tactic.FailIfNoProgress.0.Mathlib.Tactic.lctxIsDefEq.eq_def : ∀ (x x_1 : List (Option Lean.LocalDecl)),
  Mathlib.Tactic.lctxIsDefEq x x_1 =
    match x, x_1 with
    | none :: l₁, l₂ => Mathlib.Tactic.lctxIsDefEq l₁ l₂
    | l₁, none :: l₂ => Mathlib.Tactic.lctxIsDefEq l₁ l₂
    | some d₁ :: l₁, some d₂ :: l₂ =>
      if (d₁.isLet == d₂.isLet) = true then
        if (d₁.fvarId == d₂.fvarId) = true then do
          let __do_lift ← Lean.Meta.withNewMCtxDepth (Lean.Meta.isDefEq d₁.type d₂.type)
          if __do_lift = true then
              have __do_jp := fun __r => Mathlib.Tactic.lctxIsDefEq l₁ l₂;
              if d₁.isLet = true then do
                let __do_lift ← Lean.Meta.withNewMCtxDepth (Lean.Meta.isDefEq d₁.value d₂.value)
                if __do_lift = true then __do_jp () else pure false
              else __do_jp ()
            else pure false
        else pure false
      else pure false
    | [], [] => pure true
    | x, x_2 => pure false
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.comp_removeZero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G]
  (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F), q.comp p.removeZero = q.comp p
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.xgcdAux_val : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (x y : R),
  EuclideanDomain.xgcdAux x 1 0 y 0 1 = (EuclideanDomain.gcd x y, EuclideanDomain.xgcd x y)
-- Mathlib.GroupTheory.CoprodI
_private.Mathlib.GroupTheory.CoprodI.0.Monoid.CoprodI.NeWord.replaceHead.match_1.eq_1 : ∀ {ι : Type u_2} {M : ι → Type u_1} [inst : (i : ι) → Monoid (M i)]
  (motive : (x x_1 : ι) → (x_2 : M x) → x_2 ≠ 1 → Monoid.CoprodI.NeWord M x x_1 → Sort u_3) (x : ι) (x_1 : M x)
  (h : x_1 ≠ 1) (x_2 : M x) (a : x_2 ≠ 1)
  (h_1 :
    (x : ι) →
      (x_3 : M x) →
        (h : x_3 ≠ 1) → (x_4 : M x) → (a : x_4 ≠ 1) → motive x x x_3 h (Monoid.CoprodI.NeWord.singleton x_4 a))
  (h_2 :
    (x x_3 : ι) →
      (x_4 : M x) →
        (h : x_4 ≠ 1) →
          (j k : ι) →
            (w₁ : Monoid.CoprodI.NeWord M x j) →
              (hne : j ≠ k) → (w₂ : Monoid.CoprodI.NeWord M k x_3) → motive x x_3 x_4 h (w₁.append hne w₂)),
  (match x, x, x_1, h, Monoid.CoprodI.NeWord.singleton x_2 a with
    | x, .(x), x_3, h, Monoid.CoprodI.NeWord.singleton x_4 a => h_1 x x_3 h x_4 a
    | x, x_3, x_4, h, w₁.append hne w₂ => h_2 x x_3 x_4 h j k w₁ hne w₂) =
    h_1 x x_1 h x_2 a
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.map.go_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {assign : α → Bool} {inv : Bool}
  {aig : Std.Sat.AIG α} (curr : ℕ) (hcurr : curr ≤ len) (s : aig.RefVec curr) (input : aig.RefVec len)
  (f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [inst_3 : Std.Sat.AIG.RefVec.LawfulMapOperator α f]
  (start : ℕ) (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instPartialOrder : {X : Type u_1} →
  {R : Type u_3} →
    [inst : Zero X] →
      [inst_1 : Zero R] →
        [inst_2 : TopologicalSpace X] →
          [inst_3 : TopologicalSpace R] → [PartialOrder R] → PartialOrder (ContinuousMapZero X R)
-- Mathlib.Data.Matrix.Basic
AddEquiv.mapMatrix_trans : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} {γ : Type u_13} [inst : Add α] [inst_1 : Add β]
  [inst_2 : Add γ] (f : α ≃+ β) (g : β ≃+ γ), f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace),
  CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op U))
      (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.hom.base).obj U)) =
    Y.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
dist_pi_eq_iff : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  {f g : (b : β) → X b} {r : ℝ}, 0 < r → (dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r)
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.continuousOn_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, edist a b < δ → edist (f a) (f b) < ε
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulCommClassMonoidHom : ∀ {M : Type u_5} {M' : Type u_6} {A : Type u_7} {B : Type u_8} [inst : Monoid M] [inst_1 : Monoid A]
  [inst_2 : MulDistribMulAction M A] [inst_3 : MulOneClass B] [inst_4 : Monoid M'] [inst_5 : MulDistribMulAction M' A]
  [SMulCommClass M M' A], SMulCommClass Mᵈᵐᵃ M'ᵈᵐᵃ (A →* B)
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.comp_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : NonUnitalNonAssocSemiring C] [inst_5 : Star C]
  [inst_6 : NonUnitalNonAssocSemiring D] [inst_7 : Star D] (f : C →⋆ₙ+* D) (g : B →⋆ₙ+* C) (h : A →⋆ₙ+* B),
  (f.comp g).comp h = f.comp (g.comp h)
-- Lean.Level
Lean.Level.PP.Context.mvars : Lean.Level.PP.Context → Bool
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
/-- Non-unital star algebra homomorphisms are completely positive.  -/
NonUnitalStarAlgHomClass.instCompletelyPositiveMapClass : ∀ {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂]
  [inst_6 : FunLike F A₁ A₂] [NonUnitalAlgHomClass F ℂ A₁ A₂] [StarHomClass F A₁ A₂], CompletelyPositiveMapClass F A₁ A₂
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
IsPurelyInseparable.elemExponent_def : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] (a : L),
  a ^ ringExpChar K ^ IsPurelyInseparable.elemExponent K a ∈ (algebraMap K L).range
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasStrictFDerivAt.isThetaTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x → Topology.IsInducing ⇑f' → (fun p => f p.1 - f p.2) =Θ[𝕜; nhds (x, x)] fun p => p.1 - p.2
-- Mathlib.Data.ENat.Basic
ENat.natCast_toNat_eq_self : ∀ {n : ℕ∞}, ↑n.toNat = n ↔ n ≠ ⊤
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_monoidHom_injective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B], Function.Injective MonoidHomClass.toMonoidHom
-- Mathlib.Topology.UniformSpace.Completion
/-- The isomorphism between the completion of a uniform space and the completion of its separation
quotient.  -/
UniformSpace.Completion.completionSeparationQuotientEquiv : (α : Type u) → [inst : UniformSpace α] → UniformSpace.Completion (SeparationQuotient α) ≃ UniformSpace.Completion α
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Convert a (dependently typed) matrix to a morphism of biproducts.  -/
CategoryTheory.Limits.biproduct.matrix : {J : Type} →
  [inst : Finite J] →
    {K : Type} →
      [inst_1 : Finite K] →
        {C : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} C] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] →
              [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] →
                {f : J → C} → {g : K → C} → ((j : J) → (k : K) → f j ⟶ g k) → (⨁ f ⟶ ⨁ g)
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coprod_unique : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] (f : M × N →+ P),
  (f.comp (AddMonoidHom.inl M N)).coprod (f.comp (AddMonoidHom.inr M N)) = f
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_convexCombPair_comm : ∀ {R : Type u_9} {M : Type u_10} {I : Type u_11} [inst : PartialOrder R] [inst_1 : CommSemiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t)
  (h : s + t = 1) (f : Convexity.StdSimplex R I) (e₁ e₂ : I → M),
  (Convexity.iConvexComb f fun x => Convexity.convexCombPair s t hs ht h (e₁ x) (e₂ x)) =
    Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb f e₁) (Convexity.iConvexComb f e₂)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Moebius
IsUnit.moebius_eq : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α},
  IsUnit a → UniqueFactorizationMonoid.moebius a = 1
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_finsetSum_measure : ∀ {α : Type u_1} {ε : Type u_5} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  [TopologicalSpace.PseudoMetrizableSpace ε] {ι : Type u_8} {m : MeasurableSpace α} {f : α → ε}
  {μ : ι → MeasureTheory.Measure α} {s : Finset ι},
  MeasureTheory.Integrable f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, MeasureTheory.Integrable f (μ i)
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.instIsProbabilityMeasureBernoulliMeasure : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} {p : ↑unitInterval},
  MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.bernoulliMeasure x y p)
-- Mathlib.Data.Nat.Pairing
Nat.pair_unpair : ∀ (n : ℕ), Nat.pair (Nat.unpair n).1 (Nat.unpair n).2 = n
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Subtracting two points in the affine span produces a vector in the spanning submodule.  -/
vsub_mem_vectorSpan_of_mem_spanPoints_of_mem_spanPoints : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P} {p₁ p₂ : P},
  p₁ ∈ spanPoints k s → p₂ ∈ spanPoints k s → p₁ -ᵥ p₂ ∈ vectorSpan k s
-- Mathlib.Data.Nat.Squarefree
_private.Mathlib.Data.Nat.Squarefree.0.Nat.MinSqFacProp.match_1.eq_1 : ∀ (motive : Option ℕ → Sort u_1) (h_1 : Unit → motive none) (h_2 : (d : ℕ) → motive (some d)),
  (match none with
    | none => h_1 ()
    | some d => h_2 d) =
    h_1 ()
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete : ∀ (R : Type (u + 1)) [inst : Ring R], (Condensed.discrete (ModuleCat R)).Full
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.deriv_smul_ne_zero : ∀ {g : GL (Fin 2) ℝ}, 0 < (↑g).det → ∀ (τ : UpperHalfPlane), deriv (fun z => ↑(g • ↑UpperHalfPlane.ofComplex z)) ↑τ ≠ 0
-- Mathlib.RingTheory.AdicCompletion.Completeness
_private.Mathlib.RingTheory.AdicCompletion.Completeness.0.AdicCompletion.lsum_smul_comp_finsuppLEquivDirectSum_symm : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {ι : Type u_3} [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (f : ι → R),
  ((Finsupp.lsum (AdicCompletion I R)) fun i => (algebraMap R (AdicCompletion I R)) (f i) • LinearMap.id) ∘ₗ
      ↑(finsuppLEquivDirectSum (AdicCompletion I R) (AdicCompletion I M) ι).symm =
    (AdicCompletion.map I ((Finsupp.lsum R) fun i => f i • LinearMap.id) ∘ₗ
        AdicCompletion.map I ↑(finsuppLEquivDirectSum R M ι).symm) ∘ₗ
      ↑(AdicCompletion.sumEquivOfFintype I fun x => M)
-- Lean.MetavarContext
Lean.MetavarContext.UnivMVarParamResult.mctx : Lean.MetavarContext.UnivMVarParamResult → Lean.MetavarContext
-- Mathlib.Order.Hom.Lattice
SupHom.instTop : {α : Type u_2} → {β : Type u_3} → [inst : Max α] → [inst_1 : SemilatticeSup β] → [Top β] → Top (SupHom α β)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → ∀ {h : k' ∈ Std.DHashMap.ofList l}, (Std.DHashMap.ofList l).get k' h = cast ⋯ v
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- A linearly independent family of nonzero vectors gives an independent family of points
in projective space.  -/
Projectivization.Independent : {ι : Type u_1} →
  {K : Type u_2} →
    {V : Type u_3} →
      [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [inst_2 : Module K V] → (ι → Projectivization K V) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.fromSubtype.eq_1 : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)],
  CategoryTheory.Limits.biproduct.fromSubtype f p =
    CategoryTheory.Limits.biproduct.desc fun j => CategoryTheory.Limits.biproduct.ι f ↑j
-- Mathlib.Algebra.Order.CauSeq.Completion
/-- The limit of a Cauchy sequence in a complete ring. Chosen non-computably.  -/
CauSeq.lim : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] →
            {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → [CauSeq.IsComplete β abv] → CauSeq β abv → β
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey! k' = k
-- Lean.Data.FuzzyMatching
/-- Represents the role of a character inside a word.  -/
Lean.FuzzyMatching.CharRole : Type
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.continuous_reflTransSymmAux : Continuous Path.Homotopy.reflTransSymmAux
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.mdifferentiableAt_proj : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {p : Bundle.TotalSpace F E},
  MDiffAt Bundle.TotalSpace.proj p
-- Mathlib.Topology.ContinuousMap.Basic
/-- The bijection `C(X₁, Y₁) ≃ C(X₂, Y₂)` induced by homeomorphisms
`e : X₁ ≃ₜ X₂` and `e' : Y₁ ≃ₜ Y₂`.  -/
Homeomorph.continuousMapCongr : {X₁ : Type u_5} →
  {X₂ : Type u_6} →
    {Y₁ : Type u_7} →
      {Y₂ : Type u_8} →
        [inst : TopologicalSpace X₁] →
          [inst_1 : TopologicalSpace X₂] →
            [inst_2 : TopologicalSpace Y₁] →
              [inst_3 : TopologicalSpace Y₂] → X₁ ≃ₜ X₂ → Y₁ ≃ₜ Y₂ → C(X₁, Y₁) ≃ C(X₂, Y₂)
-- Mathlib.Condensed.Light.Basic
/-- **Alias** of `LightCondensed.comp_hom`. -/
LightCondensed.comp_val : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] {X Y Z : LightCondensed C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- **Alias** of `NumberField.InfinitePlace.fintype`. -/
NumberField.InfinitePlace.NumberField.InfinitePlace.fintype : {K : Type u_1} → [inst : Field K] → [NumberField K] → Fintype (NumberField.InfinitePlace K)