mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `v ∈ s`, then the neighbor set of `v` is a subset of `t`.  -/
SimpleGraph.isBipartiteWith_neighborSet_subset : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → v ∈ s → G.neighborSet v ⊆ t
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.submonoidMap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (M' : Submonoid M)
  (x : ↥M'), ↑((f.submonoidMap M') x) = f ↑x
-- Mathlib.Topology.Instances.Real.Lemmas
Real.continuous_inv : Continuous fun a => (↑a)⁻¹
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a top order
with possibly different definitional equalities.  -/
OrderTop.copy : {α : Type u} → {h h' : LE α} → (c : OrderTop α) → (top : α) → top = ⊤ → (∀ (x y : α), x ≤ y ↔ x ≤ y) → OrderTop α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_get?_iff_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α}, (t.get? a).isSome = true ↔ a ∈ t
-- Mathlib.Algebra.Order.Hom.Basic
map_ne_zero_iff_ne_zero : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [AddGroupNormClass F α β] (f : F) {x : α}, f x ≠ 0 ↔ x ≠ 0
-- Init.Data.BitVec.Lemmas
BitVec.instLawfulCommIdentityHOrOfNatOfNatNat : ∀ {n : ℕ}, Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0#n
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- Sending `X : C` to `Subobject X` is a contravariant functor `Cᵒᵖ ⥤ Type`.  -/
CategoryTheory.Subobject.functor : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasPullbacks C] → CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₁))
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instToSnapshotTreeTacticParsedSnapshot.go : Lean.Elab.Tactic.TacticParsedSnapshot → Lean.Language.ToSnapshotTreeM Lean.Language.SnapshotTree
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.fst_opProdIsoCoprod_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B] {Z : Cᵒᵖ} (h : Opposite.op A ⨿ Opposite.op B ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst.op
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
-- Lean.Declaration
Lean.instInhabitedRecursorVal : Inhabited Lean.RecursorVal
-- Batteries.Data.Fin.Lemmas
Fin.bind_findSomeRev?_guard_isSome : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α},
  (Fin.findSomeRev? (Option.guard fun i => (f i).isSome)).bind f = Fin.findSomeRev? f
-- Mathlib.Algebra.Field.IsField
/-- Transferring from `IsField` to `Field`.  -/
IsField.toField : {R : Type u} → [inst : Ring R] → IsField R → Field R
-- Mathlib.Analysis.Convex.Between
Wbtw.right_mem_image_Ici_of_left_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z → x ≠ y → z ∈ ⇑(AffineMap.lineMap x y) '' Set.Ici 1
-- Mathlib.Order.Hom.Basic
/-- Turn an element of a type `F` satisfying `OrderIsoClass F α β` into an actual
`OrderIso`. This is declared as the default coercion from `F` to `α ≃o β`.  -/
OrderIsoClass.toOrderIso : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} → [inst : LE α] → [inst_1 : LE β] → [inst_2 : EquivLike F α β] → [OrderIsoClass F α β] → F → α ≃o β
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- The naturality condition.  -/
CategoryTheory.Lax.LaxTrans.Modification.naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (self : CategoryTheory.Lax.LaxTrans.Modification η θ) {a b : B}
  (f : a ⟶ b),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.app a) (G.map f)) (θ.naturality f) =
    CategoryTheory.CategoryStruct.comp (η.naturality f) (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.app b))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.toPresheaf_preservesColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))]
  [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))]
  [∀ (X : Cᵒᵖ),
      CategoryTheory.Limits.PreservesColimit F
        ((PresheafOfModules.evaluation R X).comp (CategoryTheory.forget₂ (ModuleCat ↑(R.obj X)) AddCommGrpCat))],
  CategoryTheory.Limits.PreservesColimit F (PresheafOfModules.toPresheaf R)
