mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.iteratedLineDerivOp_const_eq_iter_lineDerivOp : ∀ {V : Type u_11} {E : Type u_12} [inst : LineDeriv V E E] (n : ℕ) (y : V) (f : E),
  LineDeriv.iteratedLineDerivOp (fun x => y) f = (LineDeriv.lineDerivOp y)^[n] f
-- Init.Data.Array.Lemmas
Array.contains_filterMap : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {xs : Array α} {x : β} {f : α → Option β},
  (Array.filterMap f xs).contains x = xs.any fun a => Option.any (fun b => x == b) (f a)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.codisjoint_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M}, Codisjoint ↑N ↑N' ↔ Codisjoint N N'
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.irreducible_pow_sup : ∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I J : Ideal T},
  I ≠ ⊥ →
    Irreducible J → ∀ (n : ℕ), J ^ n ⊔ I = J ^ min (Multiset.count J (UniqueFactorizationMonoid.normalizedFactors I)) n
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.evalCoeff.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  (x : M) (c : FiniteArchimedeanClass M),
  f.evalCoeff x c = if h : ∃ y, ↑y - x ∈ FiniteArchimedeanClass.ball K c then (ofLex (↑↑f h.choose)).coeff c else 0
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- The restriction of a reflexive, non-degenerate bilinear form on the orthogonal complement of
the span of a singleton is also non-degenerate.  -/
LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton : ∀ {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),
  B.Nondegenerate → B.IsRefl → ∀ {x : V}, (B x) x ≠ 0 → (B.restrict (B.orthogonal (K ∙ x))).Nondegenerate
-- Mathlib.Tactic.Linter.DocString
/-- The "DocString" linter validates style conventions regarding doc-string formatting.
 -/
Mathlib.Linter.linter.style.docString : Lean.Option Bool
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.dropWhile.eq_1 : ∀ (x : Char → Bool) (s : String) (b e : String.Pos.Raw),
  { str := s, startPos := b, stopPos := e }.dropWhile x =
    { str := s, startPos := Substring.Raw.takeWhileAux s e x b, stopPos := e }
