mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaComparison_map_desc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasCoproduct f] [inst_3 : CategoryTheory.Limits.HasCoproduct fun b => G.obj (f b)]
  (P : C) (g : (j : β) → f j ⟶ P),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaComparison G f)
      (G.map (CategoryTheory.Limits.Sigma.desc g)) =
    CategoryTheory.Limits.Sigma.desc fun j => G.map (g j)
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiffAt.clm_prodMap : ∀ {𝕜 : 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] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {F₄ : Type u_11}
  [inst_12 : NormedAddCommGroup F₄] [inst_13 : NormedSpace 𝕜 F₄] {n : WithTop ℕ∞} {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₄} {x : M},
  ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ →L[𝕜] F₃)) n g x →
    ContMDiffAt I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₄)) n f x →
      ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ × F₂ →L[𝕜] F₃ × F₄)) n (fun x => (g x).prodMap (f x)) x
-- Mathlib.Algebra.Group.Basic
eq_div_iff_mul_eq' : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a = b / c ↔ a * c = b
-- Init.Data.Iterators.Lemmas.Basic
/-- Induction principle for productive iterators: One can define a function `f` that maps every
iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on
the plausible skip successors of `it'.
 -/
Std.Iter.inductSkips : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    [Std.Iterators.Productive α Id] →
      (motive : Std.Iter β → Sort x) →
        ((it : Std.Iter β) →
            ({it' : Std.Iter β} → it.IsPlausibleStep (Std.IterStep.skip it') → motive it') → motive it) →
          (it : Std.Iter β) → motive it
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.avgRisk_zero_prior : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧) (κ : ProbabilityTheory.Kernel 𝓧 𝓨),
  ProbabilityTheory.avgRisk ℓ P κ 0 = 0
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.whiskerRight_def : ∀ (R : Type u) [inst : CommRing R] {X₁ X₂ : CoalgCat R} (f : X₁ ⟶ X₂) (X : CoalgCat R),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f X =
    CoalgCat.ofHom (CoalgHom.rTensor (↑X.toModuleCat) f.toCoalgHom')
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.VariableMap.findHyps.slotHyps : Aesop.VariableMap → Aesop.Slot → Aesop.Substitution → Aesop.PremiseIndex → Aesop.BaseM (Lean.PHashSet Aesop.Hyp)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
measurable_limit_of_tendsto_metrizable_ae : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β] {ι : Type u_3} [Nonempty ι]
  {μ : MeasureTheory.Measure α} {f : ι → α → β} {L : Filter ι} [L.IsCountablyGenerated],
  (∀ (n : ι), AEMeasurable (f n) μ) →
    (∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) L (nhds l)) →
      ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) L (nhds (f_lim x))
-- Mathlib.RingTheory.MvPolynomial
MvPolynomial.finrank_eq_zero : ∀ {σ : Type u} {K : Type v} [inst : CommRing K] [Nontrivial K] [Nonempty σ], Module.finrank K (MvPolynomial σ K) = 0
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point.  -/
ContDiffWithinAt.prodMap' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {E' : Type u_3} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {F' : Type u_4}
  [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace 𝕜 F'] {s : Set E} {t : Set E'} {f : E → F} {g : E' → F'}
  {p : E × E'},
  ContDiffWithinAt 𝕜 n f s p.1 → ContDiffWithinAt 𝕜 n g t p.2 → ContDiffWithinAt 𝕜 n (Prod.map f g) (s ×ˢ t) p
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- If `e : S₁ ≅ S₂` is an isomorphism of short complexes and `h₁ : HomologyData S₁`,
this is the homology data for `S₂` deduced from the isomorphism.  -/
CategoryTheory.ShortComplex.HomologyData.ofIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} → (S₁ ≅ S₂) → S₁.HomologyData → S₂.HomologyData
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- The graph with no edges on a given vertex type `V`.  -/
SimpleGraph.emptyGraph : (V : Type u) → SimpleGraph V
-- Mathlib.CategoryTheory.EqToHom
/-- `eqToHom'` is the dual of `eqToHom`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.eqToHom' : {C : Type u₁} → [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] → {X Y : C} → X = Y → (Y ⟶ X)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
/-- The power series expansion of `Real.arctan`, valid on `-1 < x < 1`.  -/
Real.hasSum_arctan : ∀ {x : ℝ}, ‖x‖ < 1 → HasSum (fun n => (-1) ^ n * x ^ (2 * n + 1) / ↑(2 * n + 1)) (Real.arctan x)
-- Lean.Elab.PreDefinition.WF.Preprocess
Lean.Elab.WF.preprocess : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DHashMap.Const.ofList l).getKey? k = none
-- Init.Data.NeZero
instNeZeroNatIte : ∀ {p : Prop} [inst : Decidable p] {n m : ℕ} [NeZero n] [NeZero m], NeZero (if p then n else m)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.containsThenInsert_fst : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.containsThenInsert k v).1 = t.contains k
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.IsPushout.IsVanKampen.flip : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  {H : CategoryTheory.IsPushout f g h i}, H.IsVanKampen → ⋯.IsVanKampen
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (n : ℕ),
  Int.Internal.Linear.cooper_dvd_left_cert p₁ p₂ p₃ d n = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 →
        d ∣ Int.Internal.Linear.Poly.denote' ctx p₃ →
          Int.Internal.Linear.OrOver n (Int.Internal.Linear.cooper_dvd_left_split ctx p₁ p₂ p₃ d)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.integrable_iff_integrableAtFilter_atBot : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε]
  [inst_5 : LinearOrder X] [OrderTop X] [CompactIccSpace X],
  MeasureTheory.Integrable f μ ↔ MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.LocallyIntegrable f μ
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.ext_iff : ∀ {α : Type u_1} {x y : GenContFract α}, x = y ↔ x.h = y.h ∧ x.s = y.s
-- Mathlib.RingTheory.WittVector.WittPolynomial
xInTermsOfW_zero : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible ↑p], xInTermsOfW p R 0 = MvPolynomial.X 0
-- Mathlib.Data.Real.ConjExponents
NNReal.holderTriple_coe_iff : ∀ {p q r : NNReal}, (↑p).HolderTriple ↑q ↑r ↔ p.HolderTriple q r
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The functor `P.Comma L R₁ Q W ⥤ P.Comma L R₃ Q W` induced by the composition of the natural
transformations `r : R₁ ⟶ R₂` and `r' : R₂ ⟶ R₃` is naturally isomorphic to the composition of the
functors induced by these natural transformations.  -/
CategoryTheory.MorphismProperty.Comma.mapRightComp : {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} →
                          [Q.RespectsIso] →
                            [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))) →
                                        CategoryTheory.MorphismProperty.Comma.mapRight L
                                            (CategoryTheory.CategoryStruct.comp r r') hrr' ≅
                                          (CategoryTheory.MorphismProperty.Comma.mapRight L r hr).comp
                                            (CategoryTheory.MorphismProperty.Comma.mapRight L r' hr')
-- Mathlib.Data.Finset.Max
/-- Induction principle for `Finset`s in any type from which a given function `f` maps to a linearly
ordered type : a predicate is true on all `s : Finset α` provided that:

* it is true on the empty `Finset`,
* for every `s : Finset α` and an element `a` such that for elements of `s` denoted by `x` we have
  `f a ≤ f x`, `p s` implies `p (insert a s)`.  -/
Finset.induction_on_min_value : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : DecidableEq ι] (f : ι → α) {motive : Finset ι → Prop}
  (s : Finset ι),
  motive ∅ → (∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f a ≤ f x) → motive s → motive (insert a s)) → motive s
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {g : γ → β}
  (f : β → α) {s : Set γ}, Set.InjOn g s → ∏' (x : ↑(g '' s)), f ↑x = ∏' (x : ↑s), f (g ↑x)
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
LinearMap.BilinForm.tensorDistribEquiv_toLinearMap : ∀ (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Module.Free R M₁]
  [inst_6 : Module.Finite R M₁] [inst_7 : Module.Free R M₂] [inst_8 : Module.Finite R M₂],
  ↑(LinearMap.BilinForm.tensorDistribEquiv R) = LinearMap.BilinForm.tensorDistrib R R
