mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instDivOfContinuousDiv : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [inst_2 : Div β] → [ContinuousDiv β] → Div C(α, β)
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.of_lt_left : ∀ {α : Type u_1} {a b a' : α} [inst : LinearOrder α], a < b → a = a' → ¬b ≤ a'
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintTextEdit.mk.injEq : ∀ (range : Lean.Syntax.Range) (newText : String) (range_1 : Lean.Syntax.Range) (newText_1 : String),
  ({ range := range, newText := newText } = { range := range_1, newText := newText_1 }) =
    (range = range_1 ∧ newText = newText_1)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_nonpos : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalSemiring R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A]
  [inst_18 : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  (∀ x ∈ quasispectrum R a, f x ≤ 0) → cfcₙ f a ≤ 0
-- Mathlib.RingTheory.KrullDimension.Regular
ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {x : R},
  IsSMulRegular R x → x ∈ Ring.jacobson R → ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denoteAsIntModule.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denoteAsIntModule ctx p =
    match p with
    | Lean.Grind.CommRing.Poly.num k => k • One.one
    | Lean.Grind.CommRing.Poly.add k m p =>
      k • Lean.Grind.CommRing.Mon.denoteAsIntModule ctx m + Lean.Grind.CommRing.Poly.denoteAsIntModule ctx p
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.mem_of_mem_roc : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {lo hi a : α}, (a ∈ lo<...=hi) → a ∈ *...=hi
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normIntModInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X Y : C), CategoryTheory.Abelian.Ext.mk₀ 0 = 0
-- Mathlib.Data.Multiset.Filter
Multiset.filter_cons_of_neg : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} (s : Multiset α),
  ¬p a → Multiset.filter p (a ::ₘ s) = Multiset.filter p s
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isNormal_omega : Order.IsNormal ⇑Ordinal.omega
-- Mathlib.Analysis.Analytic.Order
/-- Analytic order of a composition of analytic functions.  -/
AnalyticAt.analyticOrderAt_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {g : 𝕜 → 𝕜} {z₀ : 𝕜},
  AnalyticAt 𝕜 f (g z₀) →
    AnalyticAt 𝕜 g z₀ → analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x => g x - g z₀) z₀