-- Mathlib.Topology.MetricSpace.Infsep
Set.le_einfsep_iff : ∀ {α : Type u_1} [inst : EDist α] {s : Set α} {d : ENNReal}, d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.funLike : {R : Type u} →
  {ι : Type v} →
    {M₁ : ι → Type w₁} →
      {M₂ : Type w₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] →
                  [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_6 : TopologicalSpace M₂] → FunLike (ContinuousMultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Mathlib.Data.Vector.Basic
/-- Accessing the nth element of a vector made up
of one element `x : α` is `x` itself.  -/
List.Vector.get_cons_nil : ∀ {α : Type u_1} {ix : Fin 1} (x : α), (x ::ᵥ List.Vector.nil).get ix = x
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.hom_inv_leftUnitor : ∀ {R : Type u} [inst : CommSemiring R] {M : SemimoduleCat R},
  SemimoduleCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv = ↑(TensorProduct.lid R ↑M).symm
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_pow : ∀ {α : Type u_1} {N : Type u_10} [inst : CommMonoid N] [inst_1 : Fintype α] (f : α →₀ ℕ) (g : α → N),
  (f.prod fun a b => g a ^ b) = ∏ a, g a ^ f a
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.instInhabitedCommandCodeActionEntry : Inhabited Lean.CodeAction.CommandCodeActionEntry
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.mul` for matrix multiplication.  -/
mulLinearMap : {l : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} →
      (R : Type u_5) →
        {A : Type u_6} →
          [Fintype m] →
            [inst : CommSemiring R] →
              [inst_1 : NonUnitalNonAssocSemiring A] →
                [inst_2 : Module R A] →
                  [SMulCommClass R A A] → [IsScalarTower R A A] → Matrix l m A →ₗ[R] Matrix m n A →ₗ[R] Matrix l n A
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.zsmul_add_modEq : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a : G} (z : ℤ), z • p + a ≡ a [PMOD p]
-- Mathlib.Data.PNat.Prime
PNat.dvd_lcm_left : ∀ (n m : ℕ+), n ∣ n.lcm m
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- Right-multiplying a vector by a matrix in `SL(2, ℤ)` doesn't change its gcd.  -/
EisensteinSeries.vecMulSL_gcd : ∀ {r : ℕ} [NeZero r] {v : Fin 2 → ℤ},
  EisensteinSeries.finGcdMap v = r →
    ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), EisensteinSeries.finGcdMap (Matrix.vecMul v ↑A) = r
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.equiv_iff_keys_eq : ∀ {α : Type u} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.keys = t₂.keys)
-- Init.Data.UInt.Lemmas
UInt64.mod_eq_of_lt : ∀ {a b : UInt64}, a < b → a % b = a
-- Mathlib.Topology.Bases
/-- A first-countable space is one in which every point has a
countable neighborhood basis.  -/
FirstCountableTopology : (α : Type u) → [t : TopologicalSpace α] → Prop
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.const_map_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.CosimplicialObject.Augmented.const.map f).right = (CategoryTheory.CosimplicialObject.const C).map f
-- Mathlib.Topology.Algebra.Order.Field
tendsto_zpow_atTop_zero : ∀ {𝕜 : Type u_1} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {n : ℤ}, n < 0 → Filter.Tendsto (fun x => x ^ n) Filter.atTop (nhds 0)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.prodMap_contLinear : ∀ {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {P₄ : Type u_14} {V₁ : Type u_15} {V₂ : Type u_16}
  {V₃ : Type u_17} {V₄ : Type u_18} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂]
  [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : TopologicalSpace P₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [inst_15 : AddTorsor V₄ P₄] [inst_16 : TopologicalSpace P₄] [inst_17 : TopologicalSpace V₁]
  [inst_18 : IsTopologicalAddTorsor P₁] [inst_19 : TopologicalSpace V₂] [inst_20 : IsTopologicalAddTorsor P₂]
  [inst_21 : TopologicalSpace V₃] [inst_22 : IsTopologicalAddTorsor P₃] [inst_23 : TopologicalSpace V₄]
  [inst_24 : IsTopologicalAddTorsor P₄] (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄),
  (f.prodMap g).contLinear = f.contLinear.prodMap g.contLinear
-- Mathlib.Topology.Sober
QuasiSober.inter_of_isClosed_of_quasiSober_right : ∀ {α : Type u_1} [inst : TopologicalSpace α] {V : Set α} (W : Set α) [QuasiSober ↑V], IsClosed W → QuasiSober ↑(W ∩ V)
-- Mathlib.Data.Rat.Cast.Order
NNRat.ofNat_lt_cast : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} {n : ℕ}
  [inst_3 : n.AtLeastTwo], OfNat.ofNat n < ↑p ↔ OfNat.ofNat n < p
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKey!_le_maxKey!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α} {v : β}, (cmp t.maxKey! (t.insertIfNew k v).maxKey!).isLE = true
-- Lean.Parser.Term
Lean.Parser.Term.withAnonymousAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.List.MinMaxIdx
List.minIdxOn_eq_get_minIdxOn? : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.minIdxOn f xs h = (List.minIdxOn? f xs).get ⋯
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.toPath_mem_paths : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y}, W f → W.paths f.toPath
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.map_id_assoc : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (self : CategoryTheory.EnrichedFunctor V C D) (X : C) {Z : V} (h : (self.obj X ⟶[V] self.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V X) (CategoryTheory.CategoryStruct.comp (self.map X X) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eId V (self.obj X)) h
-- Mathlib.SetTheory.ZFC.PSet
PSet.Equiv.trans : ∀ {x : PSet.{u_1}} {y : PSet.{u_2}} {z : PSet.{u_3}}, x.Equiv y → y.Equiv z → x.Equiv z
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getMatchKeyArgs : Lean.Expr → Bool → Lean.MetaM (Lean.Meta.DiscrTree.Key × Array Lean.Expr)
-- Init.Data.List.Basic
/-- Alternates the elements of `l` with `sep`.

`O(|l|)`.

This is a tail-recursive version of `List.intersperse`, used at runtime.

Examples:
* `List.intersperseTR "then" [] = []`
* `List.intersperseTR "then" ["walk"] = ["walk"]`
* `List.intersperseTR "then" ["walk", "run"] = ["walk", "then", "run"]`
* `List.intersperseTR "then" ["walk", "run", "rest"] = ["walk", "then", "run", "then", "rest"]`
 -/
List.intersperseTR : {α : Type u} → α → List α → List α
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- the kernel condition for `ι`  -/
CategoryTheory.ShortComplex.RightHomologyData.wι_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.RightHomologyData) {Z : C}
  (h : (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.ι
      (CategoryTheory.CategoryStruct.comp (self.hp.desc (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯)) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.InnerProductSpace.Basic
DFinsupp.sum_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : DecidableEq ι] {α : ι → Type u_5} [inst_4 : (i : ι) → AddZeroClass (α i)]
  [inst_5 : (i : ι) → (x : α i) → Decidable (x ≠ 0)] (f : (i : ι) → α i → E) (l : Π₀ (i : ι), α i) (x : E),
  inner 𝕜 (l.sum f) x = l.sum fun i a => inner 𝕜 (f i a) x
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction.match_1.splitter : {α : Type u_2} →
  {β : Type u_1} →
    (motive : Std.Tactic.BVDecide.LRAT.Action β α → Sort u_3) →
      (x : Std.Tactic.BVDecide.LRAT.Action β α) →
        ((id : ℕ) →
            (c : β) →
              (p : Std.Sat.Literal α) →
                (rupHints : Array ℕ) →
                  (ratHints : Array (ℕ × Array ℕ)) →
                    motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints)) →
          ((x : Std.Tactic.BVDecide.LRAT.Action β α) →
              (∀ (id : ℕ) (c : β) (p : Std.Sat.Literal α) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ)),
                  x = Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints → False) →
                motive x) →
            motive x
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderComposition.universally : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C]
  (P : CategoryTheory.MorphismProperty C) [hP : P.IsStableUnderComposition], P.universally.IsStableUnderComposition
-- Mathlib.Data.List.AList
AList.lookup_empty : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α), AList.lookup a ∅ = none
-- Std.Sync.Broadcast
/-- Index of the oldest message still available for lagging receivers.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.read : {α : Type} → (self : Std.Bounded.State✝ α) → Fin ↑(Std.Bounded.State.capacity✝ self)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.measurable_polarCoord_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], Measurable ↑(NumberField.mixedEmbedding.polarCoord K).symm
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.isSimpOnly : Lean.TSyntax `tactic → Bool
-- Lean.Elab.App
/-- Throw an error message that describes why each possible interpretation for the overloaded notation and symbols did not work.
We use a nested error message to aggregate the exceptions produced by each failure.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.mergeFailures : {α : Type} → Array (Lean.Elab.Term.TermElabResult Lean.Expr) → Lean.Elab.TermElabM α
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instSup : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : SemilatticeSup β] →
        [inst_2 : Zero β] →
          [inst_3 : TopologicalSpace β] → [ContinuousSup β] → Max (CompactlySupportedContinuousMap α β)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [self : HomologicalComplex.HasHomotopyCofiber φ]
  (i j : ι), c.Rel i j → CategoryTheory.Limits.HasBinaryBiproduct (F.X j) (G.X i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The unit associated to a representative of `2 • P` for a projective point representative `P` on
a Weierstrass curve `W` that is `2`-torsion.

More specifically, the unit `u` such that `W.add P P = u • ![0, 1, 0]` where `P = W.neg P`.  -/
WeierstrassCurve.Projective.dblU : {F : Type u} → [Field F] → WeierstrassCurve.Projective F → (Fin 3 → F) → F
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
dirichletSummandHom.eq_1 : ∀ {s : ℂ} {n : ℕ} (χ : DirichletCharacter ℂ n) (hs : s ≠ 0),
  dirichletSummandHom χ hs = { toFun := fun n_1 => χ ↑n_1 * ↑n_1 ^ (-s), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Lie.Ideal
LieHom.mem_ker : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'} {x : L}, x ∈ f.ker ↔ f x = 0
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.coe_symm_of_notMem : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {b : B},
  b ∉ e.baseSet → e.symm b = fun x => Classical.arbitrary (E b)
-- Mathlib.Logic.Equiv.Defs
Equiv.sigmaCongrLeft_apply : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ ≃ α₂) (a : (a : α₁) × β (e a)),
  e.sigmaCongrLeft a = ⟨e a.fst, a.snd⟩
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_eq_getD_back?_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.maxKeyD fallback = t.keysArray.back?.getD fallback
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe_adj : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (a a_1 : V), G'.spanningCoe.Adj a a_1 = G'.Adj a a_1
-- Init.Data.Option.Monadic
Option.mapM_join : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Applicative m] [LawfulApplicative m] {f : α → m β}
  {o : Option (Option α)}, Option.mapM f o.join = Option.join <$> Option.mapM (Option.mapM f) o
