mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.LocalContext
Lean.LocalContext.mk.inj : ∀ {fvarIdToDecl : Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl}
  {decls : Lean.PersistentArray (Option Lean.LocalDecl)} {auxDeclToFullName : Lean.FVarIdMap Lean.Name}
  {fvarIdToDecl_1 : Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl}
  {decls_1 : Lean.PersistentArray (Option Lean.LocalDecl)} {auxDeclToFullName_1 : Lean.FVarIdMap Lean.Name},
  { fvarIdToDecl := fvarIdToDecl, decls := decls, auxDeclToFullName := auxDeclToFullName } =
      { fvarIdToDecl := fvarIdToDecl_1, decls := decls_1, auxDeclToFullName := auxDeclToFullName_1 } →
    fvarIdToDecl = fvarIdToDecl_1 ∧ decls = decls_1 ∧ auxDeclToFullName = auxDeclToFullName_1
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_pi_univ : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [Countable ι] {t : (i : ι) → Set (X i)},
  (∀ (i : ι), MeasurableSet (t i)) → (MeasureTheory.Measure.infinitePi μ) (Set.univ.pi t) = ∏' (i : ι), (μ i) (t i)
-- Init.Data.Bool
Bool.not_xor : ∀ (x y : Bool), (!x ^^ y) = !(x ^^ y)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
IsGreatest.csSup_mem : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α}, IsGreatest s a → sSup s ∈ s
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.target_inter_inv_preimage_preimage : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β), e.target ∩ ↑e.symm ⁻¹' ↑e ⁻¹' s = e.target ∩ s
-- Mathlib.Algebra.Group.Defs
SubtractionCommMonoid.mk : {G : Type u} → [toSubtractionMonoid : SubtractionMonoid G] → (∀ (a b : G), a + b = b + a) → SubtractionCommMonoid G
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.closure_toAddSubmonoid : ∀ {G : Type u_2} [inst : AddGroup G] (S : Set G), (AddSubgroup.closure S).toAddSubmonoid = AddSubmonoid.closure (S ∪ -S)
-- Init.Data.Dyadic.Basic
Dyadic.add_assoc : ∀ (x y z : Dyadic), x + y + z = x + (y + z)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsLimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], (P.limitsOfShape J).IsClosedUnderIsomorphisms
-- Lean.Parser.Command
Lean.Parser.Command.structInstBinder : Lean.Parser.Parser
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_le_sdiff_iff_le : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x ≤ z → y ≤ z → (z \ x ≤ z \ y ↔ y ≤ x)
-- Mathlib.Topology.Category.Profinite.Extend
/-- A bundled version of `S.asLimitCone'` and `S.asLimit'`.  -/
Profinite.lim' : (S : Profinite) → CategoryTheory.Limits.LimitCone S.diagram'
-- Mathlib.Data.Fintype.Defs
OrderDual.fintype : (α : Type u_4) → [Fintype α] → Fintype αᵒᵈ
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The span of the empty set is the bottom of the lattice of subspaces.  -/
Projectivization.Subspace.span_empty : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Projectivization.Subspace.span ∅ = ⊥
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.mk.sizeOf_spec : ∀ {P : Type u_2} [inst : MetricSpace P] [inst_1 : SizeOf P] (center : P) (radius : ℝ),
  sizeOf { center := center, radius := radius } = 1 + sizeOf center + sizeOf radius
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.rightUnitor_inv_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) h) =
    h
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.le_of_exists : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g : CauSeq α abs},
  (∃ i, ∀ j ≥ i, ↑f j ≤ ↑g j) → f ≤ g
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ofBraided_δ_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Center.ofBraided C) X Y).f =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Center.ofBraided C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).fst
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} {hc : k ∈ t.alter k f},
  (t.alter k f).get k hc = (f (t.get? k)).get ⋯
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
/-- `continuousMapPresheaf` is `U ↦ C(ConnectedComponents U, T)` if `T` is totally
disconnected.  -/
AlgebraicGeometry.continuousMapPresheafEquivOfTotallyDisconnectedSpace : (T : Type v) →
  [inst : TopologicalSpace T] →
    [TotallyDisconnectedSpace T] →
      (U : AlgebraicGeometry.Scheme) →
        (AlgebraicGeometry.continuousMapPresheaf T).obj (Opposite.op U) ≃ C(ConnectedComponents ↥U, T)
