mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderExtensions : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsSerreClass], P.IsClosedUnderExtensions
-- Mathlib.Data.Real.Pointwise
Real.mul_iSup_of_nonneg : ∀ {ι : Sort u_1} {r : ℝ}, 0 ≤ r → ∀ (f : ι → ℝ), r * ⨆ i, f i = ⨆ i, r * f i
-- Lean.Expr
Lean.mkMDataEx : Lean.MData → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_lt_iff_lt_one_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [PosMulStrictMono α]
  [PosMulReflectLT α], 0 < a → (a * b < a ↔ b < 1)
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.revCompRevIso_inv_app : ∀ (X : SimplexCategory), SimplexCategory.revCompRevIso.inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.GroupWithZero.Units.Basic
zpow_natCast_sub_natCast₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (m n : ℕ), a ^ (↑m - ↑n) = a ^ m / a ^ n
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.instIsRightAdjointStar : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
  (CategoryTheory.Over.star X).IsRightAdjoint
-- Mathlib.Data.Set.Piecewise
Set.piecewise_op₂ : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)]
  {δ' : α → Sort u_8} {δ'' : α → Sort u_9} (f' g' : (i : α) → δ' i) (h : (i : α) → δ i → δ' i → δ'' i),
  (s.piecewise (fun x => h x (f x) (f' x)) fun x => h x (g x) (g' x)) = fun x =>
    h x (s.piecewise f g x) (s.piecewise f' g' x)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.InjectiveInfo.mk.inj : ∀ {us : List Lean.Level} {α β h : Lean.Expr} {inv? : Option (Lean.Expr × Lean.Expr)} {us_1 : List Lean.Level}
  {α_1 β_1 h_1 : Lean.Expr} {inv?_1 : Option (Lean.Expr × Lean.Expr)},
  { us := us, α := α, β := β, h := h, inv? := inv? } = { us := us_1, α := α_1, β := β_1, h := h_1, inv? := inv?_1 } →
    us = us_1 ∧ α = α_1 ∧ β = β_1 ∧ h = h_1 ∧ inv? = inv?_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertMany_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          Std.DTreeMap.Internal.Impl.Const.getD
              (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)) k' fallback =
            v
-- Init.Data.List.Basic
List.concat.eq_2 : ∀ {α : Type u} (x a : α) (as : List α), (a :: as).concat x = a :: as.concat x
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement'.QuotientMulEquiv_symm_apply : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [inst_1 : K.Normal] (h : H.IsComplement' K) (a : ↥H),
  h.QuotientMulEquiv.symm a = (Subgroup.IsComplement.leftQuotientEquiv h).symm a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_diff_le_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ \ m₂).size ≤ m₁.size
-- Init.Data.Rat.Lemmas
Rat.mul_lt_mul_left : ∀ {a b c : ℚ}, 0 < c → (c * a < c * b ↔ a < b)
-- Mathlib.Analysis.CStarAlgebra.Unitization
ContinuousLinearMap.isometry_mul_flip : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing E]
  [inst_2 : StarRing E] [NormedStarGroup E] [inst_4 : NormedSpace 𝕜 E] [inst_5 : IsScalarTower 𝕜 E E]
  [inst_6 : SMulCommClass 𝕜 E E] [RegularNormedAlgebra 𝕜 E], Isometry ⇑(ContinuousLinearMap.mul 𝕜 E).flip
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} {x : α} {m : ℤ}
  {c : ↥g.cycleFactorsFinset}, (g ^ m) x ∈ (↑c).support ↔ x ∈ (↑c).support
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsShift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (a : A) [P.IsClosedUnderIsomorphisms],
  (P.shift a).IsClosedUnderIsomorphisms
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instIsScalarTowerQuotientIdealHSMulTopSubmodule : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsScalarTower R (R ⧸ I • ⊤) (M ⧸ I • ⊤)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.hasMeasurablePow : MeasurablePow ℝ ℝ
-- Init.Data.Array.Lemmas
Array.foldl_flatMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Array β} {g : γ → β → γ} {xs : Array α} {init : γ},
  Array.foldl g init (Array.flatMap f xs) = Array.foldl (fun acc x => Array.foldl g acc (f x)) init xs
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey?_eq_getLast?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.maxKey? = t.keys.getLast?
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
CategoryTheory.monoidalOfHasFiniteCoproducts.tensorHom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g = CategoryTheory.Limits.coprod.map f g
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_iInf : ∀ {ι : Sort u_1} {V : Type u} {G : SimpleGraph V} (f : ι → G.Subgraph),
  (⨅ i, f i).edgeSet = (⋂ i, (f i).edgeSet) ∩ G.edgeSet
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_base : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens), ⇑(f ∣_ U) = U.carrier.restrictPreimage ⇑f
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- An adjunction of braided functors lifts to an adjunction of their lifts to commutative monoid
objects.  -/
CategoryTheory.Adjunction.mapCommMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F : CategoryTheory.Functor C D} →
                  {G : CategoryTheory.Functor D C} →
                    (a : F ⊣ G) →
                      [inst_6 : F.Braided] → [inst_7 : G.LaxBraided] → [a.IsMonoidal] → F.mapCommMon ⊣ G.mapCommMon
