mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
extChartAt_target_mem_nhdsWithin_of_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M} {y : E},
  y ∈ (extChartAt I x).target → (extChartAt I x).target ∈ nhdsWithin y (Set.range ↑I)
-- Init.Data.UInt.Bitwise
UInt16.toFin_shiftLeft : ∀ (a b : UInt16), b < 16 → (a <<< b).toFin = a.toFin <<< b.toFin
-- Lean.Meta.Diagnostics
Lean.Meta.DiagSummary.mk : Array Lean.MessageData → ℕ → Lean.Meta.DiagSummary
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- An object is indecomposable if it cannot be written as the biproduct of two nonzero objects.  -/
CategoryTheory.Indecomposable : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → [CategoryTheory.Limits.HasBinaryBiproducts C] → C → Prop
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.BodyInfo.mk.inj : ∀ {value? value?_1 : Option Lean.Expr}, { value? := value? } = { value? := value?_1 } → value? = value?_1
-- Mathlib.Order.ULift
ULift.instLawfulLEOrd_mathlib : ∀ {α : Type u} [inst : LE α] [inst_1 : Ord α] [inst_2 : Std.LawfulLEOrd α], Std.LawfulLEOrd (ULift.{v, u} α)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.structuredArrowObj_iff : ∀ {B : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} T] (R : CategoryTheory.Functor B T)
  {W : CategoryTheory.MorphismProperty T} {X : T} (Y : CategoryTheory.StructuredArrow X R),
  CategoryTheory.MorphismProperty.structuredArrowObj R W Y ↔ W Y.hom
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The star operation on `NonUnitalSubalgebra` commutes with `NonUnitalAlgebra.adjoin`.  -/
NonUnitalSubalgebra.star_adjoin_comm : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : IsScalarTower R A A]
  [inst_7 : SMulCommClass R A A] (s : Set A), star (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (star s)
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_add_smoothingFn : ∀ (p : ℝ),
  (deriv fun z => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) =ᶠ[Filter.atTop] fun z =>
    p * z ^ (p - 1) * (1 + AkraBazziRecurrence.smoothingFn z) - z ^ (p - 1) / Real.log z ^ 2
-- Lean.Elab.MutualInductive
/-- Fully qualified name of the constructor.  -/
Lean.Elab.Command.CtorView.declName : Lean.Elab.Command.CtorView → Lean.Name
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.mem_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] (g : G), g ∈ AddSubgroup.zmultiples g
-- Mathlib.Data.List.Destutter
List.destutter'_singleton : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
  List.destutter' R a [b] = if R a b then [a, b] else [a]
-- Init.Data.Rat.Lemmas
Rat.normalize_num_den' : ∀ (num : ℤ) (den : ℕ) (nz : den ≠ 0),
  ∃ d, d ≠ 0 ∧ num = (Rat.normalize num den nz).num * ↑d ∧ den = (Rat.normalize num den nz).den * d
-- Mathlib.Algebra.Group.Defs
RightCancelMonoid.mk : {M : Type u} → [toMonoid : Monoid M] → [toIsRightCancelMul : IsRightCancelMul M] → RightCancelMonoid M
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.isOpenEmbedding_restrict : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), Topology.IsOpenEmbedding (e.source.domRestrict ↑e)
-- Mathlib.Algebra.Order.Archimedean.Class
/-- The upper set in `MulArchimedeanClass M` consisting of an upper set in
`FiniteMulArchimedeanClass M` plus `⊤`.  -/
FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClass : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] → UpperSet (FiniteMulArchimedeanClass M) ↪o UpperSet (MulArchimedeanClass M)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.instMonad : Monad FreeAbelianGroup
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.BuiltinSimprocs.mk.injEq : ∀ (keys : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey))
  (procs : Std.HashMap Lean.Name (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc))
  (keys_1 : Std.HashMap Lean.Name (Array Lean.Meta.SimpTheoremKey))
  (procs_1 : Std.HashMap Lean.Name (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)),
  ({ keys := keys, procs := procs } = { keys := keys_1, procs := procs_1 }) = (keys = keys_1 ∧ procs = procs_1)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.comm : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J} (self : D.IsTerminal e) {i j : J}
  (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (self.lift ⋯) = self.lift ⋯
-- Mathlib.Data.Fintype.Vector
Sym.Sym'.instFintype : {α : Type u_1} → [DecidableEq α] → [Fintype α] → {n : ℕ} → Fintype (Sym.Sym' α n)
-- Mathlib.Util.MemoFix
/-- Takes the fixpoint of `f` with caching of values that have been seen before.
Hashing makes use of a pointer hash.