-- Mathlib.Algebra.Order.Module.HahnEmbedding
LinearPMap.sup.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f f_1 : E →ₛₗ.[σ] F)
  (e_f : f = f_1) (g g_1 : E →ₛₗ.[σ] F) (e_g : g = g_1) (h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y),
  f.sup g h = f_1.sup g_1 ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_alter_le_size : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α] {k : α} {f : Option β → Option β},
  m.WF → (Std.DHashMap.Raw.Const.alter m k f).size ≤ m.size + 1
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.card_of_cycleType_mul_eq : ∀ (α : Type u_1) [inst : DecidableEq α] [inst_1 : Fintype α] (m : Multiset ℕ),
  {g | g.cycleType = m}.card *
      ((Fintype.card α - m.sum).factorial * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m).factorial) =
    if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α).factorial else 0
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substAlgHom_comp_substAlgHom : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] {υ : Type u_5} {T : Type u_6}
  [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] {a : PowerSeries S}
  {b : MvPowerSeries υ T} [inst_6 : IsScalarTower R S T] (ha : PowerSeries.HasSubst a) (hb : PowerSeries.HasSubst b),
  (AlgHom.restrictScalars R (PowerSeries.substAlgHom hb)).comp (PowerSeries.substAlgHom ha) = PowerSeries.substAlgHom ⋯
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Overlaps.map : Lean.Meta.Match.Overlaps → Std.HashMap ℕ (Std.TreeSet ℕ compare)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.single.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : DecidableEq X] [inst_2 : Zero Y] (x : X) (y : Y),
  Function.locallyFinsuppWithin.single x y =
    { toFun := Pi.single x y, supportWithinDomain' := ⋯, supportLocallyFiniteWithinDomain' := ⋯ }