-- Mathlib.Algebra.Exact.Basic
/-- Two maps `f : M →+ N` and `g : N →+ P` are exact if and only if the induced maps
`AddMonoidHom.range f → N → AddMonoidHom.range g` are exact.  -/
Function.Exact.iff_addMonoidHom_rangeRestrict : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : AddGroup M] [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  {f : M →+ N} {g : N →+ P}, Function.Exact ⇑f ⇑g ↔ Function.Exact ⇑f.range.subtype ⇑g.rangeRestrict
-- Std.Time.Date.Unit.Weekday
/-- Converts a `Nat` to a `Weekday`. Panics if the value provided is invalid.
 -/
Std.Time.Weekday.ofNat! : ℕ → Std.Time.Weekday
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.mk : Lean.Expr →
  Lean.Expr →
    Array Lean.Expr →
      Array Lean.Expr → Array Lean.BinderInfo → Bool → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `Module.Dual.extendRCLike`.

---

Extend `fr : Dual ℝ F` to `Dual 𝕜 F` in a way that will also be continuous and have its norm
(as a continuous linear map) equal to `‖fr‖` when `fr` is itself continuous on a normed space.  -/
LinearMap.extendTo𝕜' : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {F : Type u_2} →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module ℝ F] → [inst_3 : Module 𝕜 F] → [IsScalarTower ℝ 𝕜 F] → Module.Dual ℝ F → Module.Dual 𝕜 F
-- Mathlib.Order.SupIndep
/-- **Alias** of the reverse direction of `sSupIndep_iff_pairwiseDisjoint`. -/
Set.PairwiseDisjoint.sSupIndep : ∀ {α : Type u_1} [inst : Order.Frame α] {s : Set α}, s.PairwiseDisjoint id → sSupIndep s
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- Internal state of the `filterMap` combinator. Do not depend on its internals.
 -/
Std.Iterators.Types.FilterMap : Type w →
  {β γ : Type w} →
    (m : Type w → Type w') →
      (n : Type w → Type w'') → (⦃α : Type w⦄ → m α → n α) → (β → Std.Iterators.PostconditionT n (Option γ)) → Type w
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} [inst_1 : SizeOf C] [inst_2 : SizeOf ι]
  (obj : (i : ι) → ↑(F.obj { as := Opposite.op (X i) }).obj)
  (hom :
    (i₁ i₂ : ι) → obj i₁ ⟶ (F.map (f i₁).op.toLoc).l.toFunctor.obj ((F.map (f i₂).op.toLoc).r.toFunctor.obj (obj i₂)))
  (counit :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (hom i i) ((F.map (f i).op.toLoc).adj.counit.toNatTrans.app (obj i)) =
          CategoryTheory.CategoryStruct.id (obj i))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.counit._autoParam)
  (coassoc :
    autoParam
      (∀ (i₁ i₂ i₃ : ι),
        CategoryTheory.CategoryStruct.comp (hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂ i₃))) =
          CategoryTheory.CategoryStruct.comp (hom i₁ i₃)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map
              ((F.map (f i₂).op.toLoc).adj.unit.toNatTrans.app ((F.map (f i₃).op.toLoc).r.toFunctor.1 (obj i₃)))))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coassoc._autoParam),
  sizeOf { obj := obj, hom := hom, counit := counit, coassoc := coassoc } = 1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.setTag.congr_simp : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId fvarId_1 : Lean.FVarId),
  fvarId = fvarId_1 →
    ∀ (cidx cidx_1 : ℕ),
      cidx = cidx_1 →
        ∀ (k k_1 : Lean.Compiler.LCNF.Code pu),
          k = k_1 →
            ∀ (h : pu = Lean.Compiler.LCNF.Purity.impure),
              Lean.Compiler.LCNF.Code.setTag fvarId cidx k h = Lean.Compiler.LCNF.Code.setTag fvarId_1 cidx_1 k_1 h
