mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0to1.tr.match_1.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} (motive : Option (Λ × Turing.TM0.Stmt Γ) → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (q' : Λ) → (s : Turing.TM0.Stmt Γ) → motive (some (q', s))),
  (match none with
    | none => h_1 ()
    | some (q', s) => h_2 q' s) =
    h_1 ()
-- Mathlib.Topology.Maps.Proper.Basic
IsHomeomorph.isProperMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → IsProperMap f
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.invFun_as_coe : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.invFun = ↑e.symm
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.trW_op_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] {X Y : Cᵒᵖ} {f : X ⟶ Y}, P.op.trW f ↔ P.trW f.unop
-- Mathlib.RingTheory.Ideal.Quotient.Index
Ideal.finite_quotient_prod : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_3} (I : ι → Ideal R) (s : Finset ι),
  (∀ i ∈ s, (I i).FG) → (∀ i ∈ s, Finite (R ⧸ I i)) → Finite (R ⧸ ∏ i ∈ s, I i)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.toArray : {α : Type u_1} → {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → Array (α × β)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuation_surjective : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), Function.Surjective ⇑A.valuation
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.match_4.congr_eq_6 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_3 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a b : Lean.Grind.CommRing.Expr),
  x = a.mul b →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.intCast k => h_2 k
      | Lean.Grind.CommRing.Expr.natCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_6 a b
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.ω.eq_1 : ∀ {q : ℕ}, LucasLehmer.X.ω = (2, 1)
-- Lean.DocString.Extension
Lean.getDocStringText : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Lean.TSyntax `Lean.Parser.Command.docComment → m String
-- Lean.Meta.RecExt
/-- Environment extension for storing which declarations are recursive.
This information is populated by the `PreDefinition` module, but the simplifier
uses when unfolding declarations.
 -/
Lean.Meta.recExt : Lean.TagDeclarationExtension
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.nSwap : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.Data.Set.Sups
Set.iUnion_image_inf_left : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t : Set α), ⋃ a ∈ s, (fun x => a ⊓ x) '' t = s ⊼ t
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.of_pow : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {c c' : ℝ} {l : Filter α} [NormOneClass S] {n : ℕ} {f : α → S} {g : α → R},
  Asymptotics.IsBigOWith c l (f ^ n) (g ^ n) → n ≠ 0 → c ≤ c' ^ n → 0 ≤ c' → Asymptotics.IsBigOWith c' l f g
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- A (multiplicative) Lie group is a group and a `C^n` manifold at the same time in which
the multiplication and inverse operations are `C^n`.  -/
LieGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                WithTop ℕ∞ → (G : Type u_4) → [Group G] → [inst : TopologicalSpace G] → [ChartedSpace H G] → Prop
-- Mathlib.Data.Finset.Max
/-- Let `s` be a finset in a linear order. Then `s.min` is the minimum of `s` if `s` is not empty,
and `⊤` otherwise. It belongs to `WithTop α`. If you want to get an element of `α`, see
`s.min'`.  -/
Finset.min : {α : Type u_2} → [LinearOrder α] → Finset α → WithTop α
-- Mathlib.Topology.Path
/-- See Note [continuity lemma statement].  -/
Continuous.pathExtend : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {γ : Y → Path x y}
  {f : Y → ℝ}, Continuous ↿γ → Continuous f → Continuous fun t => (γ t).extend (f t)
-- Mathlib.Order.Minimal
Maximal.not_prop_of_gt : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : Preorder α], Maximal P x → x < y → ¬P y
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.instQuasiIsoExtendMap : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K L : HomologicalComplex C c) (φ : K ⟶ L) (e : c.Embedding c')
  [inst_3 : ∀ (j : ι), K.HasHomology j] [inst_4 : ∀ (j : ι), L.HasHomology j] [QuasiIso φ],
  QuasiIso (HomologicalComplex.extendMap φ e)
-- Mathlib.Topology.MetricSpace.Algebra
instLipschitzMulOrderDual : ∀ (α : Type u_1) [inst : PseudoMetricSpace α] [inst_1 : Monoid α] [LipschitzMul α], LipschitzMul αᵒᵈ
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.isMaximal : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (p : T.CompleteType α), FirstOrder.Language.Theory.IsMaximal ↑p
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The multiplication on the localized module.
Note that this gives a diamond with the instance on `R[S⁻¹]` (which does not require commutativity),
but is defeq to it under `with_reducible_and_instances`.
See https://github.com/leanprover-community/mathlib4/pull/25671 for an approach to generalize this
but it requires right `R` actions on `R`-algebras.
 -/
LocalizedModule.mul : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type u_3} →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] → {S : Submonoid R} → LocalizedModule S A → LocalizedModule S A → LocalizedModule S A
-- Mathlib.RingTheory.WittVector.Truncated
_private.Mathlib.RingTheory.WittVector.Truncated.0.term𝕎 : Lean.ParserDescr
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The weighted sum is unaffected by changing the weights to the
corresponding indicator function and adding points to the set.  -/
Finset.weightedVSubOfPoint_indicator_subset : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (w : ι → k) (p : ι → P) (b : P) {s₁ s₂ : Finset ι},
  s₁ ⊆ s₂ → (s₁.weightedVSubOfPoint p b) w = (s₂.weightedVSubOfPoint p b) ((↑s₁).indicator w)
