mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.lift_φ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {A : C} (a : A ⟶ S.L₁.X₂) (b : A ⟶ S.L₀.X₃)
  (h : CategoryTheory.CategoryStruct.comp a S.L₁.g = CategoryTheory.CategoryStruct.comp b S.v₀₁.τ₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift a b h) S.φ₂ =
    CategoryTheory.CategoryStruct.comp a S.v₁₂.τ₂
-- Mathlib.Data.List.TakeDrop
_private.Mathlib.Data.List.TakeDrop.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashSet.Raw.ofList l).get? k' = some k
-- Mathlib.Data.Set.Image
Function.LeftInverse.mem_preimage_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α},
  Function.LeftInverse g f → ∀ {s : Set α} {x : α}, f x ∈ g ⁻¹' s ↔ x ∈ s
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.forall_iff : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (P : CategoryTheory.Over X → Prop),
  (∀ (Y : CategoryTheory.Over X), P Y) ↔ ∀ (Y : T) (f : Y ⟶ X), P (CategoryTheory.Over.mk f)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings.  -/
two_mul_le_add_sq : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddLeftReflectLE R] [AddLeftMono R] (a b : R), 2 * a * b ≤ a ^ 2 + b ^ 2
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (u : ℤˣ) (w : HNNExtension.NormalWord d), HNNExtension.t ^ ↑u • w = HNNExtension.NormalWord.unitsSMul φ u w
-- Mathlib.Data.Finset.Fold
Finset.lt_fold_max : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [inst : LinearOrder β] (c : β),
  c < Finset.fold max b f s ↔ c < b ∨ ∃ x ∈ s, c < f x
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.inl_pushoutZeroZeroIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl 0 0)
      (CategoryTheory.Limits.pushoutZeroZeroIso X Y).hom =
    CategoryTheory.Limits.coprod.inl
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_functor_obj_obj_map : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (X_1 : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A)
  {X_2 Y : (TopologicalSpace.Opens ↥U)ᵒᵖ} (f : X_2 ⟶ Y),
  (U.sheafEquivOver.functor.obj X_1).obj.map f = X_1.obj.map (U.overEquivalence.inverse.map f.unop).op
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.Extension.tensorH1CotangentOfFormallyEtale.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  {P : Algebra.Extension R S} {Q : Algebra.Extension R T} (f : P.Hom Q) [alg : Algebra P.Ring Q.Ring]
  (halg : algebraMap P.Ring Q.Ring = f.toRingHom) [inst_7 : Module.Flat S T] (H₁ : f.toRingHom.FormallyEtale)
  (H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))),
  Algebra.Extension.tensorH1CotangentOfFormallyEtale f halg H₁ H₂ =
    LinearEquiv.ofBijective (LinearMap.liftBaseChange T (Algebra.Extension.H1Cotangent.map f)) ⋯
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.finish_isReduced : ∀ (u : PNat.XgcdType), u.finish.IsReduced
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.surjective_fst_prod : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂), Function.Surjective ⇑((LieHom.fst R L₁ L₂).comp (LieAlgebra.Basis.prod✝ eι b₁ b₂).incl)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.even_add_odd : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M] {f : ℕ → M},
  (Summable fun k => f (2 * k)) → (Summable fun k => f (2 * k + 1)) → Summable f
-- Mathlib.CategoryTheory.Yoneda
/-- The representing object for the corepresentable functor `F`.  -/
CategoryTheory.Functor.coreprX : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (F : CategoryTheory.Functor C (Type v)) → [hF : F.IsCorepresentable] → C
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, t.isEmpty = true → t.getKey! a = default
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mk : {𝕜 : Type u_7} →
  {α : Type u_8} →
    [inst : Zero 𝕜] →
      [inst_1 : LE α] → (toFun : α → α → 𝕜) → (∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0) → IncidenceAlgebra 𝕜 α