-- Mathlib.RingTheory.Coprime.Lemmas
instDecidableRelIntIsCoprime : DecidableRel IsCoprime
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr},
  Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq c = Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq c_1 → c = c_1
-- Mathlib.CategoryTheory.Abelian.Exact
/-- If `(f, g)` is exact, then `factorThruImage g` is a cokernel of `f`.  -/
CategoryTheory.ShortComplex.Exact.isColimitImage : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S : CategoryTheory.ShortComplex C} →
        S.Exact →
          CategoryTheory.Limits.IsColimit
            (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.factorThruImage S.g) ⋯)
-- Mathlib.Data.Sign.Defs
/-- The sign of an element is 1 if it's positive, -1 if negative, 0 otherwise.  -/
SignType.sign : {α : Type u_1} → [Zero α] → [inst : Preorder α] → [DecidableLT α] → α →o SignType
-- Mathlib.RingTheory.Valuation.Discrete.RankOne
Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt_restrict_apply_of_surjective : ∀ {R : Type u_2} [inst : Ring R] {v : Valuation R (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete],
  Function.Surjective ⇑v →
    ∀ (x : R), (Valuation.IsRankOneDiscrete.valueGroup₀_equiv_withZeroMulInt v) (v.restrict x) = v x
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.orthogonal_mem_invtSubmodule : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E} {U : Submodule 𝕜 E},
  U ∈ Module.End.invtSubmodule ↑(ContinuousLinearMap.adjoint T) → Uᗮ ∈ Module.End.invtSubmodule ↑T
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.infinite_add : ∀ {α : Type u_2} [inst : Add α] [IsLeftCancelAdd α] [IsRightCancelAdd α] {s t : Set α},
  (s + t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty
-- Mathlib.Data.ULift
ULift.map_bijective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Bijective (ULift.map f) ↔ Function.Bijective f
-- Std.Data.Internal.List.Associative
Std.Internal.List.forIn_eq_forIn_toProd : ∀ {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {l : List ((_ : α) × β)} {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  (forIn l init fun a d => f a.fst a.snd d) = forIn (List.map (fun x => (x.fst, x.snd)) l) init fun a d => f a.1 a.2 d
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_congr : ∀ {R : Type u_1} [inst : CommSemiring R] {a a' b b' c : R}, a = a' → b = b' → a' + b' = c → a + b = c
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.IsInitial.isPrincipal_opow : ∀ {o : Ordinal.{u_1}}, o.IsInitial → Ordinal.omega0 ≤ o → Ordinal.IsPrincipal (fun x1 x2 => x1 ^ x2) o
-- Mathlib.CategoryTheory.Sites.Descent.IsPrestack
CategoryTheory.Pseudofunctor.IsPrestack.isSheaf : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  (J : CategoryTheory.GrothendieckTopology C) [self : F.IsPrestack J] {S : C} (M N : ↑(F.obj { as := Opposite.op S })),
  CategoryTheory.Presheaf.IsSheaf (J.over S) (F.presheafHom M N)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
/-- `prefixFunction pat i …` is the maximum `k` such that `pat[0...k] = pat[stackPos - k + 1...=stackPos]`.

Using the implementation given here, computing a table of `prefixFunction pat i` for `i` in
`0...pat.size` would take cubic time, but we will later show that the `buildTable` function, which
runs in linear time, also computes this table.
 -/
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction : (pat : ByteArray) → (stackPos : ℕ) → stackPos < pat.size → ℕ
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instInv : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Inv Y] → Inv (LocallyConstant X Y)
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.backward.linearNoConfusionType : Lean.Option Bool
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.instInhabitedSemanticTokensState.default : Lean.Server.FileWorker.SemanticTokensState
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.lie_h_f : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H) (i j : ι),
  ⁅self.h j, self.f i⁆ = -self.A i j • self.f i
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
/-- The natural functor from comonoid objects in the category of `R`-modules to `R`-coalgebras.  -/
CoalgCat.ofComon : (R : Type u) → [inst : CommRing R] → CategoryTheory.Functor (CategoryTheory.Comon (ModuleCat R)) (CoalgCat R)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
tangentMapWithin_comp_at : ∀ {𝕜 : 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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {s : Set M} {g : M' → M''} {u : Set M'} (p : TangentBundle I M),
  MDiffAt[u] g (f p.proj) →
    MDiffAt[s] f p.proj →
      s ⊆ f ⁻¹' u →
        UniqueMDiffAt[s] p.proj →
          tangentMapWithin I I'' (g ∘ f) s p = tangentMapWithin I' I'' g u (tangentMapWithin I I' f s p)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesMap_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K L : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i], HomologicalComplex.opcyclesMap 0 i = 0