-- Mathlib.Order.Filter.CardinalInter
Filter.EventuallyEq.cardinal_bInter : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι},
  Cardinal.mk ↑S < c →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) → ⋂ i, ⋂ (h : i ∈ S), s i h =ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β},
  (m.modify k f).getKey? k' = if (k == k') = true then if k ∈ m then some k else none else m.getKey? k'
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightComp_hom_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ R₃ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r : R₁ ⟶ R₂) (r' : R₂ ⟶ R₃)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (hr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r'.app X.right)))
  (hrr' :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom ((CategoryTheory.CategoryStruct.comp r r').app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightComp L r r' hr hr' hrr').hom.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Topology.ContinuousMap.Basic
Homeomorph.continuousMapCongr_symm_apply : ∀ {X₁ : Type u_5} {X₂ : Type u_6} {Y₁ : Type u_7} {Y₂ : Type u_8} [inst : TopologicalSpace X₁]
  [inst_1 : TopologicalSpace X₂] [inst_2 : TopologicalSpace Y₁] [inst_3 : TopologicalSpace Y₂] (e : X₁ ≃ₜ X₂)
  (e' : Y₁ ≃ₜ Y₂) (g : C(X₂, Y₂)),
  (e.continuousMapCongr e').symm g =
    { toFun := ⇑e'.symm, continuous_toFun := ⋯ }.comp (g.comp { toFun := ⇑e, continuous_toFun := ⋯ })
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_natCast_nonneg : ∀ (n : ℕ), 0 ≤ Real.log ↑n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.aux_iteratedDeriv_tsum_cotTerm : ∀ {z : ℂ} {k : ℕ},
  1 ≤ k →
    z ∈ UpperHalfPlane.upperHalfPlaneSet →
      (-1) ^ k * ↑k.factorial * z ^ (-1 - ↑k) +
          iteratedDerivWithin k (fun z => ∑' (n : ℕ), cotTerm z n) UpperHalfPlane.upperHalfPlaneSet z =
        (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)
-- Lean.Parser.Term
Lean.Parser.Term.let_delayed.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.mem_restrictScalars : ∀ (R : Type u) {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A]
  {U : Subalgebra S A} {x : A}, x ∈ Subalgebra.restrictScalars R U ↔ x ∈ U
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- The multiplicative closure is greater than or equal to the original property.  -/
CategoryTheory.MorphismProperty.le_multiplicativeClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W ≤ W.multiplicativeClosure
-- Init.Data.Nat.Basic
Nat.exists_eq_add_one_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → ∃ k, n = k + 1
-- Mathlib.LinearAlgebra.Span.Basic
LinearEquiv.toSpanNonzeroSingleton_apply : ∀ (R : Type u_1) (M : Type u_4) [inst : Ring R] [inst_1 : IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.IsTorsionFree R M] (x : M) (h : x ≠ 0) (t : R),
  (LinearEquiv.toSpanNonzeroSingleton R M x h) t = ⟨t • x, ⋯⟩
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
_private.Mathlib.RingTheory.Coalgebra.CoassocSimps.0.CoassocSimps.termβ : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.lTensor_smul : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (a : A) (f : σ.IntertwiningMap τ),
  Representation.IntertwiningMap.lTensor ρ (a • f) = a • Representation.IntertwiningMap.lTensor ρ f
-- Mathlib.CategoryTheory.Galois.EssSurj
/-- For every open subgroup `V` of `Aut F`, there exists an `X : C` such that
`F.obj X ≅ Aut F ⧸ V` as `Aut F`-sets.  -/
CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroup : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (V : OpenSubgroup (CategoryTheory.Aut F)),
  ∃ X,
    Nonempty
      ((CategoryTheory.PreGaloisCategory.functorToAction F).obj X ≅
        Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑V)))
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.toNNReal_rpow : ∀ (x : ENNReal) (z : ℝ), (x ^ z).toNNReal = x.toNNReal ^ z
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The adjunction `Γ ⊣ Spec` from `CommRingᵒᵖ` to `Scheme`.  -/
AlgebraicGeometry.ΓSpec.adjunction : AlgebraicGeometry.Scheme.Γ.rightOp ⊣ AlgebraicGeometry.Scheme.Spec
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableOn.mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M},
  MDiff[s] f → s ∈ nhds x → MDiffAt f x
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.w_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.WeightedCone W F)
  {i j : J} (x : W.obj i) (f : i ⟶ j) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (c.π x) (CategoryTheory.CategoryStruct.comp (F.map f) h) =
    CategoryTheory.CategoryStruct.comp (c.π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x)) h
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_not_contains_map_fst_of_contains_map_fst_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)}
  {hl₁ : Std.Internal.List.DistinctKeys l₁} {k : α},
  Std.Internal.List.containsKey k l₂ = true →
    Std.Internal.List.containsKey k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = false
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.instBEqSparseCasesOnKey : BEq Lean.Meta.SparseCasesOnKey✝
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
NonnegSpectrumClass.nonneg_of_mem_quasispectrum : ∀ {A : Type u_2} [inst : NonUnitalRing A] {𝕜 : Type u_3} [inst_1 : CommSemiring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : PartialOrder A] [inst_4 : Module 𝕜 A] [NonnegSpectrumClass 𝕜 A] {a : A},
  0 ≤ a → ∀ {x : 𝕜}, x ∈ quasispectrum 𝕜 a → 0 ≤ x