-- Mathlib.Order.Disjointed
Monotone.disjointed_succ : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : SuccOrder ι] {f : ι → α},
  Monotone f → ∀ {i : ι}, ¬IsMax i → disjointed f (Order.succ i) = f (Order.succ i) \ f i
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.span_singleton_inf_orthogonal_eq_bot : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {B : LinearMap.BilinForm K V} {x : V}, (B x) x ≠ 0 → K ∙ x ⊓ B.orthogonal (K ∙ x) = ⊥
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.hComp_iso_inv_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₅] [inst_5 : CategoryTheory.Category.{v_6, u_6} C₆]
  (T₁ : CategoryTheory.Functor C₁ C₂) (T₂ : CategoryTheory.Functor C₂ C₃) (V₁ : CategoryTheory.Functor C₁ C₄)
  (V₂ : CategoryTheory.Functor C₂ C₅) (V₃ : CategoryTheory.Functor C₃ C₆) (B₁ : CategoryTheory.Functor C₄ C₅)
  (B₂ : CategoryTheory.Functor C₅ C₆) [inst_6 : CategoryTheory.CatCommSq T₁ V₁ V₂ B₁]
  [inst_7 : CategoryTheory.CatCommSq T₂ V₂ V₃ B₂] (X : C₁),
  (CategoryTheory.CatCommSq.iso (T₁.comp T₂) V₁ V₃ (B₁.comp B₂)).inv.app X =
    CategoryTheory.CategoryStruct.comp (B₂.map ((CategoryTheory.CatCommSq.iso T₁ V₁ V₂ B₁).inv.app X))
      ((CategoryTheory.CatCommSq.iso T₂ V₂ V₃ B₂).inv.app (T₁.obj X))
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.pushforwardCongr_inv_app_app : ∀ {X Y : AlgebraicGeometry.Scheme} {M : X.Modules} {f g : X ⟶ Y} (hf : f = g) (U : Y.Opens),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.pushforwardCongr hf).inv.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.Algebra.Algebra.StrictPositivity
isStrictlyPositive_one : ∀ {A : Type u_1} [inst : LE A] [inst_1 : Monoid A] [inst_2 : Zero A] [ZeroLEOneClass A], IsStrictlyPositive 1
-- Mathlib.Data.Finset.Image
Finset.filterMap_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) {f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'},
  Finset.filterMap f ∅ f_inj = ∅
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.localized'_top : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f], Submodule.localized' S p f ⊤ = ⊤
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.TerminationMeasure.mk.sizeOf_spec : ∀ (ref : Lean.Syntax) (structural : Bool) (fn : Lean.Expr),
  sizeOf { ref := ref, structural := structural, fn := fn } = 1 + sizeOf ref + sizeOf structural + sizeOf fn
-- Mathlib.Analysis.Calculus.TangentCone.Basic
UniqueDiffWithinAt.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {s t : Set E} {x : E}, UniqueDiffWithinAt 𝕜 s x → s ⊆ t → UniqueDiffWithinAt 𝕜 t x
-- Init.Prelude
/-- `a ^ b` computes `a` to the power of `b`. See `HPow`.  -/
Pow.pow : {α : Type u} → {β : Type v} → [self : Pow α β] → α → β → α
-- LeanSearchClient.Syntax
/-- Search from within Lean, depending on the option `leansearchclient.backend` (currently only leansearch).
Queries should be a string that ends with a `.` or `?`. This works as a command, as a term
and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

```lean
#search "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #search "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #search "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry

In tactic mode, if the query string is not supplied, then [LeanStateSearch](https://premise-search.com) is queried based on the goal state.
```
  -/
LeanSearchClient.search_term : Lean.ParserDescr
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.congr_left : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {g : α → F} {l : Filter α}
  {f₁ f₂ : α → E}, f₁ =O[l] g → (∀ (x : α), f₁ x = f₂ x) → f₂ =O[l] g
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrange_id : ∀ {M : Type u_1} [inst : MulOneClass M], MonoidHom.mrange (MonoidHom.id M) = ⊤
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.EStateM.run_bind.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((x : α) → (s : σ) → motive (EStateM.Result.ok x s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x
-- Mathlib.AlgebraicTopology.DoldKan.Faces
AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Y : C} {n a q : ℕ} {φ : Y ⟶ X.obj (Opposite.op { len := n + 1 })},
  AlgebraicTopology.DoldKan.HigherFacesVanish q φ →
    ∀ (hnaq : n = a + q),
      CategoryTheory.CategoryStruct.comp φ ((AlgebraicTopology.DoldKan.Hσ q).f (n + 1)) =
        -CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (X.δ ⟨a + 1, ⋯⟩) (X.σ ⟨a, ⋯⟩))
-- Mathlib.Data.Multiset.Replicate
Multiset.coe_replicate : ∀ {α : Type u_1} (n : ℕ) (a : α), ↑(List.replicate n a) = Multiset.replicate n a
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.not_ofNat_le_one : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {n : ℕ} [inst_5 : n.AtLeastTwo], ¬OfNat.ofNat n ≤ 1
-- Mathlib.Analysis.Normed.Group.Subgroup
/-- If `x` is an element of a subgroup `s` of a seminormed group `E`, its norm in `s` is equal to
its norm in `E`.  -/
Subgroup.coe_norm : ∀ {E : Type u_1} [inst : SeminormedGroup E] {s : Subgroup E} (x : ↥s), ‖x‖ = ‖↑x‖
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.algebraMap_injective : ∀ {R : Type u_1} (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A],
  Function.Injective ⇑(algebraMap R A)
-- Mathlib.Data.List.Rotate
List.rotate'_zero : ∀ {α : Type u} (l : List α), l.rotate' 0 = l
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `fallback` if no such key exists.
 -/
Std.ExtDTreeMap.getKeyLTD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → α → α
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.equiv_def : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {x y : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)},
  x ≈ y ↔ x.seq = y.seq ∧ x.toFun =ᶠ[Filter.atTop] y.toFun
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- the underlying object of a (pre)path object  -/
HomotopicalAlgebra.PrepathObject.P : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {A : C} → HomotopicalAlgebra.PrepathObject A → C
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Under.pushout_map_right : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : P.HasPushoutsAlong f]
  [inst_3 : P.IsStableUnderCobaseChangeAlong f] [inst_4 : Q.IsStableUnderCobaseChange] {A B : P.Under Q X} (g : A ⟶ B),
  ((CategoryTheory.MorphismProperty.Under.pushout P Q f).map g).right =
    CategoryTheory.Limits.pushout.desc
      (CategoryTheory.CategoryStruct.comp g.right (CategoryTheory.Limits.pushout.inl B.hom f))
      (CategoryTheory.Limits.pushout.inr B.hom f) ⋯
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      Std.Internal.List.containsKey k l = false →
        Std.Internal.List.getValueCastD k (Std.Internal.List.insertList l toInsert) fallback =
          Std.Internal.List.getValueCastD k toInsert fallback
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.comp_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v w : CategoryTheory.Arrow V} {f₁ g₁ : u ⟶ v} {f₂ g₂ : v ⟶ w} (h₁ : CategoryTheory.Arrow.RightHomotopy f₁ g₁)
  (h₂ : CategoryTheory.Arrow.RightHomotopy f₂ g₂),
  (h₁.comp h₂).hom =
    CategoryTheory.CategoryStruct.comp h₁.hom (CategoryTheory.Arrow.Hom.left f₂) +
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right g₁) h₂.hom
-- Mathlib.Order.RelSeries
RelSeries.membership : {α : Type u_1} → {r : SetRel α α} → Membership α (RelSeries r)
-- Init.Data.List.Monadic
List.forIn_pure_yield_eq_foldl : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α} (f : α → β → β)
  (init : β), (forIn l init fun a b => pure (ForInStep.yield (f a b))) = pure (List.foldl (fun b a => f a b) init l)
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.orthogonal_mk : ∀ {F : Type u_1} [inst : Field F] {m : Type u_2} [inst_1 : Fintype m] {v w : m → F} (hv : v ≠ 0) (hw : w ≠ 0),
  (Projectivization.mk F v hv).orthogonal (Projectivization.mk F w hw) ↔ v ⬝ᵥ w = 0
