mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.mkNatIso_hom_app_snd : ∀ {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} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)}
  (e₁ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₁ F G))
  (e₂ :
    J.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G) ≅
      K.comp (CategoryTheory.Limits.CategoricalPullback.π₂ F G))
  (coh :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom F)
          (CategoryTheory.CategoryStruct.comp (K.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
            (CategoryTheory.CategoryStruct.comp
              (K.whiskerLeft
                (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                    (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
              (K.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv)) =
        CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₁ F G) F).hom
          (CategoryTheory.CategoryStruct.comp
            (J.whiskerLeft
              (CategoryTheory.CatCommSq.iso (CategoryTheory.Limits.CategoricalPullback.π₁ F G)
                  (CategoryTheory.Limits.CategoricalPullback.π₂ F G) F G).hom)
            (CategoryTheory.CategoryStruct.comp (J.associator (CategoryTheory.Limits.CategoricalPullback.π₂ F G) G).inv
              (CategoryTheory.Functor.whiskerRight e₂.hom G))))
      CategoryTheory.Limits.CategoricalPullback.mkNatIso._auto_1)
  (X_1 : X), ((CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁ e₂ coh).hom.app X_1).snd = e₂.hom.app X_1
-- Lean.DocString.Markdown
/-- Checks whether `c` needs escaping in a context that definitely cannot start a block. `next?` is the
following character, used for the `![…]` image-syntax check.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.midLineSpecial : Char → Option Char → Bool
-- Mathlib.Condensed.Discrete.Colimit
/-- `lanPresheaf (locallyConstantPresheaf X)` is a sheaf for the coherent topology on `Profinite`.
 -/
Condensed.lanSheafProfinite : Type (u + 1) → CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) (Type (u + 1))
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_le_self : ∀ {a : ℤ} (b : ℤ), 0 ≤ a → a.tdiv b ≤ a
-- Mathlib.FieldTheory.Extension
/-- Lifts `L → K` of `F → K`  -/
IntermediateField.Lifts : (F : Type u_1) →
  (E : Type u_2) →
    (K : Type u_3) →
      [inst : Field F] → [inst_1 : Field E] → [inst_2 : Field K] → [Algebra F E] → [Algebra F K] → Type (max u_2 u_3)
-- ImportGraph.Tools.FindHome
/-- Find locations as high as possible in the import hierarchy
where the named declaration could live.
 -/
Lean.Name.findHome : Lean.Name → Option Lean.Environment → Lean.CoreM Lean.NameSet
-- Mathlib.Analysis.SpecificLimits.Basic
uniformity_basis_dist_pow_of_lt_one : ∀ {α : Type u_4} [inst : PseudoMetricSpace α] {r : ℝ},
  0 < r → r < 1 → (uniformity α).HasBasis (fun x => True) fun k => {p | dist p.1 p.2 < r ^ k}
-- Init.Data.RArray
_private.Init.Data.RArray.0.Lean.RArray.getImpl.match_1.eq_2 : ∀ {α : Type u_1} (motive : Lean.RArray α → Sort u_2) (p : ℕ) (l r : Lean.RArray α)
  (h_1 : (x : α) → motive (Lean.RArray.leaf x))
  (h_2 : (p : ℕ) → (l r : Lean.RArray α) → motive (Lean.RArray.branch p l r)),
  (match Lean.RArray.branch p l r with
    | Lean.RArray.leaf x => h_1 x
    | Lean.RArray.branch p l r => h_2 p l r) =
    h_2 p l r
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The underlying function of an element of the incidence algebra.

Do not use this function directly. Instead use the coercion coming from the `FunLike`
instance.  -/
IncidenceAlgebra.toFun : {𝕜 : Type u_7} → {α : Type u_8} → [inst : Zero 𝕜] → [inst_1 : LE α] → IncidenceAlgebra 𝕜 α → α → α → 𝕜
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a fallback : α}, ∅.getD a fallback = fallback
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comap_comp : ∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] {P : Type u} [inst_2 : CommRing P] (f : R →+* S)
  (g : S →+* P) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (W : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top P)) (hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U)
  (hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V),
  AlgebraicGeometry.StructureSheaf.comap (g.comp f) U W ⋯ =
    (AlgebraicGeometry.StructureSheaf.comap g V W hVW).comp (AlgebraicGeometry.StructureSheaf.comap f U V hUV)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesOfIsCycle₂_coe : ∀ {k G A : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup A] [inst_3 : Module k A]
  [inst_4 : DistribMulAction G A] [inst_5 : SMulCommClass G k A] (x : G × G →₀ A) (hx : groupHomology.IsCycle₂ x),
  ↑(groupHomology.cyclesOfIsCycle₂ x hx) = x