This is useful for implementing tree traversal functions where
subtrees may be referenced in multiple places.
 -/
memoFix : {α β : Type} → [Nonempty β] → ((α → β) → α → β) → α → β
-- Mathlib.Analysis.Convex.Intrinsic
AffineEquiv.intrinsicFrontier_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} {Q : Type u_4} {P : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [CompleteSpace 𝕜] [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V]
  [inst_5 : NormedAddCommGroup W] [inst_6 : NormedSpace 𝕜 W] [inst_7 : MetricSpace P] [inst_8 : NormedAddTorsor V P]
  [inst_9 : MetricSpace Q] [inst_10 : NormedAddTorsor W Q] (φ : P ≃ᵃ[𝕜] Q) (s : Set P),
  intrinsicFrontier 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicFrontier 𝕜 s
-- Init.Data.SInt.Lemmas
Int64.toInt_neg_ofNat_of_le : ∀ {n : ℕ}, n ≤ 2 ^ 63 → (-Int64.ofNat n).toInt = -↑n
-- Mathlib.Topology.Connected.Basic
IsPreconnected.subset_right_of_subset_union : ∀ {α : Type u} [inst : TopologicalSpace α] {s u v : Set α},
  IsOpen u → IsOpen v → Disjoint u v → s ⊆ u ∪ v → (s ∩ v).Nonempty → IsPreconnected s → s ⊆ v
-- Mathlib.Order.Comparable
/-- **Alias** of `CompRel.of_gt`. -/
LT.lt.compRel_symm : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], b < a → CompRel (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.structuredArrowMapCone_pt : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : L.comp G ⟶ F)
  (Y : D), (L.structuredArrowMapCone F G α Y).pt = G.obj Y
-- Mathlib.Data.Set.Function
Set.EqOn.cancel_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {f : α → β} {g₁ g₂ : β → γ},
  Set.EqOn (g₁ ∘ f) (g₂ ∘ f) s → Set.SurjOn f s t → Set.EqOn g₁ g₂ t
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?.go.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a)),
  Std.DTreeMap.Internal.Impl.getEntryGT?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.GroupTheory.Perm.ClosureSwap
/-- A transitive permutation group generated by transpositions must be the whole symmetric group  -/
surjective_of_isSwap_of_isPretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : DecidableEq α] [Finite α]
  (S : Set G),
  (∀ σ ∈ S, ((MulAction.toPermHom G α) σ).IsSwap) →
    Subgroup.closure S = ⊤ → ∀ [h : MulAction.IsPretransitive G α], Function.Surjective ⇑(MulAction.toPermHom G α)
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The isomorphism `spanFunctor hC ≅ indexFunctor hC` when `hC : IsCompact C`.  -/
Profinite.NobelingProof.spanFunctorIsoIndexFunctor : {I : Type u} →
  {C : Set (I → Bool)} →
    [inst : (s : Finset I) → (i : I) → Decidable (i ∈ s)] →
      (hC : IsCompact C) → Profinite.NobelingProof.spanFunctor hC ≅ Profinite.indexFunctor hC
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.parenthesizeTactic : Lean.Syntax → Lean.CoreM Lean.Syntax
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.mul_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x x' y : CommRingCat.Colimits.Prequotient F) (x_1 : CommRingCat.Colimits.Relation F x x'),
  CommRingCat.Colimits.Relation.below x_1 → motive x x' x_1 → CommRingCat.Colimits.Relation.below ⋯