-- Mathlib.Logic.Function.Defs
Function.snd_comp_diag : ∀ {α : Type u_1}, Prod.snd ∘ Function.diag = id
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.Equivalence.toOrderIso_symm_apply : ∀ {X : Type u} {Y : Type v} [inst : PartialOrder X] [inst_1 : PartialOrder Y] (e : X ≌ Y) (y : Y),
  e.toOrderIso.symm y = e.inverse.obj y
-- Mathlib.Order.GaloisConnection.Basic
/-- `sSup` and `Iic` form a Galois connection.  -/
gc_sSup_Iic : ∀ {α : Type u} [inst : CompleteSemilatticeSup α], GaloisConnection sSup Set.Iic
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- Shows that the recurrence relation (`convs`) and direct evaluation (`convs'`) of a
(regular) continued fraction coincide.  -/
ContFract.convs_eq_convs' : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {c : ContFract K},
  (↑↑c).convs = (↑↑c).convs'
-- Mathlib.CategoryTheory.Join.Sum
CategoryTheory.Join.fromSum_obj : ∀ (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] (x : C ⊕ D),
  (CategoryTheory.Join.fromSum C D).obj x =
    match x with
    | Sum.inl X => CategoryTheory.Join.left X
    | Sum.inr X => CategoryTheory.Join.right X
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.HomotopyCategory.homToNerveMk_app_zero : ∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C]
  (F : CategoryTheory.Functor X.HomotopyCategory C)
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })),
  (CategoryTheory.ConcreteCategory.hom
        ((SSet.Truncated.HomotopyCategory.homToNerveMk F).app
          (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })))
      x =
    CategoryTheory.nerveEquiv.symm (F.obj (SSet.Truncated.HomotopyCategory.mk x))
-- Mathlib.AlgebraicGeometry.EllipticCurve.LFunction
/-- The L-series of a Weierstrass curve over a number field.  -/
WeierstrassCurve.LSeries : {K : Type u_1} → [inst : Field K] → [NumberField K] → WeierstrassCurve K → ℂ → ℂ
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.color.congr_simp : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p p_1 : Besicovitch.TauPackage β α),
  p = p_1 → ∀ (a a_1 : Ordinal.{u}), a = a_1 → p.color a = p_1.color a_1
-- Mathlib.Algebra.Group.Units.Equiv
/-- Extra simp lemma that `dsimp` can use. `simp` will never use this.  -/
Equiv.mulRight_symm_apply : ∀ {G : Type u_5} [inst : Group G] (a : G), ⇑(Equiv.symm (Equiv.mulRight a)) = fun x => x * a⁻¹
-- Mathlib.Order.Sublattice
Sublattice.pi_empty : ∀ {κ : Type u_5} {π : κ → Type u_6} [inst : (i : κ) → Lattice (π i)] (L : (i : κ) → Sublattice (π i)),
  Sublattice.pi ∅ L = ⊤
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.mul_mem : ∀ {M : Type u_1} [inst : Mul M] (I : SemigroupIdeal M) (x : M) {y : M}, y ∈ I → x * y ∈ I
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.BalanceLPrecond.erase : ∀ {left right : ℕ},
  Std.DTreeMap.Internal.Impl.BalanceLPrecond left right → Std.DTreeMap.Internal.Impl.BalanceLErasePrecond left right
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- Analogue of `congr_arg f h`,
when `h : x = x'` is an equality between elements of objects in a concrete category.
 -/
