mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.le_nhds_iff_forall_dual_apply_le_nhds : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] {l : Filter (E →SWOT[σ] F)} {A : E →SWOT[σ] F},
  l ≤ nhds A ↔ ∀ (x : E) (y : StrongDual 𝕜₂ F), Filter.map (fun T => y (T x)) l ≤ nhds (y (A x))
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to an `Int8`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toInt8 : Float32.Model → Int8
-- Init.Data.List.Basic
List.take_zero : ∀ {α : Type u} {l : List α}, List.take 0 l = []
-- Mathlib.RingTheory.Localization.Pi
/-- Let `M` be a submonoid of a direct product of commutative rings `R i`.
If each `R i` has maximal nilradical then the direct product `∏ R i` surjects onto the
localization of `∏ R i` at `M`.  -/
IsLocalization.algebraMap_pi_surjective_of_isLocalization : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → CommSemiring (R i)] (S' : Type u_4) [inst_1 : CommSemiring S']
  [inst_2 : Algebra ((i : ι) → R i) S'] (M : Submonoid ((i : ι) → R i)) [∀ (i : ι), Ring.KrullDimLE 0 (R i)]
  [∀ (i : ι), IsLocalRing (R i)] [IsLocalization M S'] [Finite ι], Function.Surjective ⇑(algebraMap ((i : ι) → R i) S')
-- Mathlib.CategoryTheory.Topos.Sheaf
/-- The truth morphism in the category of presheaves. At each component `X : C`, it is the constant
map returning `⊤ : Sieve X`.  -/
CategoryTheory.Presheaf.truth : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (CategoryTheory.Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1} ⟶ CategoryTheory.Functor.sieves C
-- Batteries.Data.Array.Basic
/-- Fold a monadic function `f` over the subarray from the left, returning the list of partial results.
 -/
Subarray.scanlM : {m : Type u_1 → Type u_2} → {β : Type u_1} → {α : Type u_3} → [Monad m] → (β → α → m β) → β → Subarray α → m (Array β)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whiskeringEquivalence_functor : ∀ {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} (e : K ≌ J),
  (CategoryTheory.Limits.Cone.whiskeringEquivalence e).functor = CategoryTheory.Limits.Cone.whiskering e.functor
-- Mathlib.Algebra.Order.Group.Synonym
toColex_smul' : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : β) (a : α), toColex b • a = b • a
-- Aesop.RuleTac.Cases
Aesop.CasesTarget'.patterns.injEq : ∀ (ps ps_1 : Array (Lean.Expr × Lean.Meta.SavedState)),
  (Aesop.CasesTarget'.patterns ps = Aesop.CasesTarget'.patterns ps_1) = (ps = ps_1)
-- Init.Data.Array.Find
Array.findIdx?_eq_some_le_of_findIdx?_eq_some : ∀ {α : Type u_1} {xs : Array α} {p q : α → Bool},
  (∀ x ∈ xs, p x = true → q x = true) → ∀ {i : ℕ}, Array.findIdx? p xs = some i → ∃ j ≤ i, Array.findIdx? q xs = some j
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` preserves the limit of `K` if it creates the limit and `K ⋙ F` has the limit.  -/
CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit : ∀ {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) [CategoryTheory.CreatesLimit K F] [CategoryTheory.Limits.HasLimit (K.comp F)],
  CategoryTheory.Limits.PreservesLimit K F
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- The natural transformation `H ⟶ F` for an adjoint triple `F ⊣ G ⊣ H` with `G` fully faithful
is also equal to the whiskered unit `H ⟶ F ⋙ G ⋙ H` of the first adjunction followed by the
inverse of the whiskered unit `F ⟶ F ⋙ G ⋙ H` of the second.  -/
CategoryTheory.Adjunction.Triple.rightToLeft_eq_units : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful],
  t.rightToLeft =
    CategoryTheory.CategoryStruct.comp H.leftUnitor.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight t.adj₁.unit H)
        (CategoryTheory.CategoryStruct.comp (F.associator G H).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (F.whiskerLeft t.adj₂.unit)) F.rightUnitor.hom)))
-- Mathlib.Algebra.Group.Fin.Basic
Fin.lt_sub_one_iff : ∀ {n : ℕ} {k : Fin (n + 2)}, k < k - 1 ↔ k = 0
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.instNontrivialSubtypeLeOfNatOfAddLeftMono : ∀ {α : Type u_1} [Nontrivial α] [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α], Nontrivial { x // 0 ≤ x }
-- Mathlib.Algebra.Group.AddChar
/-- The product of `mulShift ψ r` and `mulShift ψ s` is `mulShift ψ (r + s)`.  -/
AddChar.mulShift_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M) (r s : R),
  ψ.mulShift r * ψ.mulShift s = ψ.mulShift (r + s)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- For a function on `ℝ`, the Laplacian is the second derivative.  -/
InnerProductSpace.laplacian_eq_iteratedDeriv_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {e : ℝ} (f : ℝ → F),
  Laplacian.laplacian f e = iteratedDeriv 2 f e
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.zariskisMainProperty_iff_exists_saturation_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal S},
  Algebra.ZariskisMainProperty R p ↔
    ∃ r ∉ p, ∃ (h : IsIntegral R r), (integralClosure R S).saturation (Submonoid.powers r) ⋯ = ⊤
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_eventually_congr_set' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E}
  {f : E → F} {x : E} (y : E),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → ∀ (n : ℕ), iteratedFDerivWithin 𝕜 n f s =ᶠ[nhds x] iteratedFDerivWithin 𝕜 n f t
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.instUniformContinuousConstSMulReal : ∀ {R : Type u_1} [inst : CommRing R] {T : Type u_3} [inst_1 : Field T] [inst_2 : Algebra R T] (w : AbsoluteValue T ℝ),
  UniformContinuousConstSMul R (WithAbs w)
-- Mathlib.Order.CompleteLattice.Defs
/-- `⊤ \ a` is `￢a`  -/
CompleteLinearOrder.top_sdiff : ∀ {α : Type u_8} [self : CompleteLinearOrder α] (a : α), ⊤ \ a = ￢a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Color.mk.injEq : ∀ (red green blue alpha red_1 green_1 blue_1 alpha_1 : Float),
  ({ red := red, green := green, blue := blue, alpha := alpha } =
      { red := red_1, green := green_1, blue := blue_1, alpha := alpha_1 }) =
    (red = red_1 ∧ green = green_1 ∧ blue = blue_1 ∧ alpha = alpha_1)
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExpKernel_apply_eq_condDistrib : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : Nonempty Ω] {ω : Ω},
  (ProbabilityTheory.condExpKernel μ m) ω = (ProbabilityTheory.condDistrib id id μ) (id ω)
-- Batteries.Data.BinomialHeap.Basic
/-- `node` is a well formed forest of rank `rank` with `val` at the root.  -/
Batteries.BinomialHeap.Imp.FindMin.WF.node : ∀ {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α}
  (self : Batteries.BinomialHeap.Imp.FindMin.WF le res),
  Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node self.rank
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} [inst_2 : Inhabited (β k')]
  {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast! k' (Std.Internal.List.alterKey k f l) =
      if heq : (k == k') = true then (Option.map (cast ⋯) (f (Std.Internal.List.getValueCast? k l))).get!
      else Std.Internal.List.getValueCast! k' l
-- Mathlib.Data.Rel
SetRel.IsTrans.sInter : ∀ {α : Type u_1} {ℛ : Set (SetRel α α)}, (∀ R ∈ ℛ, R.IsTrans) → SetRel.IsTrans (⋂₀ ℛ)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_of_add_le_left : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] {a b c : α}, a + b ≤ c → a ≤ c
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_mul`. -/
ENat.coe_mul : ∀ (m n : ℕ), ↑(m * n) = ↑m * ↑n
-- Mathlib.Tactic.Core
Mathlib.Tactic.withArgs : Lean.ParserDescr
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.instZero : {α : Type u_1} → [inst : MeasurableSpace α] → Zero (MeasureTheory.JordanDecomposition α)
-- Mathlib.Tactic.Subsingleton
/-- Returns the expression `Subsingleton ty`.  -/
Lean.Meta.mkSubsingleton : Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.instTrans : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Trans Std.HashMap.Equiv Std.HashMap.Equiv Std.HashMap.Equiv
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHom.id_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] (a : α), (ContinuousOrderHom.id α) a = a
-- Mathlib.Tactic.Module
/-- Lemmas used to post-process the result of the `match_scalars` and `module` tactics by converting
the `algebraMap` operations which (which proliferate in the constructed scalar goals) to more
familiar forms: `ℕ`, `ℤ` and `ℚ` casts.  -/
Mathlib.Tactic.Module.algebraMapThms : Array Lean.Name
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_vadd : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι]
  [inst_5 : (i : ι) → VAdd R (G i)] [inst_6 : VAdd R C]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)]
  [∀ (i : ι), AddActionHomClass (H i) R (G i) C] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (r : R) (x : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h (r +ᵥ x) = r +ᵥ DirectLimit.lift f (fun x => ⇑(g x)) h x
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.instInhabitedCheckResult.default : Lean.Meta.Grind.CheckResult
-- Mathlib.CategoryTheory.Sites.Point.Map
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point) (F : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D) [inst_2 : F.IsCocontinuous J K]
  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] {A : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} A]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] {P Q : CategoryTheory.Functor Dᵒᵖ A} (g : P ⟶ Q)
  (X : C) (x : Φ.fiber.obj X) {F_1 : A → A → Type uF} {carrier : A → Type w_1}
  {instFunLike : (X Y : A) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_6 : CategoryTheory.ConcreteCategory A F_1]
  (x_1 : carrier (P.obj (Opposite.op (F.obj X)))),
  (CategoryTheory.ConcreteCategory.hom ((Φ.map F K).presheafFiber.map g))
      ((CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiberMap F K P X x)) x_1) =
    (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiberMap F K Q X x))
      ((CategoryTheory.ConcreteCategory.hom (g.app (Opposite.op (F.obj X)))) x_1)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_orthogonal`. -/
Submodule.orthogonalProjection_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection] (u : E),
  Kᗮ.orthogonalProjectionOnto u = ⟨u - K.starProjection u, ⋯⟩
-- Mathlib.Algebra.Group.Action.Pi
Pi.smul_def' : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → SMul (α i) (β i)] (s : (i : ι) → α i)
  (x : (i : ι) → β i), s • x = fun i => s i • x i
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The neighbor set of `w ∈ sᶜ` in `G.between s sᶜ` excludes the vertices in `sᶜ` adjacent to `w`
in `G`.  -/
SimpleGraph.neighborSet_subset_between_union_compl : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} {s : Set V},
  w ∈ sᶜ → G.neighborSet w ⊆ (SimpleGraph.between s sᶜ G).neighborSet w ∪ sᶜ
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.saturation_sSup : ∀ {M : Type u_1} [inst : AddZeroClass M] {f : Set (AddSubmonoid M)}, (sSup f).saturation = ⨆ s ∈ f, s.saturation
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.pos_real_im : ∀ (x : { x // 0 < x }) (z : UpperHalfPlane), (x • z).im = ↑x * z.im
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Makes an ordered group isomorphism from a proof that the map preserves multiplication.  -/
OrderMonoidIso.mk' : {α : Type u_2} →
  {β : Type u_3} →
    {x : CommGroup α} →
      {x_1 : Preorder α} →
        {x_2 : CommGroup β} →
          {x_3 : PartialOrder β} →
            (f : α ≃ β) → (∀ {a b : α}, f a ≤ f b ↔ a ≤ b) → (∀ (a b : α), f (a * b) = f a * f b) → α ≃*o β
-- Mathlib.RingTheory.DualNumber
DualNumber.maximalIdeal_eq_span_singleton_eps : ∀ {K : Type u_2} [inst : Field K], IsLocalRing.maximalIdeal (DualNumber K) = Ideal.span {DualNumber.eps}
-- Init.Data.SInt.Float32
/-- Obtains the `Float32` whose value is the same as the given `Int8`.

This function does not reduce in the kernel.
 -/
Int8.toFloat32 : Int8 → Float32
-- Std.Time.Format.Modifier
Std.Time.instInhabitedNumber.default : Std.Time.Number
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.homogeneousSubmodule_one_pow : ∀ {σ : Type u_1} (R : Type u_3) [inst : CommSemiring R] (n : ℕ),
  MvPolynomial.homogeneousSubmodule σ R 1 ^ n = MvPolynomial.homogeneousSubmodule σ R n
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (e : F ≅ F')
  (X : CategoryTheory.Grp C), ((CategoryTheory.Functor.mapGrpNatIso e).hom.app X).hom.hom = e.hom.app X.X
-- Mathlib.Algebra.Notation.Prod
Prod.vadd_fst : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : VAdd E α] [inst_1 : VAdd E β] (c : E) (p : α × β),
  (c +ᵥ p).1 = c +ᵥ p.1
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instDistribMulActionOfContinuousConstSMul : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_3} →
      {M : Type u_5} →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : Monoid R] →
            [inst_3 : AddMonoid M] →
              [inst_4 : DistribMulAction R M] →
                [inst_5 : ContinuousAdd M] → [ContinuousConstSMul R M] → DistribMulAction R C(α, M)
-- Mathlib.Control.LawfulFix
LawfulFix.fix_eq : ∀ {α : Type u_3} {inst : OmegaCompletePartialOrder α} [self : LawfulFix α] {f : α → α},
  OmegaCompletePartialOrder.ωScottContinuous f → Fix.fix f = f (Fix.fix f)
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- Structure which is a helper in order to show that a functor is monoidal. It
consists of isomorphisms `εIso` and `μIso` such that the morphisms `.hom` induced
by these isomorphisms satisfy the axioms of lax monoidal functors.  -/
CategoryTheory.Functor.CoreMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [CategoryTheory.MonoidalCategory D] → CategoryTheory.Functor C D → Type (max u₁ v₂)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
/-- The bijection `(𝟙_ SSet ⟶ K) ≃ K _⦋0⦌`.  -/
SSet.unitHomEquiv : (K : SSet) → (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet ⟶ K) ≃ K.obj (Opposite.op { len := 0 })
-- Mathlib.Topology.Algebra.Monoid.Defs
Filter.tendsto_of_sub_tendsto_zero : ∀ {α : Type u_2} {E : Type u_3} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [ContinuousAdd E] {f g : α → E}
  (m : E) {x : Filter α}, Filter.Tendsto f x (nhds m) → Filter.Tendsto (g - f) x (nhds 0) → Filter.Tendsto g x (nhds m)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.cofan_inj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C}
  (i : 𝒜),
  (CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i =
    { f := fun x => ⟨i, x⟩, φ := fun x => CategoryTheory.CategoryStruct.id ((f i).obj x) }
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.instMulZeroOneClass : {α : Type u_1} → [MulZeroOneClass α] → MulZeroOneClass αᵐᵒᵖ
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.c_add_pf : ∀ {α : Type u_1} {b c : α} [inst : Add α], b = c → ∀ (a : α), a + b = a + c
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.le_uniformizer_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] [inst_2 : ValuativeRel.IsDiscrete R]
  {a : ValuativeRel.ValueGroupWithZero R}, a ≤ ValuativeRel.uniformizer R ↔ a < 1
-- Init.Data.UInt.Lemmas
USize.toUInt16_ofNatTruncate_of_le : ∀ {n : ℕ},
  USize.size ≤ n →
    (USize.ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1
-- Mathlib.Topology.MetricSpace.Closeds
/-- **Alias** of `TopologicalSpace.NonemptyCompacts.isometry_singleton`. -/
EMetric.NonemptyCompacts.isometry_singleton : ∀ {α : Type u_1} [inst : EMetricSpace α], Isometry fun x => {x}
-- Mathlib.Algebra.Algebra.Equiv
/-- Upgrade a linear equivalence to an algebra equivalence,
given that it distributes over multiplication and the identity
 -/
AlgEquiv.ofLinearEquiv : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] →
            [inst_3 : Algebra R A₁] →
              [inst_4 : Algebra R A₂] →
                (l : A₁ ≃ₗ[R] A₂) → l 1 = 1 → (∀ (x y : A₁), l (x * y) = l x * l y) → A₁ ≃ₐ[R] A₂
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.map_obj : ∀ {I : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} (g : J → I)
  (j : J) (X : C (g j)), (CategoryTheory.Sigma.map C g).obj ⟨j, X⟩ = ⟨g j, X⟩
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.isEmpty_sliceFrom : ∀ {s : String.Slice} {p : s.Pos}, (s.sliceFrom p).isEmpty = true ↔ p = s.endPos
-- Mathlib.RingTheory.Congruence.Defs
/-- The map sending a congruence relation to its underlying binary relation is injective.  -/
RingCon.ext' : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, ⇑c = ⇑d → c = d
-- Std.Http.Internal.IndexMultiMap
/-- Checks if the map is empty.
 -/
Std.Internal.IndexMultiMap.isEmpty : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.Internal.IndexMultiMap α β → Bool
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousAt_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Type u_4} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f : ι → α → γ} {a : Finset ι},
  (∀ i ∈ a, LowerSemicontinuousAt (f i) x) → LowerSemicontinuousAt (fun z => ∑ i ∈ a, f i z) x
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsCofibrant Y]
  [inst_4 : HomotopicalAlgebra.IsFibrant X] [inst_5 : HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y),
  HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight.symm
      (HomotopicalAlgebra.BifibrantObject.toHoCat.map (HomotopicalAlgebra.BifibrantObject.homMk f)) =
    HomotopicalAlgebra.RightHomotopyClass.mk f
-- Mathlib.Condensed.TopCatAdjunction
CondensedSet.topCatAdjunctionUnit_hom_app : ∀ (X : CondensedSet) (S : CompHausᵒᵖ),
  X.topCatAdjunctionUnit.hom.app S =
    TypeCat.ofHom fun x =>
      {
        toFun := fun s =>
          (CategoryTheory.ConcreteCategory.hom (X.obj.map (CompHausLike.const (CompHaus.of PUnit.{u + 1}) s).op)) x,
        continuous_toFun := ⋯ }
-- Lean.Elab.MutualInductive
Lean.Elab.Command.PreElabHeaderResult.mk.inj : ∀ {view : Lean.Elab.Command.InductiveView} {levelNames : List Lean.Name} {numParams : ℕ} {type : Lean.Expr}
  {origParams : Array Lean.Expr} {view_1 : Lean.Elab.Command.InductiveView} {levelNames_1 : List Lean.Name}
  {numParams_1 : ℕ} {type_1 : Lean.Expr} {origParams_1 : Array Lean.Expr},
  { view := view, levelNames := levelNames, numParams := numParams, type := type, origParams := origParams } =
      { view := view_1, levelNames := levelNames_1, numParams := numParams_1, type := type_1,
        origParams := origParams_1 } →
    view = view_1 ∧ levelNames = levelNames_1 ∧ numParams = numParams_1 ∧ type = type_1 ∧ origParams = origParams_1
-- Mathlib.Data.Fintype.BigOperators
Fintype.prod_bool : ∀ {α : Type u_1} [inst : CommMonoid α] (f : Bool → α), ∏ b, f b = f true * f false
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_add : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Add β]
  [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (f i + f j) (f k + f l) κ μ
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.append.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (x : Turing.ListBlank Γ), Turing.ListBlank.append [] x = x
-- Mathlib.Analysis.Normed.Algebra.Ultra
/-- Let `K` be a normed field. If a normed division ring `L` is a normed `K`-algebra,
then `L` is ultrametric (i.e. the norm on `L` is nonarchimedean) if `K` is.
 -/
IsUltrametricDist.of_normedAlgebra : ∀ (K : Type u_1) {L : Type u_2} [inst : NormedField K] [inst_1 : NormedDivisionRing L] [NormedAlgebra K L]
  [h : IsUltrametricDist K], IsUltrametricDist L
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.domExtend_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {s : Set B} (hps : IsOpen (proj ⁻¹' s)) (e : Bundle.Trivialization F fun z => proj ↑z)
  [inst_3 : Nonempty (Z → F)],
  (Bundle.Trivialization.domExtend hps e).source = Subtype.val '' e.toPretrivialization.source
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Complex.sinh` is complex analytic.  -/
Complex.analyticAt_sinh : ∀ {x : ℂ}, AnalyticAt ℂ Complex.sinh x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.contains'.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_1 ()