-- Lean.Data.Lsp.Client
Lean.Lsp.instFromJsonRegistration : Lean.FromJson Lean.Lsp.Registration
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_append_of_lt : ∀ {k w i : ℕ} {x : BitVec (k * w)} {y : BitVec w},
  i < k → BitVec.extractLsb' (i * w) w (y ++ x) = BitVec.extractLsb' (i * w) w x
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageParams.mk.inj : ∀ {type : Lean.Lsp.MessageType} {message : String} {type_1 : Lean.Lsp.MessageType} {message_1 : String},
  { type := type, message := message } = { type := type_1, message := message_1 } → type = type_1 ∧ message = message_1
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_diff_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₂ → (m₁ \ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.map_add : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B) (x y : A), f (x + y) = f x + f y
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.inc : Nat.Internal.Linear.Expr → Nat.Internal.Linear.Expr
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.closure_le : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {I : SemigroupIdeal M}, SemigroupIdeal.closure s ≤ I ↔ s ⊆ ↑I
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.X_negSucc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (n : ℕ), CochainComplex.ConnectData.X K L (Int.negSucc n) = K.X n
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.IsContained.mono_right : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B B' : SimpleGraph β}, A.IsContained B → B ≤ B' → A.IsContained B'
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_neg : ∀ {R : Type u_1} [inst : Ring R] {a : R} [MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.C (-a) = -SkewPolynomial.C a
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- **Alias** of `MeasurableEquiv.coe_setOfPred`. -/
MeasurableEquiv.coe_setOf : ∀ {α : Type u_8}, ⇑MeasurableEquiv.setOfPred = Set.ofPred
-- Mathlib.Analysis.Normed.Ring.Basic
SubringClass.toNormedRing : {S : Type u_5} →
  {R : Type u_6} → [inst : SetLike S R] → [inst_1 : NormedRing R] → [SubringClass S R] → (s : S) → NormedRing ↥s
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt_go : ∀ {α : Type u_1} (xs : List α) (i : ℕ) (acc : List α),
  List.MergeSort.Internal.splitRevAt.go✝ xs i acc = ((List.take i xs).reverse ++ acc, List.drop i xs)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.JPDecl.mk.sizeOf_spec : ∀ (name : Lean.Name) (params : Array (Lean.Elab.Term.Do.Var × Bool)) (body : Lean.Elab.Term.Do.Code),
  sizeOf { name := name, params := params, body := body } = 1 + sizeOf name + sizeOf params + sizeOf body
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderivWithin_natCast : ∀ {𝕜 : 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 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} [inst_7 : NatCast F] (n : ℕ), fderivWithin 𝕜 (↑n) s = 0
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wf_eraseMany₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}
  [inst_4 : ForIn Id ρ ((a : α) × β a)] {m : Std.DHashMap.Raw α β} {h : 0 < m.buckets.size} {l : ρ},
  m.WF → (↑↑(Std.DHashMap.Internal.Raw₀.eraseManyEntries ⟨m, h⟩ l)).WF
-- Mathlib.Data.List.Basic
List.get_tail : ∀ {α : Type u} (l : List α) (i : ℕ) (h : i < l.tail.length) (h' : optParam (i + 1 < l.length) ⋯),
  l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_natCast : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Algebra ℝ A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A] (n : ℕ), CFC.abs ↑n = ↑n
-- Lean.Elab.Deriving.Basic
_private.Lean.Elab.Deriving.Basic.0.Lean.Elab.Term.MkInstResult.instType : Lean.Elab.Term.MkInstResult✝ → Lean.Expr
-- Mathlib.Topology.Irreducible
mem_of_subset_sUnion_irreducibleComponents : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  ∀ Z ∈ irreducibleComponents X, ∀ (S : Set (Set X)), S.Finite → S ⊆ irreducibleComponents X → Z ⊆ ⋃₀ S → Z ∈ S
-- Init.Data.List.Lemmas
List.prod_singleton : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.LawfulRightIdentity (fun x1 x2 => x1 * x2) 1] {x : α},
  [x].prod = x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse_obj_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Over.forget X.1) X.2),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.inverse X).obj Y).hom = (Y.left.hom, Y.hom)
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsMaxOn.hasLineDerivWithinAt_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {s : Set E} {a b : E} {f' : ℝ},
  IsMaxOn f s a → HasLineDerivWithinAt ℝ f f' s a b → (∀ᶠ (t : ℝ) in nhds 0, a + t • b ∈ s) → f' = 0
-- Init.Data.List.MinMaxOn
List.min_eq_max : ∀ {α : Type u_1} {min : Min α} {xs : List α} {h : xs ≠ []}, xs.min h = xs.max h
-- Mathlib.Analysis.Normed.Ring.Basic
norm_mul_le_of_le : ∀ {α : Type u_2} [inst : NonUnitalSeminormedRing α] {a₁ a₂ : α} {r₁ r₂ : ℝ}, ‖a₁‖ ≤ r₁ → ‖a₂‖ ≤ r₂ → ‖a₁ * a₂‖ ≤ r₁ * r₂
-- Mathlib.Algebra.Order.Kleene
kstar_zero : ∀ {α : Type u_1} [inst : KleeneAlgebra α], KStar.kstar 0 = 1
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.mem_entourage : ∀ {α : Type u} [uniformSpace : UniformSpace α] {β : Type u_1} [inst : SemilatticeSup β] {u : β → α},
  CauchySeq u → ∀ {V : SetRel α α}, V ∈ uniformity α → ∃ k₀, ∀ (i j : β), k₀ ≤ i → k₀ ≤ j → (u i, u j) ∈ V
-- Lean.Data.Json.Printer
Lean.Json.escape : String → optParam String "" → String
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftLeft_pos_iff : ∀ {n m : ℕ}, 0 < n <<< m ↔ 0 < n
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.mem_nhds_zero_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_3 : TopologicalSpace R] (v : Valuation R Γ₀) [v.Compatible] [IsValuativeTopology R] (s : Set R),
  s ∈ nhds 0 ↔ ∃ γ, {x | v.restrict x < ↑γ} ⊆ s
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G) (j : J) {Z : C}
  (h : s.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.ι.app j)
      (CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv h) =
    CategoryTheory.CategoryStruct.comp (w.inv.app j) (CategoryTheory.CategoryStruct.comp (s.ι.app j) h)
