mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mkIso_hom_right : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right)
  (base : ψ.base ≅ ψ'.base)
  (left_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left.hom F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_1)
  (right_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right.hom G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_3),
  (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).hom.right = right.hom
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_map_iff : ∀ {ι : Type u_5} {κ : Type u_6} {X : Type u_7} {r : X → X → Prop} {f : ι → X} {φ : κ → ι} {𝓕 : Filter κ},
  Filter.IsBoundedUnder r (Filter.map φ 𝓕) f ↔ Filter.IsBoundedUnder r 𝓕 (f ∘ φ)
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_iff : ∀ {f : ℕ → ℕ}, Primrec f ↔ Nat.Primrec f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Complex.cosh` is complex analytic.  -/
Complex.analyticOnNhd_cosh : ∀ {s : Set ℂ}, AnalyticOnNhd ℂ Complex.cosh s
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.NullMeasurableSet.mono : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ν ≤ μ → MeasureTheory.NullMeasurableSet s ν
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.PlausibleIterStep.yield.congr_simp : ∀ {α : Type u} {β : Type w} {IsPlausibleStep : Std.IterStep α β → Prop} (it' it'_1 : α) (e_it' : it' = it'_1)
  (out out_1 : β) (e_out : out = out_1) (h : IsPlausibleStep (Std.IterStep.yield it' out)),
  Std.PlausibleIterStep.yield it' out h = Std.PlausibleIterStep.yield it'_1 out_1 ⋯
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  {x x' : ↑(X.presheaf.obj (Opposite.op ⊤))} {t t' : A} {d d' : ℕ} {H : f t = x} {h0d : 0 < d} {hd : t ∈ 𝒜 d}
  {H' : f t' = x'} {h0d' : 0 < d'} {hd' : t' ∈ 𝒜 d'} {s : A} (hts : t * s = t') {n : ℕ} (hn : d + n = d'),
  s ∈ 𝒜 n →
    CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f H h0d hd)
          (AlgebraicGeometry.Proj.basicOpen 𝒜 t).ι) =
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f H' h0d' hd')
        (AlgebraicGeometry.Proj.basicOpen 𝒜 t').ι
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.find?_some_eq_eq : ∀ {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α}, x ∈ RBTree.RBNode.find? cut t → cut x = Ordering.eq
-- Mathlib.ModelTheory.PartialEquiv
/-- Two structures `M` and `N` form an extension pair if the domain of any finitely-generated map
from `M` to `N` can be extended to include any element of `M`.  -/
FirstOrder.Language.IsExtensionPair : (L : FirstOrder.Language) → (M : Type w) → (N : Type w') → [L.Structure M] → [L.Structure N] → Prop
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A set `B` is a `G`-fixed block if `g +ᵥ B = B` for all `g : G`.  -/
AddAction.IsFixedBlock : (G : Type u_1) → {X : Type u_2} → [VAdd G X] → Set X → Prop
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_one_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R),
  ⌈1 + a⌉ = 1 + ⌈a⌉
-- Mathlib.Order.Interval.Finset.Floor
/-- The `0 ≤ b` hypothesis in `cast_mem_Ioc_iff` can be dropped if `IsStrictOrderedRing α`.  -/
Nat.cast_mem_Ioc_iff' : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {a b : α} {n : ℕ}
  [IsStrictOrderedRing α], 0 ≤ a → (↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊)
-- Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
_private.Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ.0.WeierstrassCurve.exists_variableChange_of_char_three : ∀ {F : Type u_1} [inst : Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [inst_2 : E.IsElliptic]
  [inst_3 : E'.IsElliptic] [CharP F 3], E.j = E'.j → ∃ C, C • E = E'
-- Init.Data.Array.Lemmas
Array.getElem!_eq_getD : ∀ {α : Type u_1} [inst : Inhabited α] {xs : Array α} {i : ℕ}, xs[i]! = xs.getD i default
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι_D₂_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j j' : ι₄) (h : ⋯ = j)
  [inst_23 : ⋯], ⋯
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link.eq_3 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr_2 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) (sz_1 : ℕ) (k'_1 : α) (v'_1 : β k'_1)
  (l'_1 r'_1 : Std.DTreeMap.Internal.Impl α β)
  (hr_4 : (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1).Balanced),
  Std.DTreeMap.Internal.Impl.link k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')
      (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1) hr_2 hr_4 =
    if h₁ : Std.DTreeMap.Internal.delta * sz < sz_1 then
      match Std.DTreeMap.Internal.Impl.link k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') l'_1 ⋯ ⋯ with
      | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balanceLErase k'_1 v'_1 ℓ r'_1 ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
    else
      if h₂ : Std.DTreeMap.Internal.delta * sz_1 < sz then
        match
          Std.DTreeMap.Internal.Impl.link k v r' (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1) ⋯ ⋯ with
        | { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ } =>
          { impl := Std.DTreeMap.Internal.Impl.balanceRErase k' v' l' ℓ ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
      else
        {
          impl :=
            Std.DTreeMap.Internal.Impl.inner (sz + 1 + sz_1) k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')
              (Std.DTreeMap.Internal.Impl.inner sz_1 k'_1 v'_1 l'_1 r'_1),
          balanced_impl := ⋯, size_impl := ⋯ }
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.instCategory : {C : Type u₁} →
  {D : Type u₂} →
    [CategoryTheory.Category.{v, u₂} D] →
      {F : C → D} → CategoryTheory.Category.{v, u₁} (CategoryTheory.InducedCategory D F)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.IsLimit.lift_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {s : CategoryTheory.Limits.WidePullbackCone f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (b : W ⟶ X)
  (a : (i : ι) → W ⟶ Y i) (w : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (a i) (f i) = b) (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullbackCone.IsLimit.lift hs b a w) (s.π i) = a i
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.zero_lt_posForm_apply_root : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [inst_9 : FaithfulSMul S R] [inst_10 : Module S M]
  [inst_11 : IsScalarTower S R M] (i : ι) (hi : optParam (P.root i ∈ Submodule.span S (Set.range ⇑P.root)) ⋯),
  0 < (B.posForm ⟨P.root i, hi⟩) ⟨P.root i, hi⟩
-- Lean.Data.Options
Lean.Options.contains : Lean.Options → Lean.Name → Bool
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.updateLastTag : Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctorMonoidal : {M : Type u} →
  [inst : Monoid M] →
    {N : Type u'} → [inst_1 : Monoid N] → (F : M →* N) → (CategoryTheory.Discrete.monoidalFunctor F).Monoidal
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentFilter.mk.inj : ∀ {language? scheme? pattern? language?_1 scheme?_1 pattern?_1 : Option String},
  { language? := language?, scheme? := scheme?, pattern? := pattern? } =
      { language? := language?_1, scheme? := scheme?_1, pattern? := pattern?_1 } →
    language? = language?_1 ∧ scheme? = scheme?_1 ∧ pattern? = pattern?_1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.filterMap.eq_1 : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [inst_1 : Monad m] (f : β → Option γ)
  (it : Std.IterM m β), Std.IterM.filterMap f it = Std.IterM.filterMapWithPostcondition (fun b => pure (f b)) it
-- Mathlib.Analysis.Convex.Gauge
comap_gauge_nhds_zero : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], Bornology.IsVonNBounded ℝ s → s ∈ nhds 0 → Filter.comap (gauge s) (nhds 0) = nhds 0
-- Mathlib.Data.Int.Cast.Basic
Int.cast_neg : ∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℤ), ↑(-n) = -↑n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∈ m → m.getKey? k = some k
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_map_epi : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  Function.Surjective ⇑f → ∀ [CategoryTheory.Epi φ] (i : ℕ), CategoryTheory.Epi ((groupHomology.chainsMap f φ).f i)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instCoeSubmodule : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → Coe (ClosedSubmodule R M) (Submodule R M)
-- Mathlib.Data.Fintype.Shrink
Fintype.card_shrink : ∀ {α : Type u} [inst : Fintype α] [inst_1 : Fintype (Shrink.{v, u} α)], Fintype.card (Shrink.{v, u} α) = Fintype.card α
-- Mathlib.Data.List.Basic
List.eq_of_mem_map_const : ∀ {α : Type u} {β : Type v} {b₁ b₂ : β} {l : List α}, b₁ ∈ List.map (Function.const α b₂) l → b₁ = b₂
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- There is a canonical map from the stalk to the original fiber, given by evaluating sections.
 -/
TopCat.stalkToFiber : {X : TopCat} →
  {T : ↑X → Type u_1} → (P : TopCat.LocalPredicate T) → (x : ↑X) → (TopCat.subsheafToTypes P).presheaf.stalk x ⟶ T x
-- Std.Net.Addr
Std.Net.SocketAddress.v6.injEq : ∀ (addr addr_1 : Std.Net.SocketAddressV6),
  (Std.Net.SocketAddress.v6 addr = Std.Net.SocketAddress.v6 addr_1) = (addr = addr_1)
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.ker_eq_range_of_comp_eq_id : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_10} {P : Type u_11} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup P] [inst_4 : Module R P] {f : M →ₗ[R] P} {g : P →ₗ[R] M},
  f ∘ₗ g = LinearMap.id → f.ker = (LinearMap.id - g ∘ₗ f).range
-- Mathlib.Order.Extension.Linear
instInhabitedLinearExtension : {α : Type u} → [Inhabited α] → Inhabited (LinearExtension α)
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.mem_coe' : ∀ {P : Type u_2} [inst : MetricSpace P] {p : P} {s : EuclideanGeometry.Sphere P}, dist p s.center = s.radius ↔ p ∈ s
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.reflection_apply_root' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [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} {i j : ι}
  (S : Type u_7) [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : Module S M] [IsScalarTower S R M]
  [inst_9 : P.IsValuedIn S], (P.reflection i) (P.root j) = P.root j - P.pairingIn S j i • P.root i
-- Mathlib.Algebra.Lie.Basic
LieEquiv.mk.sizeOf_spec : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] [inst_5 : SizeOf R] [inst_6 : SizeOf L] [inst_7 : SizeOf L']
  (toLieHom : L →ₗ⁅R⁆ L') (invFun : L' → L)
  (left_inv : autoParam (Function.LeftInverse invFun (↑toLieHom).toFun) LieEquiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun (↑toLieHom).toFun) LieEquiv.right_inv._autoParam),
  sizeOf { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } = 1 + sizeOf toLieHom
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyGE : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) → (t : Std.DTreeMap.Internal.Impl α β) → t.Ordered → (∃ a ∈ t, (compare a k).isGE = true) → α
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_fiberwise : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} {α : Type u_1}
  (g : BoxIntegral.Box ι → α) (f : (ι → ℝ) → E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤)
  (π : BoxIntegral.TaggedPrepartition I),
  ∑ y ∈ Finset.image g π.boxes, BoxIntegral.integralSum f vol (π.filter fun x => g x = y) =
    BoxIntegral.integralSum f vol π
-- Mathlib.Analysis.Calculus.FDeriv.Comp
/-- **Alias** of `fderivWithin_fun_comp`.

---

Eta-expanded form of `fderivWithin_comp` -/
fderivWithin_comp' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G} {t : Set F},
  DifferentiableWithinAt 𝕜 g t (f x) →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t →
        UniqueDiffWithinAt 𝕜 s x →
          fderivWithin 𝕜 (fun x => g (f x)) s x = fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderMonoidHom.congr_simp : ∀ (G : Type u_3) [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G]
  [inst_3 : LocallyFiniteOrder G], LocallyFiniteOrder.orderMonoidHom G = LocallyFiniteOrder.orderMonoidHom G
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Iic_castAdd : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a : Fin n),
  ∑ i ≤ Fin.castAdd m a, f i = ∑ i ≤ a, f (Fin.castAdd m i)
-- Mathlib.Algebra.Star.StarAlgHom
/-- `algebraMap R A` as a `StarAlgHom` when `A` is a star algebra over `R`.  -/
StarAlgHom.ofId : (R : Type u_7) →
  (A : Type u_8) →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] → [inst_3 : StarMul A] → [inst_4 : Algebra R A] → [StarModule R A] → R →⋆ₐ[R] A
-- Std.Http.Data.URI.Basic
/-- Creates a `Scheme` from a string, normalizing to lowercase. Panics if invalid.
 -/
Std.Http.URI.Scheme.ofString! : String → Std.Http.URI.Scheme
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isoFinYonedaComponents_inv_comp : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  {X Y : Profinite} [inst_1 : Finite ↑X.toTop] [inst_2 : Finite ↑Y.toTop]
  (f : ↑Y.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (Condensed.isoFinYonedaComponents F X).inv)
      (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom g)) =
    (CategoryTheory.ConcreteCategory.hom (F.map g.op))
      ((CategoryTheory.ConcreteCategory.hom (Condensed.isoFinYonedaComponents F Y).inv) f)
-- Init.Meta.Defs
Lean.TSyntax.Compat.instCoeTailSyntax : {k : Lean.SyntaxNodeKinds} → CoeTail Lean.Syntax (Lean.TSyntax k)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.map₂_leftUnitor_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.id
      ((F.map f).toFunctor.obj ((CategoryTheory.CategoryStruct.id (F.obj a)).toFunctor.obj X)) =
    CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).toNatTrans.app X)
        ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X))
-- Mathlib.RingTheory.SimpleModule.Isotypic
isotypicComponent.eq_1 : ∀ (R : Type u_2) (M : Type u) (S : Type u_4) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup S]
  [inst_3 : Module R M] [inst_4 : Module R S], isotypicComponent R M S = sSup {m | Nonempty (↥m ≃ₗ[R] S)}
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.instSmallOppositeObjFunctorTypeYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X : C),
  CategoryTheory.FunctorToTypes.Small.{w, v, v, u} (CategoryTheory.yoneda.obj X)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
CategoryTheory.Limits.IsInitial.isInitialObj.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X : C)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) G]
  (l l_1 : CategoryTheory.Limits.IsInitial X),
  l = l_1 → CategoryTheory.Limits.IsInitial.isInitialObj G X l = CategoryTheory.Limits.IsInitial.isInitialObj G X l_1
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K], (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = 1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D)
  [CategoryTheory.Functor.IsDenseSubsite J K G] {U V : C} (f : G.obj U ⟶ G.obj V), G.imageSieve f ∈ J U
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.mem_toCloseds : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] {x : α} {s : TopologicalSpace.Compacts α},
  x ∈ s.toCloseds ↔ x ∈ s
-- Mathlib.Algebra.Group.Subgroup.Basic
AddGroup.mem_addConjugatesOfSet_iff : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G} {x : G}, x ∈ AddGroup.addConjugatesOfSet s ↔ ∃ a ∈ s, IsAddConj a x
-- Std.Time.Date.PlainDate
/-- Creates a new `PlainDate` by adjusting the day of the month to the given `days` value, with any
out-of-range days clipped to the nearest valid date.
 -/
Std.Time.PlainDate.withDaysClip : Std.Time.PlainDate → Std.Time.Day.Ordinal → Std.Time.PlainDate
-- Mathlib.RingTheory.Localization.AsSubring
Localization.mapToFractionRing_apply : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] {B : Type u_3} [inst_4 : CommRing B] [inst_5 : Algebra A B]
  [inst_6 : IsLocalization S B] (hS : S ≤ nonZeroDivisors A) (b : B),
  (Localization.mapToFractionRing K S B hS) b = (IsLocalization.lift ⋯) b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.H1π_comp_map : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupCohomology.H1π A) (groupCohomology.map f φ 1) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₁ f φ) (groupCohomology.H1π B)
-- Init.Data.ByteArray.Lemmas
ByteArray.append_empty : ∀ {b : ByteArray}, b ++ ByteArray.empty = b
-- Mathlib.Analysis.Normed.Module.Convex
/-- **Alias** of `isConnected_setOfPred_sameRay`.

---

The set of vectors in the same ray as `x` is connected.  -/
isConnected_setOf_sameRay : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (x : E), IsConnected {y | SameRay ℝ x y}
-- Init.Data.Array.Nat
Array.min_mul_length_le_sum_nat : ∀ {xs : Array ℕ} (h : xs ≠ #[]), xs.min h * xs.size ≤ xs.sum
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.freeYoneda.isSeparating : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat),
  (PresheafOfModules.freeYoneda R).IsSeparating
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative
UniqueFactorizationMonoid.prime_pow_coprime_prod_of_coprime_insert : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] [inst_2 : DecidableEq α] {s : Finset α}
  (i : α → ℕ),
  ∀ p ∉ s,
    (∀ q ∈ insert p s, Prime q) →
      (∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q') → IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
-- Init.Data.Bool
Bool.eq_true_and_eq_false_self : ∀ (b : Bool), b = true ∧ b = false ↔ False