-- Init.Data.Nat.Basic
Nat.sub_pos_of_lt : ∀ {m n : ℕ}, m < n → 0 < n - m
-- Init.Data.Array.Extract
Array.size_extract_of_le : ∀ {α : Type u_1} {as : Array α} {i j : ℕ}, j ≤ as.size → (as.extract i j).size = j - i
-- Mathlib.GroupTheory.Congruence.Basic
/-- A multiplicative equivalence `e : α ≃* β` generates an equivalence between quotient spaces,
if it is compatible with the relations.  -/
Con.congr : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] →
      [inst_1 : Mul N] → {c : Con M} → {d : Con N} → (e : M ≃* N) → c = Con.comap ⇑e ⋯ d → c.Quotient ≃* d.Quotient
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.support_homogeneousComponent : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (n : ℕ) (p : MvPolynomial σ R),
  ((MvPolynomial.homogeneousComponent n) p).support = {c ∈ p.support | Finsupp.degree c = n}
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.instSetLike : {α : Type u_1} → [inst : CompleteLattice α] → SetLike (CompleteSublattice α) α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.simp_cert : ℤ → Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.Logic.Function.Coequalizer
Function.Coequalizer.condition : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) (x : α),
  Function.Coequalizer.mk f g (f x) = Function.Coequalizer.mk f g (g x)