-- Init.Data.SInt.Lemmas
ISize.toInt_ofInt_of_two_pow_numBits_le : ∀ {n : ℤ}, -2 ^ (System.Platform.numBits - 1) ≤ n → n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofInt n).toInt = n
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.aemeasurable : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : PseudoEMetricSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {u : Filter ι} [u.NeBot]
  [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E},
  (∀ (n : ι), AEMeasurable (f n) μ) → MeasureTheory.TendstoInMeasure μ f u g → AEMeasurable g μ
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.range_ofIsTopCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) (φ : ↥p →L[R] F)
  (ψ : ↥q →L[R] F), (↑(ContinuousLinearMap.ofIsTopCompl h φ ψ)).range = (↑φ).range ⊔ (↑ψ).range
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.lift_eqToHom_comp_iff : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R' R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : R' = R),
  p.IsHomLift (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f) φ ↔ p.IsHomLift f φ
-- Mathlib.Analysis.Normed.Order.Lattice
/-- If `α` has a solid norm, then the balls centered at the origin of `α` are solid sets.  -/
LatticeOrderedAddCommGroup.isSolid_ball : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] (r : ℝ),
  LatticeOrderedAddCommGroup.IsSolid (Metric.ball 0 r)
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.map_add_left_Ioc : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  [ExistsAddOfLE α] [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Finset.map (addLeftEmbedding c) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.trans : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V}, G.Reachable u v → G.Reachable v w → G.Reachable u w
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertManyIfNewUnit_list_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α}, Std.ExtDTreeMap.Const.insertManyIfNewUnit t l = ∅ ↔ t = ∅ ∧ l = []
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_iSup : ∀ {ι : Sort u_1} {R : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : TopologicalSpace N] [inst_3 : Module R N] [inst_4 : ContinuousAdd N] [inst_5 : ContinuousConstSMul R N]
  {x : N} {f : ι → ClosedSubmodule R N}, x ∈ ⨆ i, f i ↔ x ∈ closure (⨆ i, ↑(f i)).carrier
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.instPowAdicCauchySequenceNat : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Pow (AdicCompletion.AdicCauchySequence I R) ℕ
-- Mathlib.Data.Bundle
Bundle.TotalSpace.exists : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} {p : Bundle.TotalSpace F E → Prop}, (∃ x, p x) ↔ ∃ b y, p ⟨b, y⟩
-- Mathlib.Topology.Defs.Basic
/-- Converts an element of `WithTopology X t` to an element of `X`.  -/
WithTopology.ofTopology : {X : Type u_1} → {t : TopologicalSpace X} → WithTopology X t → X
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.oneEquiv.eq_1 : ∀ (R : Type u) [inst : CommRing R] (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  exteriorPower.oneEquiv R M =
    LinearEquiv.ofLinearMap
      (exteriorPower.alternatingMapLinearEquiv ((AlternatingMap.ofSubsingleton R M M 0) LinearMap.id))
      (have h := ⋯;
      { toFun := fun m => (exteriorPower.ιMulti R 1) fun x => m, map_add' := ⋯, map_smul' := ⋯ })
      ⋯ ⋯
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.equiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [inst_2 : L.IsLocalization W] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y],
  CategoryTheory.Localization.SmallHom.equiv W L =
    (equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm.trans (CategoryTheory.Localization.homEquiv W W.Q L)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.add_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z₁ z₂ : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + n = q),
  (z₁ + z₂).v p q hpq = z₁.v p q hpq + z₂.v p q hpq
-- Init.Coe
instCoeT : {α : Sort u_1} → {a : α} → CoeT α a α
-- Mathlib.Analysis.InnerProductSpace.Orientation
OrthonormalBasis.adjustToOrientation.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {ι : Type u_2} [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] (e e_1 : OrthonormalBasis ι ℝ E),
  e = e_1 →
    ∀ (x x_1 : Orientation ℝ E ι),
      x = x_1 → ∀ [inst_4 : Nonempty ι], e.adjustToOrientation x = e_1.adjustToOrientation x_1