-- Mathlib.Algebra.Lie.Basis.Base
LieAlgebra.Basis.coe_baseSupportEquiv_apply : ∀ {ι : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Fintype ι] [inst_1 : Field K] [inst_2 : CharZero K]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  (b : LieAlgebra.Basis ι H) [inst_6 : LieModule.IsTriangularizable K (↥H) L] [inst_7 : LieAlgebra.IsKilling K L]
  (i : ι), LieModule.Weight.toLinear K (↥H) L ↑↑(b.baseSupportEquiv i) = b.baseSupp i
-- Mathlib.Probability.Density
MeasureTheory.HasPDF.congr : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {X Y : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E},
  X =ᵐ[ℙ] Y → ∀ [hX : MeasureTheory.HasPDF X ℙ μ], MeasureTheory.HasPDF Y ℙ μ
-- Mathlib.Topology.Sets.BaseChangeNhds
TopologicalSpace.Compacts.instInitialElemOpensOpenRcNhdsOpenNhdsFunctorOfT2SpaceOfLocallyCompactSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : TopologicalSpace.Compacts α} [T2Space α] [LocallyCompactSpace α],
  ⋯.functor.Initial
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv_apply : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B)
  (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U)
  [inst_3 : CategoryTheory.Limits.HasReflexiveCoequalizers A]
  (h : (X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)) (Y : A) (X : B)
  (a : CategoryTheory.LiftLeftAdjoint.constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
  (CategoryTheory.LiftLeftAdjoint.constructLeftAdjointEquiv R F' adj₁ adj₂ h Y X) a =
    (CategoryTheory.Limits.Cofork.IsColimit.homIso (CategoryTheory.LiftLeftAdjoint.counitCoequalises adj₁ h X)
          (R.obj Y)).symm
      ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
          ((adj₂.homEquiv (U.obj X) Y)
            ↑((CategoryTheory.Limits.Cofork.IsColimit.homIso
                  (CategoryTheory.Limits.colimit.isColimit
                    (CategoryTheory.Limits.parallelPair (F'.map (U.map (adj₁.counit.app X)))
                      (CategoryTheory.LiftLeftAdjoint.otherMap R F' adj₁ adj₂ X)))
                  Y)
                a)),
        ⋯⟩
-- Init.Data.Float.Model.Float
Float.Model.instAdd : Add Float.Model
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.incenter_ne_point : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.incenter ≠ s.points i
-- Mathlib.Algebra.Homology.Augment
_private.Mathlib.Algebra.Homology.Augment.0.CochainComplex.augment.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (i j : ℕ) (h_1 : Unit → motive 0 1) (h_2 : (i j : ℕ) → motive i.succ j.succ)
  (h_3 : (x x_1 : ℕ) → motive x x_1),
  (match i.succ, j.succ with
    | 0, 1 => h_1 ()
    | i.succ, j.succ => h_2 i j
    | x, x_1 => h_3 x x_1) =
    h_2 i j
-- Mathlib.Probability.Kernel.Disintegration.Density
MeasurableSpace.countablePartition.congr_simp : ∀ (α : Type u_3) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (a a_1 : ℕ),
  a = a_1 →
    ∀ (a_2 a_3 : Set α),
      a_2 = a_3 → MeasurableSpace.countablePartition α a a_2 = MeasurableSpace.countablePartition α a_1 a_3
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrumRestricts_iff_spectrumRestricts_inr : ∀ (S : Type u_3) {R : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Algebra R S] [inst_4 : Module R A] [inst_5 : Module S A] [inst_6 : IsScalarTower S A A]
  [inst_7 : SMulCommClass S A A] [inst_8 : IsScalarTower R S A] {a : A} {f : S → R},
  QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f
-- Std.Sync.Broadcast
/-- Counter for assigning unique IDs to new receivers.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.nextId : {α : Type} → Std.Bounded.State✝ α → ℕ
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.LiftRelAux.match_1.eq_4 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ Computation α → β ⊕ Computation β → Sort u_3) (ca : Computation α)
  (cb : Computation β) (h_1 : (a : α) → (b : β) → motive (Sum.inl a) (Sum.inl b))
  (h_2 : (a : α) → (cb : Computation β) → motive (Sum.inl a) (Sum.inr cb))
  (h_3 : (ca : Computation α) → (b : β) → motive (Sum.inr ca) (Sum.inl b))
  (h_4 : (ca : Computation α) → (cb : Computation β) → motive (Sum.inr ca) (Sum.inr cb)),
  (match Sum.inr ca, Sum.inr cb with
    | Sum.inl a, Sum.inl b => h_1 a b
    | Sum.inl a, Sum.inr cb => h_2 a cb
    | Sum.inr ca, Sum.inl b => h_3 ca b
    | Sum.inr ca, Sum.inr cb => h_4 ca cb) =
    h_4 ca cb
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A B : C}
  {X Y : CategoryTheory.Subobject B} (f : A ⟶ B), (X ⊓ Y).Factors f ↔ X.Factors f ∧ Y.Factors f
-- Mathlib.Computability.Encoding
Computability.encodePosNum.eq_def : ∀ (x : PosNum),
  Computability.encodePosNum x =
    match x with
    | PosNum.one => [true]
    | n.bit0 => false :: Computability.encodePosNum n
    | n.bit1 => true :: Computability.encodePosNum n
-- Mathlib.Topology.Sheaves.Skyscraper
instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [CategoryTheory.Limits.HasColimits C], (skyscraperPresheafFunctor p₀).IsRightAdjoint
-- Mathlib.MeasureTheory.Measure.AEMeasurable
MeasurableEmbedding.aemeasurable_map_iff : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {f : α → β} {μ : MeasureTheory.Measure α} {g : β → γ},
  MeasurableEmbedding f → (AEMeasurable g (MeasureTheory.Measure.map f μ) ↔ AEMeasurable (g ∘ f) μ)
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor.mk.inj : ∀ {c : Lean.Meta.Grind.SplitInfo} {numCases : ℕ} {isRec : Bool} {e : Lean.Expr} {anchor : UInt64}
  {c_1 : Lean.Meta.Grind.SplitInfo} {numCases_1 : ℕ} {isRec_1 : Bool} {e_1 : Lean.Expr} {anchor_1 : UInt64},
  { c := c, numCases := numCases, isRec := isRec, e := e, anchor := anchor } =
      { c := c_1, numCases := numCases_1, isRec := isRec_1, e := e_1, anchor := anchor_1 } →
    c = c_1 ∧ numCases = numCases_1 ∧ isRec = isRec_1 ∧ e = e_1 ∧ anchor = anchor_1
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
instSubsingletonUniformFun : ∀ {α : Type u_1} {β : Type u_2} [Subsingleton β], Subsingleton (UniformFun α β)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find?_eq_dite : ∀ {n : ℕ} {p : Fin n → Bool},
  Fin.find? p = if h : ∃ i, p i = true then some (Fin.find (fun x => p x = true) h) else none
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The projection to the base of a wide pullback cone.  -/
CategoryTheory.Limits.WidePullbackCone.base : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : C} → {Y : ι → C} → {f : (i : ι) → Y i ⟶ X} → (s : CategoryTheory.Limits.WidePullbackCone f) → s.pt ⟶ X