-- Mathlib.Data.Set.Lattice
Set.iInter_iInter_eq_left : ∀ {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → x = b → Set α}, ⋂ x, ⋂ (h : x = b), s x h = s b ⋯
-- Lean.Parser.Basic
Lean.Parser.instInhabitedParserCategory : Inhabited Lean.Parser.ParserCategory
-- Lean.AddDecl
_private.Lean.AddDecl.0.Lean.addDeclCore : Lean.Declaration → Bool → Lean.CoreM Unit
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero : ∀ (z : UpperHalfPlane), Filter.Tendsto (fun x => EisensteinSeries.e2Summand x z) Filter.atTop (nhds 0)
-- Mathlib.Data.Countable.Defs
instUncountablePLift : ∀ {α : Sort u} [Uncountable α], Uncountable (PLift α)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImageMap.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq sq_1 : f ⟶ g),
  sq = sq_1 → CategoryTheory.Limits.HasImageMap sq = CategoryTheory.Limits.HasImageMap sq_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffWithinAt.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n (fun x => Real.cosh (f x)) s x
-- Init.Data.UInt.Lemmas
UInt8.toNat_sub_of_le : ∀ (a b : UInt8), b ≤ a → (a - b).toNat = a.toNat - b.toNat
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.le_jacobson_bot : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [IsAdicComplete I R], I ≤ ⊥.jacobson
-- Lean.Elab.PreDefinition.FixedParams
/-- Is this parameter still plausibly a fixed parameter?
 -/
Lean.Elab.FixedParams.Info.mayBeFixed : ℕ → ℕ → Lean.Elab.FixedParams.Info → Bool
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.State.mk.injEq : ∀ (toAssert : Array (Lean.Expr × Lean.Expr × ℕ)) (usedHyps : Std.HashSet Lean.FVarId)
  (toAssert_1 : Array (Lean.Expr × Lean.Expr × ℕ)) (usedHyps_1 : Std.HashSet Lean.FVarId),
  ({ toAssert := toAssert, usedHyps := usedHyps } = { toAssert := toAssert_1, usedHyps := usedHyps_1 }) =
    (toAssert = toAssert_1 ∧ usedHyps = usedHyps_1)
-- Std.Http.Data.Chunk
Std.Http.Chunk.instReprExtensionValue.repr : Std.Http.Chunk.ExtensionValue → ℕ → Std.Format
-- Mathlib.Data.Set.Subset
Set.image_val_preimage_val_subset_self : ∀ {α : Type u_2} {A B : Set α}, Subtype.val '' Subtype.val ⁻¹' B ⊆ B
-- Mathlib.Data.List.Destutter
List.destutter_cons' : ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α},
  List.destutter R (a :: l) = List.destutter' R a l
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedRequestID : Inhabited Lean.JsonRpc.RequestID
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenter_empty : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n), s.excenter ∅ = s.incenter
-- Mathlib.Tactic.SetLike
/-- The Aesop tactic (`aesop`) can automatically prove obvious facts about membership in structures
such as subgroups and subrings. Certain lemmas regarding membership in algebraic substructures
are given the `aesop` attribute according to the following principles:
- Rules are in the `SetLike` ruleset: `(rule_sets := [SetLike])`.
- Apply-style rules with trivial hypotheses are registered both as `simp` rules and as
  `safe` Aesop rules. The latter is needed in case there are metavariables in the goal.
  For instance, Aesop can use the rule `one_mem` to prove
  `(M : Type*) [Monoid M] (s : Submonoid M) ⊢ ∃ m : M, m ∈ s`.