-- Std.Http.Internal.ChunkedBuffer
/-- Build from a ByteArray directly.
 -/
Std.Http.Internal.ChunkedBuffer.ofByteArray : ByteArray → Std.Http.Internal.ChunkedBuffer
-- Std.Time.Format
/-- Formats a `PlainDateTime` using a specific format and locale.
 -/
Std.Time.PlainDateTime.format : Std.Time.PlainDateTime → String → optParam Std.Time.DateFormat Std.Time.DateFormat.enUS → String
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightExtension.instInhabitedId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a c : B} →
      {g : a ⟶ c} → Inhabited (CategoryTheory.Bicategory.RightExtension (CategoryTheory.CategoryStruct.id a) g)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Top.adjDecidable : (V : Type u) → [DecidableEq V] → DecidableRel ⊤.Adj
-- Mathlib.GroupTheory.Transfer
Subgroup.transferTransversal_apply : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (g : G) (q : G ⧸ H),
  ↑(⋯.leftQuotientEquiv q) = H.transferFunction g q
-- Mathlib.Order.Fin.Tuple
finSuccAboveOrderIso.eq_1 : ∀ {n : ℕ} (p : Fin (n + 1)), finSuccAboveOrderIso p = { toEquiv := finSuccAboveEquiv p, map_rel_iff' := ⋯ }
-- Mathlib.Dynamics.FixedPoints.Basic
/-- If self-maps `f` and `g` commute, then they are inverse of each other on the set of fixed points
of `f ∘ g`. This is a particular case of `Function.invOn_fixedPoints_comp`.  -/
Function.Commute.invOn_fixedPoints_comp : ∀ {α : Type u_1} {f g : α → α},
  Function.Commute f g → Set.InvOn f g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (f ∘ g))
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X : C),
  F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.η F))
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.forIn_eq_forIn_keys : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  Std.DTreeMap.Internal.Impl.forIn (fun a x d => f a d) init t = forIn t.keys init f
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.forall : ∀ {V : Type u} {G : SimpleGraph V} {p : G.ConnectedComponent → Prop},
  (∀ (c : G.ConnectedComponent), p c) ↔ ∀ (v : V), p (G.connectedComponentMk v)
