mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.star_mul_self_eq_zero_iff : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] (x : E), star x * x = 0 ↔ x = 0
-- Init.Data.SInt.Lemmas
Int32.lt_iff_toInt_lt : ∀ {x y : Int32}, x < y ↔ x.toInt < y.toInt
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.instModuleQuotientIdealSubtypeMemTorsionBySetCoe : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (I : Ideal R) → Module (R ⧸ I) ↥(Submodule.torsionBySet R M ↑I)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.prepartition.eq_1 : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] (B : BoxIntegral.Box ι),
  BoxIntegral.unitPartition.prepartition n B =
    {
      boxes :=
        Finset.image (fun ν => BoxIntegral.unitPartition.box n ν) (BoxIntegral.unitPartition.admissibleIndex n B),
      le_of_mem' := ⋯, pairwiseDisjoint := ⋯,
      tag := fun I =>
        if hI : ∃ ν ∈ BoxIntegral.unitPartition.admissibleIndex n B, I = BoxIntegral.unitPartition.box n ν then
          BoxIntegral.unitPartition.tag n hI.choose
        else ⋯.choose,
      tag_mem_Icc := ⋯ }
-- Mathlib.Combinatorics.Additive.Dissociation
MulDissociated.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] (s : Set α), MulDissociated s = Set.InjOn (fun x => ∏ x ∈ x, x) {t | ↑t ⊆ s}
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.map_obj_fiber : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G)
  (a : F.CoGrothendieck),
  ((CategoryTheory.Pseudofunctor.CoGrothendieck.map α).obj a).fiber =
    (α.app { as := Opposite.op a.base }).toFunctor.obj a.fiber
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_subset_sub_left : ∀ {α : Type u_2} [inst : Sub α] {s t₁ t₂ : Set α}, t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
/-- As it is unclear whether the opposite category `Cᵒᵖ` should always be equipped
with the shift by `ℤ` such that shifting by `n` on `Cᵒᵖ` corresponds to shifting
by `-n` on `C`, the user shall have to do `open CategoryTheory.Pretriangulated.Opposite`
in order to get this shift and the (pre)triangulated structure on `Cᵒᵖ`.  -/
_private.Mathlib.CategoryTheory.Triangulated.Opposite.Basic.0.CategoryTheory.Pretriangulated.Opposite.OppositeShiftAux : (C : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.HasShift C ℤ] → Type u_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₂ → k ∈ m₁
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.analyticWithinAt_bilinear : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)) (x : E × F),
  AnalyticWithinAt 𝕜 (fun x => (f x.1) x.2) s x
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
le_liminf_add : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommGroup α] [inst_1 : ConditionallyCompleteLinearOrder α] [DenselyOrdered α]
  [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) le_liminf_add._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) le_liminf_add._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) le_liminf_add._auto_5 →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) le_liminf_add._auto_7 →
          Filter.liminf u f + Filter.liminf v f ≤ Filter.liminf (u + v) f
-- Mathlib.Topology.Filter
Filter.tendsto_nhds_atBot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder β] {l : Filter α} {f : α → Filter β},
  Filter.Tendsto f l (nhds Filter.atBot) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Set.Iic y ∈ f a
-- Mathlib.Data.Fin.Tuple.Basic
Fin.succAboveCases.eq_1 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j))
  (j : Fin (n + 1)),
  i.succAboveCases x p j = if hj : j = i then ⋯ ▸ x else if hlt : j < i then ⋯ ▸ p (j.castPred ⋯) else ⋯ ▸ p (j.pred ⋯)
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.familyOfElements_isCompatible : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1}
  {Y : I → C} {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y},
  x.IsCompatible → ∀ (X : C), (x.familyOfElements X).Compatible
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.homeoOfIso_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (x : ↥X), (AlgebraicGeometry.Scheme.homeoOfIso e) x = e.hom x
-- Mathlib.Combinatorics.Additive.Dissociation
/-- **Alias** of the forward direction of `addDissociated_neg`. -/
AddDissociated.of_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] {s : Set α}, AddDissociated (-s) → AddDissociated s
-- Mathlib.Topology.Algebra.Module.Equiv
/-- A continuous linear map is invertible if it is the forward direction of a continuous linear
equivalence.  -/
ContinuousLinearMap.IsInvertible : {R : Type u_1} →
  {M : Type u_2} →
    {M₂ : Type u_3} →
      [inst : TopologicalSpace M] →
        [inst_1 : TopologicalSpace M₂] →
          [inst_2 : Semiring R] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] → [inst_5 : AddCommMonoid M₂] → [inst_6 : Module R M₂] → (M →L[R] M₂) → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_sub_nat_mul_two_pi : ∀ (x : ℝ) (n : ℕ), Real.sin (x - ↑n * (2 * Real.pi)) = Real.sin x
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.hasFunctorialFactorization : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [I.IsCardinalForSmallObjectArgument κ],
  I.rlp.llp.HasFunctorialFactorization I.rlp