- Apply-style rules with nontrivial hypotheses are marked `unsafe`. This is because applying them
  might not be provability-preserving in the context of more complex membership rules.
  For instance, `mul_mem` is marked `unsafe`.
  - Unsafe rules are given a probability no higher than 90%. This is the same probability
    Aesop gives to safe rules when they generate metavariables. If the priority is too high, loops
    generated in the presence of metavariables will time out Aesop.
  - Rules that cause loops (even in the absence of metavariables) are given a low priority of 5%.
    These rules are placed in the `SetLike!` ruleset instead of the `SetLike` ruleset so that
    they are not invoked by default. An example is `SetLike.mem_of_subset`.
  - Simplifying the left-hand side of a membership goal is prioritised over simplifying the
    right-hand side. By default, rules simplifying the LHS (e.g., `mul_mem`) are given
    probability 90% and rules simplifying the RHS are given probability 80%
    (e.g., `Subgroup.mem_closure_of_mem`).
  - These default probabilities are for rules with simple hypotheses that fail quickly when
    not satisfied, such as `mul_mem`. Rules with more complicated hypotheses, or rules that are
    less likely to progress the proof state towards a solution, are given a lower priority.
- To optimise performance and avoid timeouts, Aesop should not be invoking low-priority rules
  unless it can make no other progress. If common usage patterns cause Aesop to invoke such rules,
  additional lemmas are added at a higher priority to cover that pattern.
  For example, `Subgroup.mem_closure_of_mem` covers a common use case of `SetLike.mem_of_subset`.

Some examples of membership-related goals which Aesop with this ruleset is designed to close
can be found in the file `MathlibTest/set_like.lean`.
 -/
LibraryNote.SetLike_Aesop_ruleset : Batteries.Util.LibraryNote
-- Lean.Meta.Tactic.SplitIf
/-- Split an `if-then-else` in the hypothesis `fvarId`.
 -/
Lean.Meta.splitIfLocalDecl? : Lean.MVarId → Lean.FVarId → optParam (Option Lean.Name) none → Lean.MetaM (Option (Lean.MVarId × Lean.MVarId))
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.unit_pullbackId_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).unit
      ((CategoryTheory.Over.map (CategoryTheory.CategoryStruct.id X)).whiskerLeft
        (CategoryTheory.ChosenPullbacksAlong.pullbackId X).hom) =
    (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.id X)).unit
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.ωConj_invFun : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
  (RootPairing.GeckConstruction.ωConj b).invFun x =
    RootPairing.GeckConstruction.ω b * x * RootPairing.GeckConstruction.ω b
-- Mathlib.Analysis.Convex.Independent
/-- If a family is convex independent, so is any subfamily given by composition of an embedding into
index type with the original family.  -/
ConvexIndependent.comp_embedding : ∀ {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {ι' : Type u_4} (f : ι' ↪ ι) {p : ι → E}, ConvexIndependent 𝕜 p → ConvexIndependent 𝕜 (p ∘ ⇑f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.darts_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v),
  p.reverse.darts = (List.map SimpleGraph.Dart.symm p.darts).reverse
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.nonempty : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s N : Set X},
  Metric.IsCover ε s N → s.Nonempty → N.Nonempty
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.subset_vertexSet_of_mem_edgeSet : ∀ {α : Type u_1} {e : Set α} {H : Hypergraph α}, e ∈ H.edgeSet → e ⊆ H.vertexSet
-- Std.Sat.AIG.Basic
Std.Sat.AIG.unexpandDenote : Lean.PrettyPrinter.Unexpander
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- The counit for the adjunction for `Cocone.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)`.

Auxiliary definition for `functorialityAdjunction`.
 -/
CategoryTheory.Adjunction.functorialityCounit : {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) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  (K : CategoryTheory.Functor J C) →
                    (adj.functorialityRightAdjoint K).comp (CategoryTheory.Limits.Cocone.functoriality K F) ⟶
                      CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone (K.comp F))
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
/-- A non-negative function whose logarithmic counting function is big-O of `log` has finite support.
 -/