-- Mathlib.Order.BoundedOrder.Lattice
min_bot_left : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] (a : α), min ⊥ a = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.degree_boxProd : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x : α × β)
  [inst : Fintype ↑(G.neighborSet x.1)] [inst_1 : Fintype ↑(H.neighborSet x.2)]
  [inst_2 : Fintype ↑((G □ H).neighborSet x)], (G □ H).degree x = G.degree x.1 + H.degree x.2
-- Lean.Meta.Tactic.Grind.ExtAttr
Lean.Meta.Grind.ExtTheorems.eraseDecl : Lean.Meta.Grind.ExtTheorems → Lean.Name → Lean.CoreM Lean.Meta.Grind.ExtTheorems
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_iInf : ∀ {R : Type u} [inst : NonAssocSemiring R] {ι : Sort u_1} {S : ι → Subsemiring R} {x : R},
  x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.instLinearOrderOfIsOrderedCancelMonoid : {α : Type u_1} →
  [inst : CommMonoid α] →
    [inst_1 : LinearOrder α] → [IsOrderedCancelMonoid α] → {s : Submonoid α} → LinearOrder (Localization s)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
instContinuousConstSMulTangentSpace : ∀ {𝕜 : 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] (_x : M), ContinuousConstSMul 𝕜 (TangentSpace I _x)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_disjoint : ∀ {V : Type u} (G : SimpleGraph V) (s : Set (Sym2 V)), Disjoint (SimpleGraph.fromEdgeSet s) G ↔ Disjoint s G.edgeSet
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instZero : {α : Type u_1} → [Zero α] → Zero (Colex α)
-- Mathlib.Algebra.Group.Action.Faithful
faithfulVAdd_iff_injective_vadd_zero : ∀ (R : Type u_4) (A : Type u_5) [inst : AddZeroClass A] [inst_1 : VAdd R A] [VAddAssocClass R A A],
  FaithfulVAdd R A ↔ Function.Injective fun r => r +ᵥ 0
-- Mathlib.Algebra.Homology.HomotopyCofiber
Homotopy.ofEq.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (h : f = g), Homotopy.ofEq h = Homotopy.ofEq h
-- Mathlib.Data.Multiset.Fintype
Multiset.map_toEnumFinset_fst : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), Multiset.map Prod.fst m.toEnumFinset.val = m
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.inter_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ m₄ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∩ m₂).Equiv (m₃ ∩ m₄)
-- Std.Internal.UV.Loop
Std.Internal.UV.Loop.Options.mk : Bool → Bool → Std.Internal.UV.Loop.Options
-- Mathlib.Order.Monotone.Basic
StrictMono.isMin_of_apply : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a : α},
  StrictMono f → IsMin (f a) → IsMin a
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.induce_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {s : Set V} (hw : ∀ x ∈ SimpleGraph.Walk.nil.support, x ∈ s),
  SimpleGraph.Walk.induce s SimpleGraph.Walk.nil hw = SimpleGraph.Walk.nil