-- Mathlib.Analysis.Complex.Basic
RCLike.ofReal_tsum : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} (f : α → ℝ),
  ↑(∑'[L] (a : α), f a) = ∑'[L] (a : α), ↑(f a)
-- Mathlib.Tactic.FunProp.FunctionData
/-- Decomposes `fun x ↦ f y₁ ... yₙ` into `(fun g ↦ g yₙ) ∘ (fun x y ↦ f y₁ ... yₙ₋₁ y)`

Returns `DecompositionResult.failed` if:
- `n=0`
- `yₙ` contains `x`
- `n=1` and `(fun x y ↦ f y)` is identity function i.e. `x=f`  -/
Mathlib.Meta.FunProp.FunctionData.peeloffArgDecomposition : Mathlib.Meta.FunProp.FunctionData → Lean.MetaM Mathlib.Meta.FunProp.DecompositionResult
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_smul : ∀ (p : ENNReal) {K : Type u_1} {V : Type u_4} [inst : SMul K V] (c : K) (x : V),
  WithLp.toLp p (c • x) = c • WithLp.toLp p x
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- Given an affinely independent family of points, an affine combination lies in the
span of two points given as affine combinations if and only if it is an affine combination
with weights those of one point plus a multiple of the difference between the weights of the
two points.  -/
affineCombination_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} {p : ι → P},
  AffineIndependent k p →
    ∀ {w w₁ w₂ : ι → k} {s : Finset ι},
      ∑ i ∈ s, w i = 1 →
        ∑ i ∈ s, w₁ i = 1 →
          ∑ i ∈ s, w₂ i = 1 →
            ((Finset.affineCombination k s p) w ∈
                line[k, (Finset.affineCombination k s p) w₁, (Finset.affineCombination k s p) w₂] ↔
              ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i)
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- **Double counting** argument.

Considering `r` as a bipartite graph, the LHS is a lower bound on the number of edges while the RHS
is a strict upper bound.  -/
Finset.card_nsmul_lt_card_nsmul_of_le_of_lt : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R]
  (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : R} [inst_3 : (a : α) → (b : β) → Decidable (r a b)],
  t.Nonempty →
    (∀ a ∈ s, m ≤ ↑(Finset.bipartiteAbove r t a).card) →
      (∀ b ∈ t, ↑(Finset.bipartiteBelow r s b).card < n) → s.card • m < t.card • n
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationData.name : ProofWidgets.ExprPresentationData → Lean.Name
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.inter : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s₁ s' : Set (Set Ω)} (s₂ : Set (Set Ω)),
  ProbabilityTheory.CondIndepSets m' hm' s₁ s' μ → ProbabilityTheory.CondIndepSets m' hm' (s₁ ∩ s₂) s' μ
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.hsymmPart_indiscrete : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] (n : ℕ),
  MvPolynomial.hsymmPart σ R (Nat.Partition.indiscrete n) = MvPolynomial.hsymm σ R n
-- Mathlib.MeasureTheory.Group.AEStabilizer
AddAction.aestabilizer_congr : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.VAddInvariantMeasure G α μ] {s t : Set α},
  s =ᵐ[μ] t → AddAction.aestabilizer G μ s = AddAction.aestabilizer G μ t
-- Std.Async.Select
/-- Performs fair and data-loss free multiplexing on the `Selectable`s in `selectables`.

The protocol for this is as follows:
1. The `selectables` are shuffled randomly.
2. Run `Selector.tryFn` for each element in `selectables`. If any succeed, the corresponding
  `Selectable.cont` is executed and its result is returned immediately.
3. If none succeed, a `Waiter` is registered with each `Selector` using `Selector.registerFn`.
   Once one of them resolves the `Waiter`, all `Selector.unregisterFn` functions are called, and
   the `Selectable.cont` of the winning `Selector` is executed and returned.
 -/
Std.Async.Selectable.one : {α : Type} → Array (Std.Async.Selectable α) → Std.Async.Async α
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCancelMonoid α],
  Colex.instAddCancelMonoid = { toAddLeftCancelMonoid := Colex.instAddLeftCancelMonoid, toIsRightCancelAdd := ⋯ }
-- Mathlib.RingTheory.Trace.Basic
Module.Basis.traceDual_def : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] [inst_5 : Finite ι] [inst_6 : DecidableEq ι]
  (b : Module.Basis ι K L), b.traceDual = (Algebra.traceForm K L).dualBasis ⋯ b
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.functor_obj_map : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) {X Y : J} (f : X ⟶ Y),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).obj S).map f =
    S.mapNatTrans ((CategoryTheory.evaluation J C).map f)
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Append two compositions to get a composition of the sum of numbers.  -/
Composition.append : {n m : ℕ} → Composition m → Composition n → Composition (m + n)
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomId.mk : ∀ {R : Type u_4} [inst : Semiring R] {σ : R →+* R}, σ = RingHom.id R → RingHomId σ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termG₂ : Lean.ParserDescr
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCocone_map_to_top : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i : J) (hi : i < j),
  (CategoryTheory.SmallObject.SuccStruct.ofCocone c).map (CategoryTheory.homOfLE ⋯) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c i hi).hom
      (CategoryTheory.CategoryStruct.comp (c.ι.app ⟨i, hi⟩)
        (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIsoPt c).inv)
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- Components of the counit of the adjunction `Cat.objects ⊣ Codiscrete.functorToCat`  -/
CategoryTheory.Codiscrete.counitApp : (A : Type u) → CategoryTheory.Codiscrete A → A
-- Mathlib.Topology.Algebra.Ring.Basic
/-- A topological semiring is a semiring `R` where addition and multiplication are continuous.
We allow for non-unital and non-associative semirings as well.