CategoryTheory.congr_arg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y) {x x' : CategoryTheory.ToType X},
  x = x' → (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom f) x'
-- Mathlib.RingTheory.SimpleModule.Basic
jacobson_density : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  (f : Module.End (Module.End R M) M) (s : Finset M), ∃ r, ∀ m ∈ s, f m = r • m
-- Init.Data.Vector.Lemmas
Vector.toArray_range : ∀ {n : ℕ}, (Vector.range n).toArray = Array.range n
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.foldlM.loop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (i' : ℕ) → motive i'.succ),
  (match 0 with
    | 0 => h_1 ()
    | i'.succ => h_2 i') =
    h_1 ()
-- Mathlib.Algebra.Algebra.Operations
Submodule.bot_pow : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] {n : ℕ}, n ≠ 0 → ⊥ ^ n = ⊥
-- Lean.Meta.Tactic.Grind.Types
/-- Injectivity theorem.  -/
Lean.Meta.Grind.SplitSource.inj : Lean.Meta.Grind.Origin → Lean.Meta.Grind.SplitSource
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {m : Std.HashSet.Raw α}, m.isEmpty = (m.size == 0)
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.posterior.eq_1 : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (κ : ProbabilityTheory.Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω)
  [inst_2 : MeasureTheory.IsFiniteMeasure μ] [inst_3 : ProbabilityTheory.IsFiniteKernel κ],
  ProbabilityTheory.posterior κ μ = (MeasureTheory.Measure.map Prod.swap (μ.compProd κ)).condKernel
-- Mathlib.RingTheory.Polynomial.Subring
Polynomial.toSubring.congr_simp : ∀ {R : Type u_1} [inst : Ring R] (p p_1 : Polynomial R) (e_p : p = p_1) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑T),
  p.toSubring T hp = p_1.toSubring T ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.extract.inj : ∀ {w start len : ℕ} {expr : Std.Tactic.BVDecide.BVExpr w} {w_1 start_1 : ℕ} {expr_1 : Std.Tactic.BVDecide.BVExpr w_1},
  Std.Tactic.BVDecide.BVExpr.extract start len expr = Std.Tactic.BVDecide.BVExpr.extract start_1 len expr_1 →
    w = w_1 ∧ start = start_1 ∧ expr ≍ expr_1
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Given a pointwise right Kan extension of `F` along `L`, exhibits
`(RightExtension.whiskerRight L F G).obj E` as a pointwise right Kan extension of `F ⋙ G` at `L`.  -/
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.postcompose : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  {F : CategoryTheory.Functor A B} →
                    {L : CategoryTheory.Functor A C} →
                      [G.PreservesPointwiseRightKanExtension F L] →
                        {E : L.RightExtension F} →
                          E.IsPointwiseRightKanExtension →
                            ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj
                                E).IsPointwiseRightKanExtension
-- Mathlib.MeasureTheory.Group.Defs
/-- A measure `μ` on a measurable group is right invariant
if the measure of right translations of a set are equal to the measure of the set itself.  -/
MeasureTheory.Measure.IsMulRightInvariant : {G : Type u_1} → [inst : MeasurableSpace G] → [Mul G] → MeasureTheory.Measure G → Prop
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPStructureInstances : Lean.Options → Bool
-- Mathlib.Data.List.Duplicate
_private.Mathlib.Data.List.Duplicate.0.List.«term_∈+_» : Lean.TrailingParserDescr
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.take.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → Stream'.Seq α → Sort u_2) (n : ℕ) (s : Stream'.Seq α)
  (h_1 : (x : Stream'.Seq α) → motive 0 x) (h_2 : (n : ℕ) → (s : Stream'.Seq α) → motive n.succ s),
  (match n.succ, s with
    | 0, x => h_1 x
    | n.succ, s => h_2 n s) =
    h_2 n s
-- Init.Data.Array.Basic
/-- Returns the first element of the array for which the monadic predicate `p` returns `true`, or `none`
if no such element is found. Elements of the array are checked in order.

The monad `m` is restricted to `Type → Type` to avoid needing to use `ULift Bool` in `p`'s type.

Example:
```lean example
#eval #[7, 6, 5, 8, 1, 2, 6].findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false
```
```output
Almost! 6
Almost! 5
```
```output
some 1
```
 -/
Array.findM? : {m : Type → Type u_1} → {α : Type} → [Monad m] → (α → m Bool) → Array α → m (Option α)