-- Mathlib.RingTheory.Localization.Module
LinearMap.restrictScalars_extendScalarsOfIsLocalization : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (f : M →ₗ[R] N),
  ↑R (LinearMap.extendScalarsOfIsLocalization S A f) = f
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S') ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂) (q' : Y ⟶ S)
  (f₁' : Y ⟶ X (α j₁)) (f₂' : Y ⟶ X (α j₂))
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_3)
  (hq' :
    autoParam (CategoryTheory.CategoryStruct.comp q p = q')
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_5)
  (hf₁' :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (p' j₁) = f₁')
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_7)
  (hf₂' :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (p' j₂) = f₂')
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_9)
  {Z : ↑(F.obj { as := Opposite.op Y })}
  (h : (F.map f₂.op.toLoc).toFunctor.obj ((F.map (p' j₂).op.toLoc).toFunctor.obj (D.obj (α j₂))) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯) h =
    CategoryTheory.CategoryStruct.comp
      ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc f₁'.op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)))
      (CategoryTheory.CategoryStruct.comp (D.hom q' f₁' f₂' ⋯ ⋯)
        (CategoryTheory.CategoryStruct.comp
          ((F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc f₂'.op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))) h))
-- Mathlib.Algebra.Polynomial.Div
Polynomial.degree_add_divByMonic : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R},
  q.Monic → q.degree ≤ p.degree → q.degree + (p /ₘ q).degree = p.degree
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_natCast_lt_lift : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.aleph ↑n < Cardinal.lift.{v, u} c ↔ Cardinal.aleph ↑n < c
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.canonical_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.RightHomologyData.canonical S).ι = S.homologyι
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.map_surjective_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  Function.Surjective (Polynomial.map f) ↔ Function.Surjective ⇑f
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearEquiv_ofLinearEquiv : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (l : A₁ ≃ₗ[R] A₂) (map_one : l 1 = 1)
  (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y), ↑(AlgEquiv.ofLinearEquiv l map_one map_mul) = l
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.sigma_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I)
  {c : CategoryTheory.Limits.Cofan I.left} (hc : CategoryTheory.Limits.IsColimit c)
  {d : CategoryTheory.Limits.Cofan I.right} (hd : CategoryTheory.Limits.IsColimit d),
  CategoryTheory.CategoryStruct.comp (I.fstSigmaMapOfIsColimit d hc)
      (CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π) =
    CategoryTheory.CategoryStruct.comp (I.sndSigmaMapOfIsColimit d hc)
      (CategoryTheory.Limits.Cofan.IsColimit.desc hd K.π)
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer.0.CategoryTheory.Limits.WalkingMultispan.instFinCategoryOfLOfDecidableEqR.match_4.splitter : {J : CategoryTheory.Limits.MultispanShape} →
  (motive :
      (b : J.R) →
        (a : J.L) →
          (CategoryTheory.Limits.WalkingMultispan.left a ⟶ CategoryTheory.Limits.WalkingMultispan.right b) →
            J.fst a = b → J.snd a = b → Sort u_3) →
    (b : J.R) →
      (a : J.L) →
        (x : CategoryTheory.Limits.WalkingMultispan.left a ⟶ CategoryTheory.Limits.WalkingMultispan.right b) →
          (h₁ : J.fst a = b) →
            (h₂ : J.snd a = b) →
              ((a : J.L) →
                  (h₁ : J.fst a = J.fst a) →
                    (h₂ : J.snd a = J.fst a) →
                      motive (J.fst a) a (CategoryTheory.Limits.WalkingMultispan.Hom.fst a) h₁ h₂) →
                ((a : J.L) →
                    (h₁ : J.fst a = J.snd a) →
                      (h₂ : J.snd a = J.snd a) →
                        motive (J.snd a) a (CategoryTheory.Limits.WalkingMultispan.Hom.snd a) h₁ h₂) →
                  motive b a x h₁ h₂
-- Mathlib.Data.Fintype.BigOperators
Fintype.card_eq_sum_ones : ∀ {α : Type u_4} [inst : Fintype α], Fintype.card α = ∑ _a, 1
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.unit_naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X Y : C} (f : X ⟶ Y) {Z : C}
  (h : G.obj (F.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj.unit.app X) (CategoryTheory.CategoryStruct.comp (G.map (F.map f)) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (adj.unit.app Y) h)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.mono_of_epi_of_epi_mono' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 2} (φ : R₁ ⟶ R₂),
  R₁.map' 0 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2
        CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1 =
      0 →
    CategoryTheory.Epi
        (R₁.map' 1 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6
          CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
      R₂.Exact →
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2) →
          CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
            CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1)
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.lt_sizeUpTo_index_succ : ∀ {n : ℕ} (c : Composition n) (j : Fin n), ↑j < c.sizeUpTo ↑(c.index j).succ
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.zipWithMAux.eq_def : ∀ {α : Type u} {β : Type u_1} {γ : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (bs : Array β)
  (f : α → β → m γ) (i : ℕ) (cs : Array γ),
  as.zipWithMAux bs f i cs =
    if h : i < as.size then
      have a := as[i];
      if h : i < bs.size then
        have b := bs[i];
        do
        let __do_lift ← f a b
        as.zipWithMAux bs f (i + 1) (cs.push __do_lift)
      else pure cs
    else pure cs
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isBigOWith_abs_left`. -/
Asymptotics.IsBigOWith.abs_left : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {c : ℝ} {g : α → F} {l : Filter α} {u : α → ℝ},
  Asymptotics.IsBigOWith c l u g → Asymptotics.IsBigOWith c l (fun x => |u x|) g
-- Lean.DocString.Extension
/-- The location of the snippet in the source file.
 -/
Lean.VersoModuleDocs.Snippet.declarationRange : Lean.VersoModuleDocs.Snippet → Lean.DeclarationRange
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- The forgetful functor from categories to quivers.  -/
CategoryTheory.ReflQuiv.forget : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.ReflQuiv
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace.eq_1 : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K),
  NumberField.mixedEmbedding.normAtPlace w =
    { toFun := fun x => if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖, map_zero' := ⋯, map_one' := ⋯,
      map_mul' := ⋯ }
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.coe_set_neg : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Submodule R M),
  ↑(-S) = -↑S
-- Mathlib.SetTheory.ZFC.Class
instInsertZFSetClass : Insert ZFSet.{u_1} Class.{u_1}
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_getModify_EStateM_apply_eq : ∀ {σ ε : Type} {post : σ → σ → Prop} {epost : ε → σ → Prop} (f : σ → σ),
  Std.Internal.Do.wp (getModify f) post epost = Std.Internal.Do.wp (MonadStateOf.modifyGet fun s => (s, f s)) post epost
-- Lean.MetavarContext
/-- Return true iff `e` depends on a free variable `x` s.t. `pf x`, or an unassigned metavariable `?m` s.t. `pm ?m` is true.  -/
Lean.dependsOnPred : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadMCtx m] →
      Lean.Expr →
        (optParam (Lean.FVarId → Bool) fun x => false) → (optParam (Lean.MVarId → Bool) fun x => false) → m Bool
-- Mathlib.Algebra.Group.End
Equiv.Perm.extendDomain_eq_one_iff : ∀ {α : Type u_4} {β : Type u_5} {p : β → Prop} [inst : DecidablePred p] {e : Equiv.Perm α} {f : α ≃ Subtype p},
  e.extendDomain f = 1 ↔ e = 1
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- Given a sieve `S` on `X : C`, a presheaf `P : Cᵒᵖ ⥤ A`, and an object `E` of `A`,
the cones over the natural diagram `S.arrows.diagram.op ⋙ P` associated to `S` and `P`
with cone point `E` are in 1-1 correspondence with `SieveCompatible` family of elements
for the sieve `S` and the presheaf of types `Hom (E, P -)`.  -/
CategoryTheory.Presheaf.conesEquivSieveCompatibleFamily : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        (P : CategoryTheory.Functor Cᵒᵖ A) →
          {X : C} →
            (S : CategoryTheory.Sieve X) →
              (E : Aᵒᵖ) → (S.arrows.diagram.op.comp P).cones.obj E ≃ { x // x.SieveCompatible }
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.finite_right : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} [H.FiniteIndex], Subgroup.IsComplement (↑H) T → T.Finite
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_subtype_lt_map_subtype : ∀ {G : Type u_1} [inst : Group G] {G' : Subgroup G} {H K : Subgroup ↥G'},
  Subgroup.map G'.subtype H < Subgroup.map G'.subtype K ↔ H < K
-- Mathlib.Algebra.Group.Prod
AddHom.snd_comp_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : M →ₙ+ N)
  (g : M →ₙ+ P), (AddHom.snd N P).comp (f.prod g) = g
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is uniformly equicontinuous on a set `S`, the same is true for its
closure in *any* topology for which evaluation at any `x ∈ S` i continuous. Since this will be
applied to `DFunLike` types, we state it for any topological space with a map to `β → α` satisfying
the right continuity conditions. See also `Set.UniformEquicontinuousOn.closure` for a more familiar
(but weaker) statement.  -/
UniformEquicontinuousOn.closure' : ∀ {Y : Type u_5} {α : Type u_6} {β : Type u_8} [tY : TopologicalSpace Y] [uα : UniformSpace α] [uβ : UniformSpace β]
  {A : Set Y} {u : Y → β → α} {S : Set β},
  UniformEquicontinuousOn (u ∘ Subtype.val) S →
    Continuous (S.domRestrict ∘ u) → UniformEquicontinuousOn (u ∘ Subtype.val) S
-- Mathlib.FieldTheory.Laurent
RatFunc.laurentAux_algebraMap : ∀ {R : Type u} [inst : CommRing R] (r : R) (p : Polynomial R) [inst_1 : IsDomain R],
  (RatFunc.laurentAux r) ((algebraMap (Polynomial R) (RatFunc R)) p) =
    (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          (preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)) →
            autoParam (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f)
                CategoryTheory.Functor.FullyFaithful.map_preimage._autoParam →
              autoParam (∀ {X Y : C} (f : X ⟶ Y), preimage (F.map f) = f)
                  CategoryTheory.Functor.FullyFaithful.preimage_map._autoParam →
                F.FullyFaithful
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.instDistribMulActionSubtypeMemAddSubgroupOfStarModule : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Star R] →
      [TrivialStar R] →
        [inst_2 : AddCommGroup A] →
          [inst_3 : StarAddMonoid A] →
            [inst_4 : Monoid R] →
              [inst_5 : DistribMulAction R A] → [StarModule R A] → DistribMulAction R ↥(skewAdjoint A)
-- Lean.Meta.Basic
/-- Given `e` of the form `fun ..xs => A`, execute `k xs A`.
This combinator will declare local declarations, create free variables for them,
execute `k` with updated local context, and make sure the cache is restored after executing `k`.

If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
 -/
Lean.Meta.lambdaTelescope : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] → {α : Type} → Lean.Expr → (Array Lean.Expr → Lean.Expr → n α) → optParam Bool false → n α
-- Init.Data.String.Lemmas.TakeDrop
String.take_toSlice : ∀ {s : String} {n : ℕ}, s.toSlice.take n = s.take n
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) {Z : C} (h : S₂.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap φ) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp h₂.homologyIso.inv h)
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasPullbacks C}
  {x y : CategoryTheory.Pretopology C}, x = y ↔ x.coverings = y.coverings
-- Mathlib.Order.Antisymmetrization
liftFun_antisymmRel : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β),
  Relator.LiftFun ⇑(AntisymmRel.setoid α fun x1 x2 => x1 ≤ x2) ⇑(AntisymmRel.setoid β fun x1 x2 => x1 ≤ x2) ⇑f ⇑f
-- Mathlib.Geometry.Euclidean.Angle.Bisector
/-- A point `p` is equidistant to two affine subspaces (typically lines, for this version of the
lemma) if twice the oriented angles at a point `p'` in their intersection between `p` and its
orthogonal projections onto the subspaces are equal.  -/
EuclideanGeometry.dist_orthogonalProjection_eq_of_two_zsmul_oangle_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [inst_4 : Fact (Module.finrank ℝ V = 2)] [inst_5 : Module.Oriented ℝ V (Fin 2)]
  {p p' : P} {s₁ s₂ : AffineSubspace ℝ P} (hp'₁ : p' ∈ s₁) (hp'₂ : p' ∈ s₂),
  ↑((EuclideanGeometry.orthogonalProjection s₁) p) ≠ p' →
    ↑((EuclideanGeometry.orthogonalProjection s₂) p) ≠ p' →
      2 • EuclideanGeometry.oangle (↑((EuclideanGeometry.orthogonalProjection s₁) p)) p' p =
          2 • EuclideanGeometry.oangle p p' ↑((EuclideanGeometry.orthogonalProjection s₂) p) →
        dist p ↑((EuclideanGeometry.orthogonalProjection s₁) p) =
          dist p ↑((EuclideanGeometry.orthogonalProjection s₂) p)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.mk.injEq : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (left : X.left ⟶ Y.left) (right : X.right ⟶ Y.right)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map left) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map right))
      CategoryTheory.CommaMorphism.w._autoParam)
  (left_1 : X.left ⟶ Y.left) (right_1 : X.right ⟶ Y.right)
  (w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map left_1) Y.hom =
        CategoryTheory.CategoryStruct.comp X.hom (R.map right_1))
      CategoryTheory.CommaMorphism.w._autoParam),
  ({ left := left, right := right, w := w } = { left := left_1, right := right_1, w := w_1 }) =
    (left = left_1 ∧ right = right_1)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.apply_skipPrefixWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {h : s.skipPrefixWhile P ≠ s.endPos},
  ¬P ((s.skipPrefixWhile P).get h)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.diam_range : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F), Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