-- Mathlib.GroupTheory.OrderOfElement
smul_eq_self_of_mem_zpowers : ∀ {G : Type u_1} [inst : Group G] {x y : G} {α : Type u_6} [inst_1 : MulAction G α],
  x ∈ Subgroup.zpowers y → ∀ {a : α}, y • a = a → x • a = a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_maxKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {km : α} {hc : Std.DTreeMap.Internal.Impl.contains km t = true}, t.maxKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_add : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  Multiset.toFinsupp (s + t) = Multiset.toFinsupp s + Multiset.toFinsupp t
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.comp_eqToHom_lift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] {a' : 𝒳} (h : a' = a),
  p.IsHomLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) φ)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.veq_iff_eq : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] {x y : R}, x =ᵥ y ↔ v x = v y
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.State.mk.injEq : ∀ (mctx : Lean.MetavarContext) (paramNames : Array Lean.Name) (nextParamIdx : ℕ)
  (cache : Std.HashMap Lean.ExprStructEq Lean.Expr) (mctx_1 : Lean.MetavarContext) (paramNames_1 : Array Lean.Name)
  (nextParamIdx_1 : ℕ) (cache_1 : Std.HashMap Lean.ExprStructEq Lean.Expr),
  ({ mctx := mctx, paramNames := paramNames, nextParamIdx := nextParamIdx, cache := cache } =
      { mctx := mctx_1, paramNames := paramNames_1, nextParamIdx := nextParamIdx_1, cache := cache_1 }) =
    (mctx = mctx_1 ∧ paramNames = paramNames_1 ∧ nextParamIdx = nextParamIdx_1 ∧ cache = cache_1)
-- Init.Core
/-- Type class for the `insert` operation.
Used to implement the `{ a, b, c }` syntax.
 -/
