mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.mk.inj : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} {inst : Ring k}
  {inst_1 : AddCommGroup V₁} {inst_2 : AddCommGroup V₂} {inst_3 : Module k V₁} {inst_4 : Module k V₂}
  {inst_5 : AddTorsor V₁ P₁} {inst_6 : AddTorsor V₂ P₂} {toEquiv : P₁ ≃ P₂} {linear : V₁ ≃ₗ[k] V₂}
  {map_vadd' : ∀ (p : P₁) (v : V₁), toEquiv (v +ᵥ p) = linear v +ᵥ toEquiv p} {toEquiv_1 : P₁ ≃ P₂}
  {linear_1 : V₁ ≃ₗ[k] V₂} {map_vadd'_1 : ∀ (p : P₁) (v : V₁), toEquiv_1 (v +ᵥ p) = linear_1 v +ᵥ toEquiv_1 p},
  { toEquiv := toEquiv, linear := linear, map_vadd' := map_vadd' } =
      { toEquiv := toEquiv_1, linear := linear_1, map_vadd' := map_vadd'_1 } →
    toEquiv = toEquiv_1 ∧ linear = linear_1
-- Init.Data.Repr
instReprId : {α : Type u_1} → [Repr α] → Repr (id α)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Radon-Nikodym derivative with respect to the scalar multiple of a measure.
See also `rnDeriv_smul_right_of_ne_top`, which has no hypothesis on `μ` but requires finite `ν`.  -/
MeasureTheory.Measure.rnDeriv_smul_right_of_ne_top' : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν]
  [MeasureTheory.SigmaFinite μ] {r : ENNReal}, r ≠ 0 → r ≠ ⊤ → ν.rnDeriv (r • μ) =ᵐ[μ] r⁻¹ • ν.rnDeriv μ
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instBot : {R : Type u} → {M : Type v} → [inst : SMul R M] → Bot (SubMulAction R M)
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_apply_eq_zero_iff_symm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] {i j : ↥b.support},
  b.cartanMatrix i j = 0 ↔ b.cartanMatrix j i = 0
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_pre_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasColimit F] (E : CategoryTheory.Functor K J)
  [inst_4 : CategoryTheory.Limits.HasColimit (E.comp F)] (k : K) {Z : C} (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (E.comp F) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.pre F E) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (E.obj k)) h
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Result.mk.inj : ∀ {expr : Lean.Expr} {type? : Option Lean.Expr} {expr_1 : Lean.Expr} {type?_1 : Option Lean.Expr},
  { expr := expr, type? := type? } = { expr := expr_1, type? := type?_1 } → expr = expr_1 ∧ type? = type?_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.homotopyEquivNormalizedChainComplex_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  (X.homotopyEquivNormalizedChainComplex R).hom = X.toNormalizedChainComplex R
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.ExtDTreeMap.Const.ofList : {α : Type u} →
  {β : Type v} →
    List (α × β) →
      (cmp : autoParam (α → α → Ordering) Std.ExtDTreeMap.Const.ofList._auto_1) → Std.ExtDTreeMap α (fun x => β) cmp
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanFinset_coe : ∀ (R₁ : Type u_3) [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] {ι : Type u_5} (s : Finset ι) (f : ι → K),
  ↑(FractionalIdeal.spanFinset R₁ s f) = Submodule.span R₁ (f '' ↑s)
-- Mathlib.Condensed.Light.Module
/-- The category of light condensed `R`-modules, defined as sheaves of `R`-modules over
`LightProfinite.{u}` with respect to the coherent Grothendieck topology.
 -/
LightCondMod : (R : Type u) → [Ring R] → Type (u + 1)
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `derivWithin_fun_const_smul_field`.

---