-- Mathlib.Order.FixedPoints
fixedPoints.instSemilatticeInfElemFixedPointsCoeOrderHom : {α : Type u} → [inst : CompleteLattice α] → (f : α →o α) → SemilatticeInf ↑(Function.fixedPoints ⇑f)
-- Mathlib.CategoryTheory.Sites.Point.Category
/-- a natural transformation, in the opposite direction  -/
CategoryTheory.GrothendieckTopology.Point.Hom.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → {Φ₁ Φ₂ : J.Point} → Φ₁.Hom Φ₂ → (Φ₂.fiber ⟶ Φ₁.fiber)
-- Std.Internal.Do.PredTrans
/-- Unfolding `dite` through `apply`.  -/
Std.Internal.Do.PredTrans.apply_dite : ∀ {α : Type u_1} {Pred : Type u} {EPred : Type v} (c : Prop) [inst : Decidable c]
  (t : c → Std.Internal.Do.PredTrans Pred EPred α) (e : ¬c → Std.Internal.Do.PredTrans Pred EPred α) (post : α → Pred)
  (epost : EPred),
  (if h : c then t h else e h).apply post epost = if h : c then (t h).apply post epost else (e h).apply post epost
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_eq_one : ∀ {r : ℝ}, r.toNNReal = 1 ↔ r = 1
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.Const.modify_eq_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {a : α} {f : β → β}
  {l : Std.DHashMap.Internal.AssocList α fun x => β},
  Std.DHashMap.Internal.AssocList.Const.modify a f l =
    Std.DHashMap.Internal.AssocList.Const.alter a (fun x => Option.map f x) l
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.range_lift_le : ∀ {α : Type u} {β : Type v} [inst : Group β] {f : α → β} {s : Subgroup β},
  Set.range f ⊆ ↑s → (FreeGroup.lift f).range ≤ s
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Matroidᵣ.ext_iff : ∀ {α : Type u_2} {x y : Matroid.Matroidᵣ α}, x = y ↔ x.toMatroid = y.toMatroid
-- Mathlib.Order.DirectedInverseSystem
/-- The projection from a Pi type to the Pi type over an initial segment of its indexing type.  -/
InverseSystem.piLTProj : {ι : Type u_1} →
  [inst : Preorder ι] → {X : ι → Type u_5} → ⦃i j : ι⦄ → i ≤ j → InverseSystem.piLT X j → InverseSystem.piLT X i
-- Mathlib.Topology.UniformSpace.Defs
IsUniformInducing.mk : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  Filter.comap (fun x => (f x.1, f x.2)) (uniformity β) = uniformity α → IsUniformInducing f
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_map : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (S : Subsemigroup M)
  (g : N →ₙ* P) (f : M →ₙ* N), Subsemigroup.map g (Subsemigroup.map f S) = Subsemigroup.map (g.comp f) S
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.IsExtendible.eq_1 : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] (σ : IntermediateField.Lifts F E K),
  σ.IsExtendible = ∀ (S : Finset E), ∃ τ ≥ σ, ↑S ⊆ ↑τ.carrier