The `IsTopologicalSemiring` class should *only* be instantiated in the presence of a
`NonUnitalNonAssocSemiring` instance; if there is an instance of `NonUnitalNonAssocRing`,
then `IsTopologicalRing` should be used. Note: in the presence of `NonAssocRing`, these classes are
mathematically equivalent (see `IsTopologicalSemiring.continuousNeg_of_mul` or
`IsTopologicalSemiring.toIsTopologicalRing`).  -/
IsTopologicalSemiring : (R : Type u_1) → [TopologicalSpace R] → [NonUnitalNonAssocSemiring R] → Prop
-- Lean.Environment
/-- Register a height override for a definition so that `getMaxHeight` uses it.  -/
Lean.setDefHeightOverride : Lean.Environment → Lean.Name → UInt32 → Lean.Environment
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.ι_mapBifunctorMapObjDesc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K) {X : CategoryTheory.GradedObject I C₁} {Y : CategoryTheory.GradedObject J C₂} {A : C₃} {k : K}
  [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
  (f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)) (i : I) (j : J) (hij : p (i, j) = k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X Y i j k hij)
      (CategoryTheory.GradedObject.mapBifunctorMapObjDesc f) =
    f i j hij
-- Init.Data.Array.Basic
/-- Auxiliary for `ofFn`. `ofFn.go f acc i h = acc ++ #[f (n - i), ..., f(n - 1)]`  -/
_private.Init.Data.Array.Basic.0.Array.ofFn.go : {α : Type u} → {n : ℕ} → (Fin n → α) → Array α → (i : ℕ) → i ≤ n → Array α
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst.injEq : ∀ (x : Int.Internal.Linear.Var) (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (x_1 : Int.Internal.Linear.Var)
  (c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.subst x_1 c₁_1 c₂_1) =
    (x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_eq_singleton_iff : ∀ {k m n : ℤ}, (m...=n).toArray = #[k] ↔ n = m ∧ m = k
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Eta-expanded form of `contDiffOn_id` -/
contDiffOn_fun_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {s : Set E}, ContDiffOn 𝕜 n (fun x => x) s
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- Composition of matrices using matrix multiplication.  -/
CategoryTheory.Mat_.Hom.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Preadditive C] → {M N K : CategoryTheory.Mat_ C} → M.Hom N → N.Hom K → M.Hom K
-- Init.Data.Array.Lemmas
Array.pop_push : ∀ {α : Type u_1} {xs : Array α} {x : α}, (xs.push x).pop = xs
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixedField.smul : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] → (K : IntermediateField F E) → SMul ↥K ↥(IntermediateField.fixedField K.fixingSubgroup)
-- Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
CategoryTheory.Presheaf.isLocallyInjective_of_whisker : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4}
  {CA : A → Type u_5} [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_4 : CategoryTheory.ConcreteCategory A FA],
  CategoryTheory.CoverPreserving J K H →
    ∀ [H.IsCoverDense K] [CategoryTheory.Presheaf.IsLocallyInjective J (H.op.whiskerLeft f)],
      CategoryTheory.Presheaf.IsLocallyInjective K f
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap'_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.ShortComplex.opcyclesMap' 0 h₁ h₂ = 0
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pattern.BackwardSliceSearcher.endsWith_iff : ∀ {pat s : String.Slice}, String.Slice.Pattern.BackwardSliceSearcher.endsWith pat s = true ↔ ∃ t, s.copy = t ++ pat.copy
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.functor_obj_obj : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) (j : J),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.functor J C).obj S).obj j =
    S.map ((CategoryTheory.evaluation J C).obj j)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.instIsAffineHomToNormalization : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] [AlgebraicGeometry.IsAffineHom f],
  AlgebraicGeometry.IsAffineHom (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_iff_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax a → (b < Order.succ a ↔ b ≤ a)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) {c : R}, c ≠ 0 → (Polynomial.C c * Polynomial.X ^ n).support = {n}
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureHelpContext.fromJson : Lean.Json → Except String Lean.Lsp.SignatureHelpContext
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Ring homomorphisms preserve additive inverse.  -/
RingHom.map_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocRing α] [inst_1 : NonAssocRing β] (f : α →+* β) (x : α), f (-x) = -f x
-- Mathlib.Tactic.SetNotationForOrder
/-- Superset relation: `a ⊇ b`.
For types tagged with `@[use_set_notation_for_order]`,
the relation `GE.ge` is used instead of `Superset`.
The hover info shows which one is used. 