-- Std.Data.Iterators.Lemmas.Combinators.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.DropWhile.0.Std.Iter.val_step_intermediateDropWhile.match_3.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Std.Time.Time.Unit.Second
Std.Time.Second.instLEOrdinal : {leap : Bool} → LE (Std.Time.Second.Ordinal leap)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.not_isLoop : ∀ {α : Type u_1} (M : Matroid α) [M.Loopless] (e : α), ¬M.IsLoop e
-- Mathlib.Data.Finsupp.Option
/-- Restrict a finitely supported function on `Option α` to a finitely supported function on `α`.  -/
Finsupp.some : {α : Type u_1} → {M : Type u_2} → [inst : Zero M] → (Option α →₀ M) → α →₀ M
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
one_mem_posTangentConeAt_iff_mem_closure : ∀ {s : Set ℝ} {a : ℝ}, 1 ∈ posTangentConeAt s a ↔ a ∈ closure (Set.Ioi a ∩ s)
-- Init.Data.List.Sublist
List.infix_iff_suffix_prefix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ ↔ ∃ t, l₁ <:+ t ∧ t <+: l₂
-- Init.Data.Nat.Simproc
Nat.Simproc.eq_add_gt : ∀ (a : ℕ) {b c : ℕ}, c > a → (a = b + c) = False
-- Mathlib.Data.TypeVec
/-- vector of equality on a product of vectors  -/
TypeVec.repeatEq : {n : ℕ} → (α : TypeVec.{u_1} n) → (α.prod α).Arrow (TypeVec.repeat n Prop)
-- Mathlib.LinearAlgebra.Quotient.Pi
Submodule.piQuotientLift_mk : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] {N : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : Module R N]
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) (q : Submodule R N)
  (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i ≤ Submodule.comap (f i) q) (x : (i : ι) → Ms i),
  ((Submodule.piQuotientLift p q f hf) fun i => Submodule.Quotient.mk (x i)) =
    Submodule.Quotient.mk (((LinearMap.lsum R Ms R) f) x)
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
/-- An injection into the metric space provides a unit-distance embedding of the empty graph.  -/
SimpleGraph.UnitDistEmbedding.bot : {V : Type u_1} → {E : Type u_3} → [inst : MetricSpace E] → (V ↪ E) → ⊥.UnitDistEmbedding E
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.coherentExtensiveEquivalence_inverse_obj_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.Preregular C]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : ∀ (X : C), CategoryTheory.Projective X]
  (X : CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A),
  (CategoryTheory.Presheaf.coherentExtensiveEquivalence.inverse.obj X).obj = X.obj
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.exists_seq_mono_tendsto : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι),
  ∃ J,
    (∀ (n : ℕ), BoxIntegral.Box.Icc (J n) ⊆ BoxIntegral.Box.Ioo I) ∧
      Filter.Tendsto (BoxIntegral.Box.lower ∘ ⇑J) Filter.atTop (nhds I.lower) ∧
        Filter.Tendsto (BoxIntegral.Box.upper ∘ ⇑J) Filter.atTop (nhds I.upper)
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.revAt_zero : ∀ (N : ℕ), (Polynomial.revAt N) 0 = N
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_insertIfNew : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insertIfNew k v).size = if k ∈ m then m.size else m.size + 1
-- Init.GrindInstances.ToInt
Lean.Grind.instLEUInt32UintOfNatNat : Lean.Grind.ToInt.LE UInt32 (Lean.Grind.IntInterval.uint 32)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- If `f : X ⤏ Y` is a rational map from a reduced scheme to a separated scheme,
then `f` can be represented as a partial map on its domain of definition.  -/
AlgebraicGeometry.Scheme.RationalMap.toPartialMap : {X Y : AlgebraicGeometry.Scheme} → [AlgebraicGeometry.IsReduced X] → [Y.IsSeparated] → X.RationalMap Y → X.PartialMap Y
-- Std.Sat.CNF.Basic
Std.Sat.CNF.unsat_add_nil : ∀ {α : Type u_1} {g : Std.Sat.CNF α}, (Std.Sat.CNF.add [] g).Unsat
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.elabHeadersAux.match_1.eq_1 : ∀ (motive : Lean.Expr × ℕ → Sort u_1) (type : Lean.Expr) (snd : ℕ)
  (h_1 : (type : Lean.Expr) → (snd : ℕ) → motive (type, snd)),
  (match (type, snd) with
    | (type, snd) => h_1 type snd) =
    h_1 type snd