-- Mathlib.Topology.QuasiSeparated
QuasiSeparatedSpace.mk : ∀ {α : Type u_3} [inst : TopologicalSpace α],
  (∀ (U V : Set α), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) → QuasiSeparatedSpace α
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.getKindForLetRecs : Array Lean.Elab.DefViewElabHeader → Lean.Elab.DefKind
-- Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
/-- The volume form coming from an orientation in an inner product space gives measure `1` to the
parallelepiped associated to any orthonormal basis. This is a rephrasing of
`abs_volumeForm_apply_of_orthonormal` in terms of measures.  -/
Orientation.measure_orthonormalBasis : ∀ {ι : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F]
  [inst_2 : MeasurableSpace F] [inst_3 : BorelSpace F] [inst_4 : Fintype ι] [inst_5 : FiniteDimensional ℝ F] {n : ℕ}
  [_i : Fact (Module.finrank ℝ F = n)] (o : Orientation ℝ F (Fin n)) (b : OrthonormalBasis ι ℝ F),
  o.volumeForm.measure (parallelepiped ⇑b) = 1
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_neg`. -/
SkewMonoidAlgebra.toFinsupp_neg : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroup k] (a : SkewMonoidAlgebra k G), (-a).coeff = -a.coeff
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.comp_congr : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_7}
  {M'' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : AddCommMonoid M''] [inst_5 : Module R M']
  [inst_6 : Module R M''] (e : M' ≃ₗ[R] M'') (B : LinearMap.BilinForm R M) (l r : M' →ₗ[R] M),
  (LinearMap.BilinForm.congr e) (B.comp l r) = B.comp (l ∘ₗ ↑e.symm) (r ∘ₗ ↑e.symm)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- If `s ≅ t` and `IsKan (s.whisker h)`, then `IsKan (t.whisker h)`.  -/
CategoryTheory.Bicategory.LeftLift.IsKan.whiskerOfCommute : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (s t : CategoryTheory.Bicategory.LeftLift f g) →
            (s ≅ t) → {x : B} → (h : x ⟶ c) → (s.whisker h).IsKan → (t.whisker h).IsKan
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_iff_ordConnected : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {s : Set α}, IsPreconnected s ↔ s.OrdConnected
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupportValueSet.mk.inj : ∀ {valueSet valueSet_1 : Array Lean.Lsp.CodeActionKind},
  { valueSet := valueSet } = { valueSet := valueSet_1 } → valueSet = valueSet_1
-- Lean.Server.AsyncList
Lean.AsyncList.brecOn_3.go : {ε : Type u} →
  {α : Type v} →
    {motive_1 : Lean.AsyncList ε α → Sort u_1} →
      {motive_2 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α)) → Sort u_1} →
        {motive_3 : Task (Except ε (Lean.AsyncList ε α)) → Sort u_1} →
          {motive_4 : Except ε (Lean.AsyncList ε α) → Sort u_1} →
            (t : Except ε (Lean.AsyncList ε α)) →
              ((t : Lean.AsyncList ε α) → t.below → motive_1 t) →
                ((t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_1 t → motive_2 t) →
                  ((t : Task (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_2 t → motive_3 t) →
                    ((t : Except ε (Lean.AsyncList ε α)) → Lean.AsyncList.below_3 t → motive_4 t) →
                      motive_4 t ×' Lean.AsyncList.below_3 t
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_addMonoidAlgebraMap : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (g : S₁ →+ R)
  (φ : MvPolynomial σ S₁) (m : σ →₀ ℕ), MvPolynomial.coeff m (AddMonoidAlgebra.map g φ) = g (MvPolynomial.coeff m φ)
-- Init.Data.Stream
ToStream.toStream : {collection : Type u} → {stream : outParam (Type u)} → [self : Std.ToStream collection stream] → collection → stream
-- Mathlib.LinearAlgebra.Ray
/-- Equivalence of nonzero vectors, in terms of `SameRay`.  -/
equiv_iff_sameRay : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {v₁ v₂ : RayVector R M},
  v₁ ≈ v₂ ↔ SameRay R ↑((RayVector.equiv R M) v₁) ↑((RayVector.equiv R M) v₂)