Conventions for notations in identifiers:

 * The recommended spelling of `⊇` in identifiers is `superset`. -/
Mathlib.Meta.SetNotationForOrder.supsetStx' : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Hom.Monoid
/-- An `OrderMonoidHom` is a monotone function.  -/
OrderMonoidHom.monotone' : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] (self : α →*o β), Monotone (↑self.toMonoidHom).toFun
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopic.trans : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] ⦃f g h : C(X, Y)⦄,
  f.Homotopic g → g.Homotopic h → f.Homotopic h
-- Mathlib.Topology.MetricSpace.DilationEquiv
instDilationClassOfDilationEquivClass : ∀ (F : Type u_1) (X : outParam (Type u_2)) (Y : outParam (Type u_3)) [inst : PseudoEMetricSpace X]
  [inst_1 : PseudoEMetricSpace Y] [inst_2 : EquivLike F X Y] [DilationEquivClass F X Y], DilationClass F X Y
-- Mathlib.Data.Sum.Interval
Sum.Ioc_inr_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (a₂ : α) (b₁ : β), Finset.Ioc (Sum.inr b₁) (Sum.inl a₂) = ∅
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.NonnegCoeffs.brecOn : ∀ {motive : (a : Lean.Grind.CommRing.Poly) → a.NonnegCoeffs → Prop} {a : Lean.Grind.CommRing.Poly} (t : a.NonnegCoeffs),
  (∀ (a : Lean.Grind.CommRing.Poly) (t : a.NonnegCoeffs), Lean.Grind.CommRing.Poly.NonnegCoeffs.below t → motive a t) →
    motive a t
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trStmts₁.match_1.eq_4 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (p : Turing.PartrecToTM2.Γ' → Bool) (k : Turing.PartrecToTM2.K')
  (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.move p k₁ k₂ q → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.K') →
        (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.push k s q → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 :
    (Q : Turing.PartrecToTM2.Λ') →
      (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') →
        Q = Turing.PartrecToTM2.Λ'.read q → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.clear p k q → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.copy → motive q.copy)
  (h_6 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.succ → motive q.succ)
  (h_7 : (Q q₁ q₂ : Turing.PartrecToTM2.Λ') → Q = q₁.pred q₂ → motive (q₁.pred q₂))
  (h_8 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.Cont') → Q = Turing.PartrecToTM2.Λ'.ret k → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match Turing.PartrecToTM2.Λ'.clear p k q with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => h_1 Q p k₁ k₂ q h
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => h_2 Q k s q h
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => h_3 Q q h
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => h_4 Q p k q h
    | Q@h:q.copy => h_5 Q q h
    | Q@h:q.succ => h_6 Q q h
    | Q@h:(q₁.pred q₂) => h_7 Q q₁ q₂ h
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => h_8 Q k h) =
    h_4 (Turing.PartrecToTM2.Λ'.clear p k q) p k q ⋯
-- Mathlib.Topology.Algebra.Valued.NormedValued
NormedField.valuation_apply : ∀ {K : Type u_1} [hK : NormedField K] [inst : IsUltrametricDist K] (x : K), NormedField.valuation x = ‖x‖₊
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.ext_iff : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G}
  {x y : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ}, x = y ↔ x.app = y.app
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.setIntegral_tilted_mul_eq_mgf' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : Ω → E) {s : Set Ω},
  MeasurableSet s →
    (∫ (x : Ω) in s, g x ∂μ.tilted fun x => t * X x) =
      ∫ (x : Ω) in s, (Real.exp (t * X x) / ProbabilityTheory.mgf X μ t) • g x ∂μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightKind.text.sizeOf_spec : sizeOf Lean.Lsp.DocumentHighlightKind.text = 1