-- Aesop.Rule.Name
Aesop.instBEqBuilderName.beq : Aesop.BuilderName → Aesop.BuilderName → Bool
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_ι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f ∣_ U) (CategoryTheory.CategoryStruct.comp U.ι h) =
    CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.mk_mem_target : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {x : B} {y : F}, (x, y) ∈ e'.target ↔ x ∈ e'.baseSet
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- Shrinking `F` to `Type w` followed by universe lifting is the same as shrinking to
`Type (max w w')`.  -/
CategoryTheory.FunctorToTypes.shrinkCompUliftFunctorIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w')) →
      [inst_1 : CategoryTheory.FunctorToTypes.Small.{w, w', v, u} F] →
        [inst_2 : CategoryTheory.FunctorToTypes.Small.{max w w'', w', v, u} F] →
          (CategoryTheory.FunctorToTypes.shrink.{w, w', v, u} F).comp CategoryTheory.uliftFunctor.{w'', w} ≅
            CategoryTheory.FunctorToTypes.shrink.{max w w'', w', v, u} F
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the norm of the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `‖f a‖ ≤ B a`;
* `f` has right derivative `f'` at every point of `[a, b)`;
* `B` has derivative `B'` everywhere on `ℝ`;
* we have `‖f' x‖ ≤ B x` everywhere on `[a, b)`.

Then `‖f x‖ ≤ B x` everywhere on `[a, b]`. We use one-sided derivatives in the assumptions
to make this theorem work for piecewise differentiable functions.
 -/
image_norm_le_of_norm_deriv_right_le_deriv_boundary : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' : ℝ → E},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      ∀ {B B' : ℝ → ℝ},
        ‖f a‖ ≤ B a →
          (∀ (x : ℝ), HasDerivAt B (B' x) x) →
            (∀ x ∈ Set.Ico a b, ‖f' x‖ ≤ B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
-- Lean.Util.LeanOptions
/-- The option's name.  -/
Lean.LeanOption.name : Lean.LeanOption → Lean.Name
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.length_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Init.Data.UInt.Bitwise
USize.shiftRight_zero : ∀ {a : USize}, a >>> 0 = a
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} (η : F ⟶ G) {a b c : B} {a' : C} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a')
  {Z : F.obj a ⟶ a'}
  (h_1 :
    CategoryTheory.CategoryStruct.comp (η.app a)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (η.app a) (G.map (CategoryTheory.CategoryStruct.comp f g)) h).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a)
            (CategoryTheory.Bicategory.whiskerRight (G.mapComp f g).hom h))
          h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (η.app c)) h)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (η.app c)).hom
          h)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (F.map g) (η.app c))
              h).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (F.map f)
              (CategoryTheory.Bicategory.whiskerRight (η.naturality g).hom h))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (CategoryTheory.CategoryStruct.comp (η.app b) (G.map g))
                  h).inv
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerRight
                  (CategoryTheory.Bicategory.associator (F.map f) (η.app b) (G.map g)).inv h)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Bicategory.whiskerRight
                    (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom (G.map g)) h)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.whiskerRight
                      (CategoryTheory.Bicategory.associator (η.app a) (G.map f) (G.map g)).hom h)
                    (CategoryTheory.CategoryStruct.comp
                      (CategoryTheory.Bicategory.associator (η.app a)
                          (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) h).hom
                      h_1))))))))
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counit_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {X Y : D} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) (e.counit.app Y) =
    CategoryTheory.CategoryStruct.comp (e.counit.app X) f
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.discreteTopology_iff : ∀ {α : Type u} [inst : TopologicalSpace α],
  DiscreteTopology (ConnectedComponents α) ↔ ∀ (x : α), IsOpen (connectedComponent x)