Insert : outParam (Type u) → Type v → Type (max u v)
-- Mathlib.RepresentationTheory.Basic
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` which is trivial on `S` factors
through `G ⧸ S`.  -/
Representation.ofQuotient : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Semiring k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (S : Subgroup G) →
                  [inst_4 : S.Normal] →
                    [Representation.IsTrivial (MonoidHom.comp ρ S.subtype)] → Representation k (G ⧸ S) V
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the coherence composition `η ⊗≫ θ := η ≫ α ≫ θ` with `η : f ⟶ g`
and `θ : h ⟶ i`.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.coherenceComp : Lean.Expr →
  Option Mathlib.Tactic.BicategoryLike.IsoLift →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.CoherenceHom →
              Mathlib.Tactic.BicategoryLike.Mor₂ →
                Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `DFunLike.coe` as a `RingHom`.  -/
LocallyConstant.coeFnRingHom : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : Semiring Y] → LocallyConstant X Y →+* X → Y
-- Init.Data.UInt.Bitwise
USize.toNat_shiftRight : ∀ (a b : USize), (a >>> b).toNat = a.toNat >>> (b.toNat % System.Platform.numBits)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.leftComm_tmul : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (m : A) (n : B) (p : C), (Algebra.TensorProduct.leftComm R A B C) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) = n ⊗ₜ[R] (m ⊗ₜ[R] p)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatApp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] (U : Y.Opens),
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.app f U)
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.quotient_finite_of_isOpen' : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G]
  (U : AddSubgroup G) (K : AddSubgroup ↥U), IsOpen ↑U → IsOpen ↑K → Finite (↥U ⧸ K)
-- Init.Data.Int.Linear
Int.Internal.Linear.Var.denote : Int.Internal.Linear.Context → Int.Internal.Linear.Var → ℤ
-- Std.Async.Signal
Std.Async.instReprSignal.repr : Std.Async.Signal → ℕ → Std.Format
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_of_subset_left : ∀ {α : Type u_1} {s t u : Multiset α}, s ⊆ u → Disjoint u t → Disjoint s t
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- `p' ↦ p -ᵥ p'` as an affine isometric equivalence.  -/
AffineIsometryEquiv.constVSub : (𝕜 : Type u_1) →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] → [inst_3 : PseudoMetricSpace P] → [inst_4 : NormedAddTorsor V P] → P → P ≃ᵃⁱ[𝕜] V
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_π_ne_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {j j' : J},
  j ≠ j' →
    ∀ {Z : C} (h : f j' ⟶ Z),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j') h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- If `[x -[ℝ] x + y] ⊆ s`, then `y` belongs to the positive tangent cone of `s`.  -/
mem_posTangentConeAt_of_segment_subset : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {x y : E},
  segment ℝ x (x + y) ⊆ s → y ∈ posTangentConeAt s x
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.mk : {ι : 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} →
                    (support : Finset ι) →
                      LinearIndepOn R ⇑P.root ↑support →
                        LinearIndepOn R ⇑P.coroot ↑support →
                          (∀ (i : ι),
                              P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support) ∨
                                -P.root i ∈ AddSubmonoid.closure (⇑P.root '' ↑support)) →
                            (∀ (i : ι),
                                P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support) ∨
                                  -P.coroot i ∈ AddSubmonoid.closure (⇑P.coroot '' ↑support)) →
                              P.Base
-- Mathlib.Logic.Function.Basic
Function.Injective.of_comp_iff' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) {g : γ → α},
  Function.Bijective g → (Function.Injective (f ∘ g) ↔ Function.Injective f)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReprExpr : Repr Lean.Grind.CommRing.Expr
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- **Alias** of `Convexity.convexCombPair`.

---

Take a convex combination of two points.  -/
Convexity.convexComboPair : {R : Type u_1} →
  {M : Type u_3} →
    [inst : PartialOrder R] →
      [inst_1 : Semiring R] →
        [inst_2 : IsStrictOrderedRing R] →
          [Convexity.ConvexSpace R M] → (s t : R) → 0 ≤ s → 0 ≤ t → s + t = 1 → M → M → M
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] {Z : AlgebraicGeometry.PresheafedSpace C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict f).hom
      (CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Probability.Moments.CovarianceBilinDual
MeasureTheory.memLp_id_of_self_sub_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] {p : ENNReal},
  MeasureTheory.MemLp (fun x => x - ∫ (y : E), y ∂μ) p μ → MeasureTheory.MemLp id p μ
-- Init.Data.List.Lemmas
List.filterMap_length_eq_length : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α},
  (List.filterMap f l).length = l.length ↔ ∀ a ∈ l, (f a).isSome = true
-- Mathlib.RingTheory.WittVector.Teichmuller
_private.Mathlib.RingTheory.WittVector.Teichmuller.0.WittVector.map_teichmullerFun : ∀ (p : ℕ) {R : Type u_1} {S : Type u_2} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [inst_1 : CommRing S]
  (f : R →+* S) (r : R), (WittVector.map f) (WittVector.teichmullerFun p r) = WittVector.teichmullerFun p (f r)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_one : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid γ] {f : Π₀ (i : ι), β i},
  (f.prod fun x x_1 => 1) = 1
-- Mathlib.Analysis.CStarAlgebra.Exponential
selfAdjoint.expUnitary_zero : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : StarRing A] [inst_3 : ContinuousStar A]
  [inst_4 : CompleteSpace A] [inst_5 : StarModule ℂ A], selfAdjoint.expUnitary 0 = 1
-- Mathlib.Algebra.Group.Defs
/-- An additive semigroup is a type with an associative `(+)`.  -/
AddSemigroup : Type u → Type u
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
/-- When `η` is a Markov kernel, `borelMarkovFromReal Ω η` is a Markov kernel.  -/
ProbabilityTheory.Kernel.instIsMarkovKernelBorelMarkovFromReal : ∀ {α : Type u_1} {Ω : Type u_4} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (η : ProbabilityTheory.Kernel α ℝ) [ProbabilityTheory.IsMarkovKernel η],
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.borelMarkovFromReal Ω η)
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.instInhabitedMethods.default : Lean.Meta.Sym.Simp.Methods
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k (t₁.getKeyD k fallback)
-- Lean.Level
Lean.Level.PP.Result.brecOn.go : {motive_1 : Lean.Level.PP.Result → Sort u} →
  {motive_2 : List Lean.Level.PP.Result → Sort u} →
    (t : Lean.Level.PP.Result) →
      ((t : Lean.Level.PP.Result) → t.below → motive_1 t) →
        ((t : List Lean.Level.PP.Result) → Lean.Level.PP.Result.below_1 t → motive_2 t) → motive_1 t ×' t.below
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.instCoeSortType : CoeSort TopCat (Type u)
-- Mathlib.Logic.Equiv.Basic
Equiv.subtypeSubtypeEquivSubtypeExists_apply_coe : ∀ {α : Sort u_1} (p : α → Prop) (q : Subtype p → Prop) (a : Subtype q),
  ↑((Equiv.subtypeSubtypeEquivSubtypeExists p q) a) = ↑↑a
-- Mathlib.Dynamics.Ergodic.Ergodic
/-- For a quasi-ergodic map, sets that are almost invariant (rather than strictly invariant) are
still either almost empty or full.  -/
QuasiErgodic.ae_mem_or_ae_notMem₀ : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : Set α} {f : α → α} {μ : MeasureTheory.Measure α},
  QuasiErgodic f μ →
    MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s =ᵐ[μ] s → (∀ᵐ (x : α) ∂μ, x ∈ s) ∨ ∀ᵐ (x : α) ∂μ, x ∉ s
-- Mathlib.Algebra.Order.Pi
Function.extend_nonneg : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Zero γ] [inst_1 : LE γ] {f : α → β} {g : α → γ} {e : β → γ},
  0 ≤ g → 0 ≤ e → 0 ≤ Function.extend f g e
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.instHasCardinalFilteredColimitsOfHasColimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v₁, u₁} C], CategoryTheory.HasCardinalFilteredColimits C κ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false → (Std.HashMap.Raw.ofList l).getD k fallback = fallback
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.IsAcc.inter_Ioo_nonempty : ∀ {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}}, o.IsAcc S → ∀ {p : Ordinal.{u_1}}, p < o → (S ∩ Set.Ioo p o).Nonempty