-- Mathlib.Topology.Homotopy.Path
/-- Given `Homotopy p₀ p₁` and `Homotopy p₁ p₂`, we can define a `Homotopy p₀ p₂` by putting the first
homotopy on `[0, 1/2]` and the second on `[1/2, 1]`.
 -/
Path.Homotopy.trans : {X : Type u} →
  [inst : TopologicalSpace X] → {x₀ x₁ : X} → {p₀ p₁ p₂ : Path x₀ x₁} → p₀.Homotopy p₁ → p₁.Homotopy p₂ → p₀.Homotopy p₂
-- Mathlib.Order.Hom.Basic
OrderHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : βᵒᵈ →o γᵒᵈ) (f : αᵒᵈ →o βᵒᵈ), OrderHom.dual.symm (g.comp f) = (OrderHom.dual.symm g).comp (OrderHom.dual.symm f)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context : Type
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassP_add_coe : ∀ (L : PeriodPair) (z : ℂ) (l : ↥L.lattice), L.derivWeierstrassP (z + ↑l) = L.derivWeierstrassP z
-- Lean.Data.Lsp.Utf16
_private.Lean.Data.Lsp.Utf16.0.Lean.String.csize16 : Char → ℕ
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Equivalence.mapCommMon_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] (e : C ≌ D)
  [inst_6 : e.functor.Braided] [inst_7 : e.inverse.Braided] [inst_8 : e.IsMonoidal],
  e.mapCommMon.functor = e.functor.mapCommMon
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeListTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List ℕ → List α → Array (List α) → Sort u_2) (xs : List α) (acc : Array (List α))
  (h_1 : (xs : List α) → (acc : Array (List α)) → motive [] xs acc)
  (h_2 : (n : ℕ) → (ns : List ℕ) → (xs : List α) → (acc : Array (List α)) → motive (n :: ns) xs acc),
  (match [], xs, acc with
    | [], xs, acc => h_1 xs acc
    | n :: ns, xs, acc => h_2 n ns xs acc) =
    h_1 xs acc
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.braiding_inv_apply : ∀ {X Y : Type u} {x : X} {y : Y}, (CategoryTheory.ConcreteCategory.hom (β_ X Y).inv) (y, x) = (x, y)