-- Lean.Meta.Basic
/-- `isClass? type` return `some ClsName` if `type` is an instance of the class `ClsName`.
Example:
```
#eval do
  let x ← mkAppM ``Inhabited #[mkConst ``Nat]
  IO.println (← isClass? x)
  -- (some Inhabited)
```
 -/
Lean.Meta.isClass? : Lean.Expr → Lean.MetaM (Option Lean.Name)
-- Mathlib.Algebra.Lie.Normalizer
/-- The normalizer of a Lie submodule.

See also `LieSubmodule.idealizer`.  -/
LieSubmodule.normalizer : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [LieModule R L M] → LieSubmodule R L M → LieSubmodule R L M
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.CommRingCat.Colimits.descFunLift.match_1.eq_2 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (motive : CommRingCat.Colimits.Prequotient F → Sort u_2)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (CommRingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive CommRingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive CommRingCat.Colimits.Prequotient.one)
  (h_4 : (x : CommRingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : CommRingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match CommRingCat.Colimits.Prequotient.zero with
    | CommRingCat.Colimits.Prequotient.of j x => h_1 j x
    | CommRingCat.Colimits.Prequotient.zero => h_2 ()
    | CommRingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_2 ()
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.nat_rawCast_1 : ∀ {R : Type u_1} [inst : CommSemiring R], Nat.rawCast 1 = 1
-- Mathlib.Order.Filter.Pi
/-- Coproduct of filters.  -/
Filter.coprodᵢ : {ι : Type u_1} → {α : ι → Type u_2} → ((i : ι) → Filter (α i)) → Filter ((i : ι) → α i)
-- Mathlib.LinearAlgebra.LinearDisjoint
Submodule.LinearDisjoint.mk : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  Function.Injective ⇑(M.mulMap N) → M.LinearDisjoint N
-- Mathlib.Topology.Order.SuccPred
SuccOrder.nhds_bot : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α]
  [inst_5 : OrderBot α], nhds ⊥ = pure ⊥
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.tendsto_measure_sigmaFiniteSetGE : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [inst : MeasureTheory.IsFiniteMeasure ν],
  Filter.Tendsto (fun n => ν (μ.sigmaFiniteSetGE ν n)) Filter.atTop
    (nhds (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : MeasureTheory.SigmaFinite (μ.restrict s)), ν s))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.ctorAlt.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (info : Lean.Compiler.LCNF.CtorInfo) (code : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_3)
  (info_1 : Lean.Compiler.LCNF.CtorInfo) (code_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_3),
  (Lean.Compiler.LCNF.Alt.ctorAlt info code h = Lean.Compiler.LCNF.Alt.ctorAlt info_1 code_1 h_1) =
    (info = info_1 ∧ code = code_1)