Function.locallyFinsuppWithin.finite_support_of_logCounting_isBigO_log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] {D : Function.locallyFinsupp E ℤ},
  0 ≤ D →
    Function.locallyFinsuppWithin.logCounting D =O[Filter.atTop] Real.log →
      (Function.locallyFinsuppWithin.support D).Finite
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- If `ι` is an empty type and `V` is zero-dimensional, there is a unique `ι`-indexed basis.  -/
basisOfFinrankZero : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          [FiniteDimensional K V] → {ι : Type u_1} → [IsEmpty ι] → Module.finrank K V = 0 → Module.Basis ι K V
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular],
  CategoryTheory.IsCardinalPresentable X κ ↔ (CategoryTheory.coyoneda.obj (Opposite.op X)).IsCardinalAccessible κ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.ofList_eq_insertMany : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {l : List (α × β)},
  Std.DTreeMap.Internal.Impl.Const.ofList l =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coe_mem_source : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] (e' : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B}
  {y : E b}, ⟨b, y⟩ ∈ e'.source ↔ b ∈ e'.baseSet
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_iff_source_of_mem_source : ∀ {𝕜 : 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}
  [IsManifold I 1 M] {x' : M},
  x' ∈ (chartAt H x).source →
    (MDiffAt[s] f x' ↔
      MDiffAt[↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I] (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x'))
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.valuedCompletionAtInfty.def : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {x : RatFunc.CompletionAtInfty F},
  Valued.v x = Valued.extensionValuation x
-- Mathlib.GroupTheory.Submonoid.Center
val_addUnitsCenterToCenterAddUnits_apply_coe : ∀ (M : Type u_1) [inst : AddMonoid M] (n : AddUnits ↥(AddSubmonoid.center M)),
  ↑↑((addUnitsCenterToCenterAddUnits M) n) = ↑↑n
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A morphism of chain complexes
induces a morphism of arrows of the differentials out of each object.
 -/
HomologicalComplex.Hom.sqFrom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} →
          {C₁ C₂ : HomologicalComplex V c} →
            C₁.Hom C₂ → (i : ι) → CategoryTheory.Arrow.mk (C₁.dFrom i) ⟶ CategoryTheory.Arrow.mk (C₂.dFrom i)
-- Mathlib.CategoryTheory.Products.Basic
/-- Whiskering by `F` and then evaluating at `a` is the same as evaluating at `F` and then
applying `F`.  -/
CategoryTheory.whiskeringRight_comp_evaluation : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A),
  ((CategoryTheory.Functor.whiskeringRight A B C).obj F).comp ((CategoryTheory.evaluation A C).obj a) =
    ((CategoryTheory.evaluation A B).obj a).comp F
-- Lean.Data.Json.Basic
Lean.JsonNumber.instCoeInt : Coe ℤ Lean.JsonNumber
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instSMulZeroClassOfMulActionHomClass : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {G : ι → Type u_3} →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : Nonempty ι] →
                    [inst_5 : (i : ι) → Zero (G i)] →
                      [inst_6 : (i : ι) → SMulZeroClass R (G i)] →
                        [∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)] →
                          SMulZeroClass R (DirectLimit G f)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 →
    ∀ (a a_1 : α),
      a = a_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → t.getKeyD a fallback = t_1.getKeyD a_1 fallback_1
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.neg_mem_Ico_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a c d : α},
  -a ∈ Set.Ico c d ↔ a ∈ Set.Ioc (-d) (-c)
-- Mathlib.CategoryTheory.Galois.Basic
/-- Definition of a fiber functor from a Galois category. Lenstra, Def 3.1, (G4)-(G6)  -/
CategoryTheory.PreGaloisCategory.FiberFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [CategoryTheory.PreGaloisCategory C] → CategoryTheory.Functor C FintypeCat → Prop