A variant of `derivWithin_fun_const_smul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
derivWithin_fun_const_smul' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {𝕝 : Type u_3} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F),
  derivWithin (fun y => c • f y) s x = c • derivWithin f s x
-- Mathlib.Order.WithBot
WithTop.lt_untop_iff : ∀ {α : Type u_1} {b : α} [inst : LT α] {x : WithTop α} (hx : x ≠ ⊤), b < x.untop hx ↔ ↑b < x
-- Mathlib.Topology.ContinuousMap.Interval
/-- The extension operation from continuous maps on an interval to continuous maps on the whole
type, as a `ContinuousMap`.  -/
ContinuousMap.IccExtendCM : {α : Type u_1} →
  [inst : LinearOrder α] →
    [inst_1 : TopologicalSpace α] →
      [OrderTopology α] →
        {a b : α} → [Fact (a ≤ b)] → {E : Type u_2} → [inst_4 : TopologicalSpace E] → C(C(↑(Set.Icc a b), E), C(α, E))
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_inverse_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  {X_1 Y : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ} (f : X_1 ⟶ Y),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.inverse.obj X).map f =
    match
      match Opposite.unop X_1 with
      | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
      | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
      match Opposite.unop Y with
      | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
      | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
      match f with
      | Opposite.op f_1 =>
        match X_1, Y, f_1, f with
        | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_1 =>
          (CategoryTheory.WithTerminal.down f).op
        | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_1 =>
          CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.of (Opposite.op a))
        | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_1 =>
          CategoryTheory.CategoryStruct.id CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
      X.left.map (CategoryTheory.WithTerminal.down f)
    | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => X.hom.app x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
compactOperator_topologicalClosure : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : AddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜₁ M₁] [inst_5 : Module 𝕜₂ M₂] [inst_6 : UniformSpace M₂] [inst_7 : IsUniformAddGroup M₂]
  [inst_8 : ContinuousConstSMul 𝕜₂ M₂] [T2Space M₂] [CompleteSpace M₂],
  (compactOperator σ₁₂ M₁ M₂).topologicalClosure = compactOperator σ₁₂ M₁ M₂
-- Mathlib.Data.Nat.Find
Nat.findGreatest_of_not : ∀ {P : ℕ → Prop} [inst : DecidablePred P] {n : ℕ}, ¬P (n + 1) → Nat.findGreatest P (n + 1) = Nat.findGreatest P n
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.toProdMulOppositeHom_apply : ∀ {𝕜 : 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] (a : DoubleCentralizer 𝕜 A),
  DoubleCentralizer.toProdMulOppositeHom a = a.toProdMulOpposite
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_inter!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter! m₂).getKey? k = none
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instR1Space : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [R1Space R], R1Space (ContinuousMapZero X R)
-- Mathlib.Algebra.Ring.Int.Parity
/-- **Alias** of the reverse direction of `Int.natAbs_even`. -/
Even.natAbs : ∀ {n : ℤ}, Even n → Even n.natAbs
-- Lean.Elab.Term.TermElabM
/-- Apply the result/exception and state captured with `observing`.
We use this method to implement overloaded notation and symbols.  -/
Lean.Elab.Term.applyResult : {α : Type} → Lean.Elab.Term.TermElabResult α → Lean.Elab.TermElabM α
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The unit of an adjunction  -/
CategoryTheory.Adjunction.unit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} → (F ⊣ G) → (CategoryTheory.Functor.id C ⟶ F.comp G)
-- Mathlib.Topology.Algebra.Order.Field
IsStrictOrderedRing.topologicalRing : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜], IsTopologicalRing 𝕜
-- Lean.Meta.Sym.SynthInstance
/-- Registers `inst` as **the** instance for `type`. `synthInstance?` returns it without
running typeclass resolution, making `inst` the canonical representative for `type`.
Intended for satellite modules that construct instances for types they create themselves
(e.g., `grind linarith`'s envelope type `IntModule.OfNatModule.Q`).
 -/
Lean.Meta.Sym.registerInstance : Lean.Expr → Lean.Expr → Lean.Meta.Sym.SymM Unit
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- `of` is the canonical injection from the type to the free group over that type by sending each
element to the equivalence class of the letter that is the element.  -/
FreeGroup.of : {α : Type u} → α → FreeGroup α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.conjugate_comp : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] (φ : K →+* ℂ) (σ : k →+* K),
  (NumberField.ComplexEmbedding.conjugate φ).comp σ = NumberField.ComplexEmbedding.conjugate (φ.comp σ)
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_le_self : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) (n : ℕ), S.lowerCentralSeries n ≤ S
-- Init.Data.UInt.Lemmas
UInt8.le_total : ∀ (a b : UInt8), a ≤ b ∨ b ≤ a
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.algebraMapCLM_apply : ∀ {𝕜₁ : Type u_1} [inst : NormedField 𝕜₁] {E : Type u_3} [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜₁ E] {S : Type u_5} [inst_4 : CommSemiring S] [inst_5 : Module S E] [inst_6 : SMulCommClass 𝕜₁ S E]
  [inst_7 : SMul S 𝕜₁] [inst_8 : IsScalarTower S 𝕜₁ E] [inst_9 : ContinuousConstSMul S E]
  [inst_10 : IsTopologicalAddGroup E] (c : S) (x : E), ((algebraMap S (E →WOT[𝕜₁] E)) c) x = c • x
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.toSet_max : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W₁ W₂ : CategoryTheory.MorphismProperty C),
  (W₁ ⊔ W₂).toSet = W₁.toSet ∪ W₂.toSet
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_comp : ∀ {R : Type u} {S : Type u₁} {T : Type u_1} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Monoid T] {φ : R →* S}
  {A : Type v} {B : Type w} {C : Type w₁} [inst_3 : NonUnitalNonAssocSemiring A] [inst_4 : DistribMulAction R A]
  [inst_5 : NonUnitalNonAssocSemiring B] [inst_6 : DistribMulAction S B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction T C] {ψ : S →* T} {χ : R →* T} (f : B →ₛₙₐ[ψ] C) (g : A →ₛₙₐ[φ] B)
  [inst_9 : φ.CompTriple ψ χ], ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insertMany_empty_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] {l : List ((a : α) × β a)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).getKey? k' = some k
-- Mathlib.Data.Finset.Sort
/-- Any finite linear order order-embeds into any infinite linear order.  -/
nonempty_orderEmbedding_of_finite_infinite : ∀ (α : Type u_1) [inst : LinearOrder α] [hα : Finite α] (β : Type u_2) [inst_1 : LinearOrder β] [hβ : Infinite β],
  Nonempty (α ↪o β)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.rename_comp_toMvPolynomial : ∀ {R : Type u_1} {σ : Type u_3} {τ : Type u_4} [inst : CommSemiring R] (f : σ → τ) (a : σ),
  (MvPolynomial.rename f).comp (Polynomial.toMvPolynomial a) = Polynomial.toMvPolynomial (f a)
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionHom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] {c c' : C} {d d' : D} (f : d ⟶ d')
  (g : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
    CategoryTheory.CategoryStruct.comp ((F.map g).app d) ((F.obj c').map f)
-- Mathlib.Data.PEquiv
PEquiv.mem_ofSet_self_iff : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {a : α}, a ∈ (PEquiv.ofSet s) a ↔ a ∈ s
-- Std.Time.DateTime.WallTime
/-- Creates a `WallTime` from a `Nanosecond.Offset`. The epoch is 1970-01-01 00:00:00 in local
(civil) time, not UTC.
 -/
Std.Time.WallTime.ofNanoseconds : Std.Time.Nanosecond.Offset → Std.Time.WallTime
-- Mathlib.RingTheory.FiniteStability
Algebra.FinitePresentation.baseChange : ∀ {R : Type w₁} [inst : CommRing R] {A : Type w₂} [inst_1 : CommRing A] [inst_2 : Algebra R A] (B : Type w₃)
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FinitePresentation R A],
  Algebra.FinitePresentation B (TensorProduct R B A)
-- Mathlib.Analysis.Normed.Group.Ultra
/-- All triangles are isosceles in an ultrametric normed group.  -/
IsUltrametricDist.nnnorm_div_eq_max_of_nnnorm_div_ne_nnnorm_div : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] (x y z : S),
  ‖x / y‖₊ ≠ ‖y / z‖₊ → ‖x / z‖₊ = max ‖x / y‖₊ ‖y / z‖₊
-- Mathlib.Order.Filter.Map
Filter.map_inr_inf_map_inl : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, Filter.map Sum.inr f ⊓ Filter.map Sum.inl g = ⊥
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.cocone_naturality : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat) {j j' : J}
  (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (F.map f) (CommRingCat.Colimits.coconeMorphism F j') =
    CommRingCat.Colimits.coconeMorphism F j
-- Mathlib.LinearAlgebra.Basis.Basic
/-- Given a basis, the `i`th element of the dual basis evaluates to 0 on the `j`th element of the
basis if `j ≠ i`.  -/
Module.Basis.mk_coord_apply_ne : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : ι → M} {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)} {i j : ι},
  j ≠ i → ((Module.Basis.mk hli hsp).coord i) (v j) = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
le_or_lt_of_mul_le_mul : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α] [MulLeftMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α},
  a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.instHasFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [CategoryTheory.PreGaloisCategory C],
  CategoryTheory.Limits.HasFiniteLimits C
-- Mathlib.Analysis.Analytic.Binomial
binomialSeries_eq_ordinaryHypergeometricSeries : ∀ {𝕂 : Type u} [inst : Field 𝕂] [inst_1 : CharZero 𝕂] {𝔸 : Type v} [inst_2 : Ring 𝔸] [inst_3 : Algebra 𝕂 𝔸]
  [inst_4 : TopologicalSpace 𝔸] [inst_5 : IsTopologicalRing 𝔸] {a b : 𝕂},
  (∀ (k : ℕ), ↑k ≠ -b) →
    binomialSeries 𝔸 a = (ordinaryHypergeometricSeries 𝔸 (-a) b b).compContinuousLinearMap (-ContinuousLinearMap.id 𝕂 𝔸)
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The metric between two curves `α` and `β` is the supremum of the metric between `α t` and `β t`
over all `t` in the domain. This is finite when the domain is compact, such as a closed
interval in our case.  -/
ODE.FunSpace.instMetricSpace : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} → {t₀ : ↑(Set.Icc tmin tmax)} → {x₀ : E} → {r L : NNReal} → MetricSpace (ODE.FunSpace t₀ x₀ r L)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.map_map_of_aemeasurable : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {g : β → γ} {f : α → β},
  AEMeasurable g (MeasureTheory.Measure.map f μ) →
    AEMeasurable f μ → MeasureTheory.Measure.map g (MeasureTheory.Measure.map f μ) = MeasureTheory.Measure.map (g ∘ f) μ
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_bot_iff : ∀ {α : Type u_1} {r : α → α → Prop} {sym : Std.Symm r}, Sym2.fromRel sym = ∅ ↔ r = ⊥
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.NonnegCoeffs.num : ∀ c ≥ 0, (Lean.Grind.CommRing.Poly.num c).NonnegCoeffs
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.associator_inv : {B : Type u} →
  [inst : Quiver B] →
    {a b c d : CategoryTheory.FreeBicategory B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            CategoryTheory.FreeBicategory.Hom₂
              (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_some_getD_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, t.contains a = true → t[a]? = some (t.getD a fallback)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the reverse direction of `SimpleGraph.Walk.isCycle_mapLe`. -/
SimpleGraph.Walk.IsCycle.mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u},
  p.IsCycle → (SimpleGraph.Walk.mapLe h p).IsCycle
-- Mathlib.Order.Sublattice
Sublattice.le_prod_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {M : Sublattice β}
  {N : Sublattice (α × β)}, N ≤ L.prod M ↔ N ≤ Sublattice.comap LatticeHom.fst L ∧ N ≤ Sublattice.comap LatticeHom.snd M
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.lt_mul : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.mul_ineq_cert p₁ k p = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ < 0 → Lean.Grind.CommRing.Poly.denote ctx p < 0
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.hasWeakSheafify_of_isEquivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) (A : Type u_4)
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  [(G.sheafPushforwardContinuous A J K).IsEquivalence] [CategoryTheory.HasWeakSheafify J A],
  CategoryTheory.HasWeakSheafify K A
-- Mathlib.Condensed.TopComparison
/-- If `G` preserves finite coproducts (which is the case when `C` is `CompHaus`, `Profinite` or
`Stonean`), then `yonedaPresheaf` preserves finite products, which is required to be a sheaf for
the extensive topology.
 -/
instPreservesFiniteProductsOppositeYonedaPresheafOfPreservesFiniteCoproductsTopCat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C TopCat) (X : Type w')
  [inst_1 : TopologicalSpace X] [CategoryTheory.Limits.PreservesFiniteCoproducts G],
  CategoryTheory.Limits.PreservesFiniteProducts (ContinuousMap.yonedaPresheaf G X)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesLimit_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D), Subsingleton (CategoryTheory.Limits.PreservesLimit K F)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.copy_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) (m : F.I ⟶ Y) (e : X ⟶ F.I)
  (hm : autoParam (m = F.m) CategoryTheory.Limits.MonoFactorisation.copy._auto_1)
  (he : autoParam (e = F.e) CategoryTheory.Limits.MonoFactorisation.copy._auto_3), (F.copy m e hm he).m = m
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β}
  {fallback : α}, (t.insert k v).minKeyD fallback = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.Order.Filter.ENNReal
ENNReal.limsup_const_mul : ∀ {α : Type u_1} {f : Filter α} [CountableInterFilter f] {u : α → ENNReal} {a : ENNReal},
  Filter.limsup (fun x => a * u x) f = a * Filter.limsup u f
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_vadd_closedBall : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ℝ),
  (fun x => c +ᵥ x) ⁻¹' Metric.closedBall x r = Metric.closedBall (-c +ᵥ x) r
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.instFinallySmallOfHasTerminal : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.Limits.HasTerminal J],
  CategoryTheory.FinallySmall J
-- Mathlib.Order.Atoms
/-- **Alias** of the forward direction of `isAtom_compl`. -/
IsAtom.of_compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α}, IsAtom aᶜ → IsCoatom a
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_adjunction_id_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {L R : CategoryTheory.Functor C C} (adj : L ⊣ R)
  (α : R ⟶ CategoryTheory.Functor.id C) (c : C),
  ((CategoryTheory.conjugateEquiv adj CategoryTheory.Adjunction.id).symm α).app c =
    CategoryTheory.CategoryStruct.comp (adj.unit.app c) (α.app (L.obj c))
-- Mathlib.Topology.Homotopy.Product
Path.Homotopic.pi_lift : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {as bs : (i : ι) → X i}
  (γ : (i : ι) → Path (as i) (bs i)),
  (Path.Homotopic.pi fun i => Path.Homotopic.Quotient.mk (γ i)) = Path.Homotopic.Quotient.mk (Path.pi γ)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh_two_mul : ∀ (x : ℂ), Complex.cosh (2 * x) = Complex.cosh x ^ 2 + Complex.sinh x ^ 2
-- Mathlib.SetTheory.Lists
Lists'.mem_of_subset : ∀ {α : Type u_1} {a : Lists α} {l₁ l₂ : Lists' α true}, l₁ ⊆ l₂ → a ∈ l₁ → a ∈ l₂
-- Mathlib.Data.Fintype.EquivFin
instFiniteProp : ∀ (p : Prop), Finite p
-- Mathlib.Computability.Primrec.Basic
Primcodable.ulower : {α : Type u_1} → [inst : Primcodable α] → Primcodable (ULower α)