-- Mathlib.Data.Set.Card
Set.ncard_le_encard : ∀ {α : Type u_1} (s : Set α), ↑s.ncard ≤ s.encard
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_eq_one : ∀ {α : Type u_2} [inst : One α] {s : Finset α}, ↑s = 1 ↔ s = 1
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instLattice : {R : Type u_2} →
  {N : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : TopologicalSpace N] →
          [inst_3 : Module R N] → [ContinuousAdd N] → [ContinuousConstSMul R N] → Lattice (ClosedSubmodule R N)
-- Std.Http.Data.URI.Basic
Std.Http.RequestTarget.absoluteForm.injEq : ∀ (uri uri_1 : Std.Http.URI),
  (Std.Http.RequestTarget.absoluteForm uri = Std.Http.RequestTarget.absoluteForm uri_1) = (uri = uri_1)
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.preservesColimitsOfSize_algΓ : ∀ {R : CommRingCat}, CategoryTheory.Limits.PreservesColimitsOfSize.{w, v, u, u, u + 1, u + 1} (AlgebraicGeometry.algΓ R)
-- Init.Prelude
/-- `expandMacro? stx` returns `some stxNew` if `stx` is a macro,
and `stxNew` is its expansion.
 -/
Lean.Macro.expandMacro? : Lean.Syntax → Lean.MacroM (Option Lean.Syntax)
-- Mathlib.Algebra.Module.Submodule.Map
LinearMap.map_codRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₂₁ : R₂ →+* R}
  [inst_6 : RingHomSurjective σ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h : ∀ (c : M₂), f c ∈ p)
  (p' : Submodule R₂ M₂),
  Submodule.map (LinearMap.codRestrict p f h) p' = Submodule.comap p.subtype (Submodule.map f p')
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.notMem_simplex : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (hx : SSet.prodStdSimplex.pairingCore.IsType₂ x) {d : ℕ} (hd : x.dim = d),
  hx.simplex hd ∉ ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).obj (Opposite.op { len := d + 1 })
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.algebraMap_snd : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (k : 𝕜),
  ((algebraMap 𝕜 (DoubleCentralizer 𝕜 A)) k).toProd.2 = (algebraMap 𝕜 (A →L[𝕜] A)) k
-- Mathlib.NumberTheory.Real.Irrational
Irrational.inv : ∀ {x : ℝ}, Irrational x → Irrational x⁻¹
-- Lean.Meta.PProdN
/-- Given a value `e` of type `t = t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ`  -/
Lean.Meta.PProdN.proj : ℕ → ℕ → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.RingTheory.LocalProperties.Submodule
Module.eq_of_isLocalized_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_3 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_4 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (x y : M),
      (∀ (r : ↑s), (f r) x = (f r) y) → x = y
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P]
  {Φ :
    CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂})}
  {f g :
    CategoryTheory.Functor.LeftExtension.mk F.op.lan
        (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶
      Φ},
  f = g ↔ True
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.presheafHomObjHomEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  {M N : ↑(F.obj { as := Opposite.op S })}
  (f :
    (F.map
              (Opposite.unop
                      (Opposite.op
                        (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S)))).hom.op.toLoc).toFunctor.obj
        M ⟶
      (F.map
              (Opposite.unop
                      (Opposite.op
                        (CategoryTheory.Over.mk (CategoryTheory.CategoryStruct.id S)))).hom.op.toLoc).toFunctor.obj
        N),
  F.presheafHomObjHomEquiv.symm f =
    CategoryTheory.CategoryStruct.comp ((F.mapId { as := Opposite.op S }).inv.toNatTrans.app M)
      (CategoryTheory.CategoryStruct.comp f ((F.mapId { as := Opposite.op S }).hom.toNatTrans.app N))