-- Std.Time.DateTime.WallTime
Std.Time.instDecidableLeWallTime : {x y : Std.Time.WallTime} → Decidable (x ≤ y)
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.category_id_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] (F : C → D)
  (P : CategoryTheory.MorphismProperty D) [inst_1 : P.IsMultiplicative] (X : CategoryTheory.InducedWideCategory D F P),
  (CategoryTheory.CategoryStruct.id X).hom = CategoryTheory.CategoryStruct.id (F X)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_takeEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String},
  (s.takeEndWhile pat).isEmpty = !s.endsWith pat
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.intCast_def : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroupWithOne k] [inst_1 : One G] (z : ℤ), ↑z = SkewMonoidAlgebra.single 1 ↑z
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.PullbackCone.fst_eq_snd_of_mono_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} [CategoryTheory.Mono f]
  (t : CategoryTheory.Limits.PullbackCone f f), t.fst = t.snd
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.IsCardinalLocallyPresentable.of_le : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalLocallyPresentable C κ] {κ' : Cardinal.{w}} [inst_3 : Fact κ'.IsRegular],
  κ ≤ κ' → CategoryTheory.IsCardinalLocallyPresentable C κ'
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instNonAssocRing : {R : Type u_1} → [NonAssocRing R] → NonAssocRing Rᵒᵈ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_none : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  a ∉ t → t.getKey? a = none
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise multiplication of `f` and `g` is minimized when `f` and
`g` antivary together. Stated by permuting the entries of `g`.  -/
Antivary.sum_mul_le_sum_mul_comp_perm : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι], Antivary f g → ∑ i, f i * g i ≤ ∑ i, f i * g (σ i)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).hom (E.p₁ k) =
    CategoryTheory.CategoryStruct.comp (E.p₁ ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k))
      (CategoryTheory.eqToHom ⋯)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.of_map_injective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] {f : M →ₗ[R] N},
  Function.Injective ⇑f → (PointedCone.map f F).IsFaceOf (PointedCone.map f C) → F.IsFaceOf C
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The conversion from a Weierstrass curve in projective coordinates to affine coordinates.  -/
WeierstrassCurve.Projective.toAffine : {R : Type r} → WeierstrassCurve.Projective R → WeierstrassCurve.Affine R
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)} (φ : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.map₂ α β).map φ).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.iSup_def : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_2} {f : ι → SaturatedAddSubmonoid M},
  iSup f = (⨆ i, (f i).toAddSubmonoid).saturation
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
ContinuousOn.integrableOn_Icc : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_5 : Preorder X] [CompactIccSpace X] [T2Space X],
  ContinuousOn f (Set.Icc a b) → MeasureTheory.IntegrableOn f (Set.Icc a b) μ
-- Mathlib.Algebra.Group.Indicator
Set.indicator_compl_add_self_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : AddZeroClass M] (s : Set α) (f : α → M) (a : α),
  sᶜ.indicator f a + s.indicator f a = f a
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
tsum_op : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {f : β → α} [T2Space α], ∑'[L] (x : β), MulOpposite.op (f x) = MulOpposite.op (∑'[L] (x : β), f x)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opEquiv_unitIso : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T),
  (CategoryTheory.Comma.opEquiv L R).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Comma L R)).obj X)) ⋯
-- ProofWidgets.Component.MakeEditLink
ProofWidgets.MakeEditLinkProps.mk : Lean.Lsp.TextDocumentEdit → Option Lean.Lsp.Range → Option String → ProofWidgets.MakeEditLinkProps
-- Mathlib.RingTheory.RingHomProperties
/-- A property of ring homomorphisms `P` is said to have equalizers, if the equalizer of algebra
maps between algebras satisfying `P` also satisfies `P`.  -/
RingHom.HasEqualizers : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.RingTheory.Ideal.Operations
Submodule.smul_top_le_comap_smul_top : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] (I : Ideal R) (f : M →ₗ[R] N), I • ⊤ ≤ Submodule.comap f (I • ⊤)
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edgeSet_edge_of_ne : ∀ {V : Type u_1} {s t : V}, s ≠ t → (SimpleGraph.edge s t).edgeSet = {s(s, t)}