-- Plausible.Gen
Plausible.Gen.inhabitedGen : {α : Type u_1} → Inhabited (Plausible.Gen α)
-- Mathlib.Topology.Maps.Basic
Topology.IsQuotientMap.of_comp_isQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsQuotientMap f → Topology.IsQuotientMap (g ∘ f) → Topology.IsQuotientMap g
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The cosine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
adjacent side.  -/
EuclideanGeometry.cos_angle_mul_dist_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 → Real.cos (EuclideanGeometry.angle p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
-- Mathlib.Data.PNat.Order
PNat.succ_eq_add_one : ∀ (n : ℕ+), Order.succ n = n + 1
-- Mathlib.Order.Filter.Prod
Filter.prod_mono_left : ∀ {α : Type u_1} {β : Type u_2} (g : Filter β) {f₁ f₂ : Filter α}, f₁ ≤ f₂ → f₁ ×ˢ g ≤ f₂ ×ˢ g
-- Init.Grind.Ordered.Ring
/-- A ring which is also equipped with a preorder is considered a strict ordered ring if addition, negation,
and multiplication are compatible with the preorder, and `0 < 1`.
 -/
Lean.Grind.OrderedRing : (R : Type u) → [Lean.Grind.Semiring R] → [inst : LE R] → [LT R] → [Std.IsPreorder R] → Prop
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) ↔ ∃ a, (a, b, c) ∈ t
-- Mathlib.NumberTheory.Dioph
/-- The set of places where two Diophantine functions are unequal is Diophantine.  -/
Dioph.«term_D≠_» : Lean.TrailingParserDescr
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_ofBitVec : ∀ {b : BitVec 8}, { toBitVec := b }.toUInt64 = { toBitVec := BitVec.setWidth 64 b }
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.isoModSerre.HasTwoOutOfThreeProperty
-- Init.Data.List.Lemmas
List.all_replicate : ∀ {α : Type u_1} {f : α → Bool} {n : ℕ} {a : α}, (List.replicate n a).all f = if n = 0 then true else f a
-- Lean.Meta.Basic
/-- `withResetZetaDeltaFVarIds x` executes `x` in a context where the `zetaDeltaFVarIds` is temporarily cleared.

**Warning:** This does not reset the cache.
 -/
_private.Lean.Meta.Basic.0.Lean.Meta.withResetZetaDeltaFVarIds : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.mk.sizeOf_spec : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : SizeOf G] (toSubgroup : Subgroup G)
  (isClosed' : IsClosed toSubgroup.carrier),
  sizeOf { toSubgroup := toSubgroup, isClosed' := isClosed' } = 1 + sizeOf toSubgroup + sizeOf isClosed'
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instSub : {R : Type u_3} → {c₁ c₂ c₃ : R} → [AddGroup R] → Sub (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Order.Category.HeytAlg
/-- Construct a bundled `HeytAlg` from the underlying type and typeclass.  -/
HeytAlg.of : (X : Type u_1) → [HeytingAlgebra X] → HeytAlg
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.ChainComplex.augment.match_3.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (h_1 : Unit → motive 1 0) (h_2 : (i j : ℕ) → motive i.succ j.succ)
  (h_3 : (x x_1 : ℕ) → motive x x_1),
  (match 1, 0 with
    | 1, 0 => h_1 ()
    | i.succ, j.succ => h_2 i j
    | x, x_1 => h_3 x x_1) =
    h_1 ()
-- Lean.Compiler.IR.Format
Lean.IR.instToFormatExpr : Std.ToFormat Lean.IR.Expr
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.eq_iff_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) (g : S.LocalizationMap P) {x y : M}, f x = f y ↔ g x = g y
-- Init.Data.Array.Find
Array.findIdx?_map : ∀ {β : Type u_1} {α : Type u_2} {f : β → α} {xs : Array β} {p : α → Bool},
  Array.findIdx? p (Array.map f xs) = Array.findIdx? (p ∘ f) xs
-- Std.Data.ExtTreeMap.Basic
/-- Returns `true` if there is a mapping for the given key `a` or a key that is equal to `a` according
to the comparator `cmp`. There is also a `Prop`-valued version
of this: `a ∈ t` is equivalent to `t.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for equality checks, while for tree maps, both use the given comparator `cmp`.
 -/
Std.ExtTreeMap.contains : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Bool
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.curry_two_eq_curry : ∀ {p : Fin 2 → Type u} {τ : Type u} (f : ((i : Fin 2) → p i) → τ),
  Function.FromTypes.curry f = Function.curry (f ∘ ⇑(piFinTwoEquiv p).symm)
-- Lean.Meta.Basic
Lean.Meta.withInTypeClassResolution : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_symm_apply_val : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.Functor Cᵒᵖ (Type u_3)) (s : Subtype (CategoryTheory.Presieve.Arrows.Compatible F E.f))
  (i : E.I₀), ((E.sectionsSaturateEquiv F).symm s).val i = ↑s i
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Map from `ℍ` to `SL(2, ℝ)`, giving a continuous section of the map `g ↦ g • I`.  -/
UpperHalfPlane.toSL2R : UpperHalfPlane → Matrix.SpecialLinearGroup (Fin 2) ℝ
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Returns an `Int` that is close to the given `(sign, mantissa, exponent)` triple. Specifically, we
round to zero rather than rounding to nearest like we do everywhere else.
 -/
Float.Model.UnpackedFloat.roundToInt : Float.Model.UnpackedFloat.Sign → ℕ → ℤ → ℤ
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.whiskerLeft_comp_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] (x : C) {y y' : C}
  (g : y ⟶ y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x) (G.map g))
      ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y')) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x g))
-- Lean.Server.ServerTask
Lean.Server.ServerTask.BaseIO.mapTaskCheap : {α : Type u_1} → {β : Type} → (α → BaseIO β) → Lean.Server.ServerTask α → BaseIO (Lean.Server.ServerTask β)
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_eq_empty : ∀ {α : Type u_1} [inst : LE α] {s : UpperSet α}, ↑s = ∅ ↔ s = ⊤
-- Mathlib.Order.Bounds.Basic
bddBelow_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, BddBelow (Set.Ici a)
-- Mathlib.Analysis.RCLike.Basic
RCLike.algebraMap_eq_ofReal : ∀ {K : Type u_1} [inst : RCLike K], ⇑(algebraMap ℝ K) = RCLike.ofReal
-- Mathlib.Combinatorics.Graph.Simple
Graph.Inc.isNonloopAt : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {e : β} [G.Loopless], G.Inc e u → G.IsNonloopAt e u
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instModule' : {R' : Type u'} →
  {R : Type u} →
    {A : Type v} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            {S : NonUnitalSubalgebra R A} →
              [inst_3 : Semiring R'] →
                [inst_4 : SMul R' R] → [inst_5 : Module R' A] → [IsScalarTower R' R A] → Module R' ↥S
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- Construct an element of `(F ⨯ G).obj a` from an element of `F.obj a` and
an element of `G.obj a`.  -/
CategoryTheory.FunctorToTypes.prodMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor C (Type w)} → {a : C} → F.obj a → G.obj a → (F ⨯ G).obj a
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_sub_right : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {x y z : E},
  inner A x (y - z) = inner A x y - inner A x z
-- Mathlib.SetTheory.Ordinal.Notation
ONote.cmp.eq_3 : ∀ (x : ONote), (x = ONote.zero → False) → ONote.zero.cmp x = Ordering.lt
-- Mathlib.Computability.Primrec.List
List.lookup.eq_def : ∀ {α : Type u} {β : Type v} [inst : BEq α] (x : α) (x_1 : List (α × β)),
  List.lookup x x_1 =
    match x, x_1 with
    | x, [] => none
    | a, (k, b) :: as =>
      match a == k with
      | true => some b
      | false => List.lookup a as
-- Mathlib.Data.Set.Image
Set.range_inr_inter_range_inl : ∀ {α : Type u_1} {β : Type u_2}, Set.range Sum.inr ∩ Set.range Sum.inl = ∅
-- Mathlib.Geometry.Polygon.Basic
Polygon.mk : {P : Type u_1} → {n : ℕ} → (Fin n → P) → Polygon P n
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The embedding of a unital magma into its magma algebra.  -/
MonoidAlgebra.of : (R : Type u_8) → (M : Type u_9) → [inst : Semiring R] → [inst_1 : MulOneClass M] → M →* MonoidAlgebra R M
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_associator_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X Y Z : P.FullSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).hom
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- A bounded bilinear map `f : E × F → G` defines a continuous linear map
`f : E →L[𝕜] F →L[𝕜] G`.  -/
IsBoundedBilinearMap.toContinuousLinearMap : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : SeminormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {G : Type u_4} →
                  [inst_5 : SeminormedAddCommGroup G] →
                    [inst_6 : NormedSpace 𝕜 G] → {f : E × F → G} → IsBoundedBilinearMap 𝕜 f → E →L[𝕜] F →L[𝕜] G
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsCocircuit.delete_sdiff_isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {K X : Set α}, M.IsCocircuit K → X ⊆ K → X.Nonempty → (M.delete (K \ X)).IsCocircuit X
-- Mathlib.GroupTheory.OrderOfElement
Subgroup.pow_index_mem : ∀ {G : Type u_6} [inst : Group G] (H : Subgroup G) [H.Normal] (g : G), g ^ H.index ∈ H
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_conjTranspose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {j : n} {c : m → α} [inst : DecidableEq n]
  [inst_1 : Star α], M.conjTranspose.updateRow j (star c) = (M.updateCol j c).conjTranspose