mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.ext_hom_iff : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {N : Type u_3} [inst_1 : Monoid N]
  {f g : Monoid.CoprodI M →* N}, f = g ↔ ∀ (i : ι), f.comp Monoid.CoprodI.of = g.comp Monoid.CoprodI.of
-- Lean.Elab.Util
Lean.Elab.checkSyntaxNodeKindAtCurrentNamespaces : Lean.Name → Lean.AttrM Lean.Name
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.uniqueHom : {A : Type u} → (x y : CategoryTheory.Codiscrete A) → Unique (x ⟶ y)
-- Std.Data.TreeMap.Raw.Basic
/-- Returns an array of all keys present in the tree map in ascending  order.  -/
Std.TreeMap.Raw.keysArray : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → Array α
-- Mathlib.Analysis.Asymptotics.TVS
/-- We say that `f =Θ[𝕜; l] g` (`IsThetaTVS 𝕜 l f g`), if `f =O[𝕜; l] g` and `g =O[𝕜; l] f`.
It is a generalization of `f =Θ[l] g` that works in topological `𝕜`-vector spaces.  -/
Asymptotics.«term_=Θ[_;_]_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i)
          (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
            (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i))) =
    CategoryTheory.Limits.pullback.fst f g
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.Monic.eq_1 : ∀ {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.Monic f = (m.leadingCoeff f = 1)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_cast : ∀ {m n : ℕ} (h : m = n) (s : Set (Fin m)), Fin.cast h '' s = Fin.cast ⋯ ⁻¹' s
-- Mathlib.Topology.Category.LightProfinite.Sequence
LightProfinite.instCountableCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyNatUnionInfty : Countable ↑LightProfinite.NatUnionInfty.toTop
-- Mathlib.Order.Cover
Pi.exists_forall_eq_of_covBy : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i},
  a ⋖ b → ∃ i, ∀ (j : ι), j ≠ i → a j = b j
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.saveState : Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.SavedState
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.isOpen_iff : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {s : Set Γ₀}, IsOpen s ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Set.Iio γ ⊆ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.Affine.Point.sym2x_some_some : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y x' y' : R} (h : W'.Nonsingular x y)
  (h' : W'.Nonsingular x' y'),
  (WeierstrassCurve.Affine.Point.some x y h).sym2x (WeierstrassCurve.Affine.Point.some x' y' h') = ![x * x', x + x', 1]
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap.eq_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.I₀),
  AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullbackRightPullbackFstIso s.fst (𝒰.f j)
          ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)).hom
      (CategoryTheory.Limits.pullback.map
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i) s.fst)
        (𝒰.f j)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.f i)).hom
          (CategoryTheory.Limits.pullback.map (𝒰.f i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
            (CategoryTheory.CategoryStruct.id (𝒰.X i)) s.snd f ⋯ ⋯))
        (CategoryTheory.CategoryStruct.id (𝒰.X j)) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.contDiffOn_extendCoordChange : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} [inst_5 : ChartedSpace H M],
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I n M →
      ContDiffOn 𝕜 n (↑(ModelWithCorners.extendCoordChange e e')) (ModelWithCorners.extendCoordChange e e').source
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.fintypeQuotient : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] → [IsTopologicalGroup G] → [CompactSpace G] → (H : OpenSubgroup G) → Fintype (G ⧸ ↑H)
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of the forward direction of `tendsto_div_nhds_one_iff_eq`.

---

If `f → a` and `g → b` along a nontrivial filter on the domain, valued in a
Hausdorff topological group, then `f / g → 1` if and only if `a = b`.  -/
eq_of_tendsto_div_nhds_one : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {α : Type u_1} {l : Filter α}
  [l.NeBot] [T2Space G] {f g : α → G} {a b : G},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto g l (nhds b) → Filter.Tendsto (fun x => f x / g x) l (nhds 1) → a = b
-- Mathlib.Order.Birkhoff
/-- The **Birkhoff Embedding** of a finite partial order as inf-irreducible elements in its
lattice of lower sets.  -/
OrderEmbedding.infIrredUpperSet : {α : Type u_1} → [inst : PartialOrder α] → α ↪o { s // InfIrred s }
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.FG.restrictScalars_of_surjective : ∀ {R : Type u_4} {A : Type u_5} {M : Type u_6} [inst : Semiring A] [inst_1 : AddCommMonoid M] [inst_2 : Module A M]
  {S : Submodule A M} [inst_3 : CommSemiring R] [inst_4 : Algebra R A] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M], S.FG → Function.Surjective ⇑(algebraMap R A) → (Submodule.restrictScalars R S).FG
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst l).contains k = false → (Std.ExtDHashMap.ofList l).getKey! k = default
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- **Alias** of `Metric.exists_contMDiffMap_forall_closedEBall_subset`.

---

Let `M` be a smooth σ-compact manifold with extended distance. Let `K : ι → Set M` be a locally
finite family of closed sets, let `U : ι → Set M` be a family of open sets such that `K i ⊆ U i` for
all `i`. Then there exists a positive smooth function `δ : M → ℝ≥0` such that for any `i` and
`x ∈ K i`, we have `Metric.closedEBall x (δ x) ⊆ U i`.  -/
Emetric.exists_contMDiffMap_forall_closedBall_subset : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) [FiniteDimensional ℝ E] {n : ℕ∞} {M : Type u_1}
  [inst_4 : EMetricSpace M] [inst_5 : ChartedSpace H M] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] {K U : ι → Set M},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K →
          ∃ δ, (∀ (x : M), 0 < δ x) ∧ ∀ (i : ι), ∀ x ∈ K i, Metric.closedEBall x (ENNReal.ofReal (δ x)) ⊆ U i
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- For a unital C⋆-subalgebra `S` of `A` and `x : S`, if `↑x : A` is invertible in `A`, then
`x` is invertible in `S`.  -/
StarSubalgebra.coe_isUnit : ∀ {A : Type u_1} [inst : CStarAlgebra A] (S : StarSubalgebra ℂ A) [hS : IsClosed ↑S] {a : ↥S}, IsUnit ↑a ↔ IsUnit a
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The isomorphism between the `-n-1`-th Tate cohomology and `n`-th group homology for `n : ℕ`
non-zero.  -/
TateCohomology.isoGroupHomology : {R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] →
      [inst_2 : Fintype G] →
        (m : ℤ) → (n : ℕ) → m = -(↑n + 1) → [NeZero n] → tateCohomologyFunctor m ≅ groupHomology.functor R G n
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- Let `P` be a predicate on `Set J.obj` where `J : CardinalDirectedPoset κ`.
We assume that `Subtype P` is directed and nonempty, and that any `a : J.obj`
belongs to some `S : Set J.obj` satisfying `P`. Then, `J` is the colimit in the
category `CardinalDirectedPoset κ` of these subsets.  -/
CategoryTheory.CardinalDirectedPoset.isColimitCoconeOfPredicateSet : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    {J : CategoryTheory.CardinalDirectedPoset κ} →
      (P : Set ↑J.obj → Prop) →
        [IsDirectedOrder (Subtype P)] →
          [Nonempty (Subtype P)] →
            [inst_3 : ∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] →
              (∀ (a : ↑J.obj), ∃ S, P S ∧ a ∈ S) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet P)
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.dual_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s → AntivaryOn (⇑OrderDual.toDual ∘ f) g s
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.continuousAt_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace Y]
  [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace Z],
  Topology.IsInducing g → ∀ {x : X}, ContinuousAt f x ↔ ContinuousAt (g ∘ f) x
-- Mathlib.Order.SetNotation
supSet_to_nonempty : ∀ (α : Type u_1) [SupSet α], Nonempty α
-- Init.Omega.IntList
Lean.Omega.IntList.mul_cons₂ : ∀ {x : ℤ} {xs : List ℤ} {y : ℤ} {ys : List ℤ}, (x :: xs) * (y :: ys) = x * y :: xs * ys
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.mk.injEq : ∀ {R : Type u} [inst : LE R] [inst_1 : AddCommMonoid R] [inst_2 : One R] {M : Type v} (weights : M →₀ R)
  (nonneg : 0 ≤ weights) (total : (weights.sum fun x r => r) = 1) (weights_1 : M →₀ R) (nonneg_1 : 0 ≤ weights_1)
  (total_1 : (weights_1.sum fun x r => r) = 1),
  ({ weights := weights, nonneg := nonneg, total := total } =
      { weights := weights_1, nonneg := nonneg_1, total := total_1 }) =
    (weights = weights_1)
-- Mathlib.Data.PNat.Factors
instSubPrimeMultiset : Sub PrimeMultiset
-- Init.Data.BitVec.Lemmas
/-- Sign-extending to `w + n` bits, extracting bits `[w - 1 + n..n]`, and setting width
back to `w` is equivalent to arithmetic right shift by `n`, since both sides discard the `n`
least significant bits and replicate the sign bit into the upper bits.  -/
BitVec.signExtend_extractLsb_setWidth : ∀ {w : ℕ} {x : BitVec w} {n : ℕ},
  BitVec.setWidth w (BitVec.extractLsb (w - 1 + n) n (BitVec.signExtend (w + n) x)) = x.sshiftRight n
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.eval_indicator_apply_eq_one : ∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Fintype σ] [inst_2 : CommRing K] (a : σ → K),
  (MvPolynomial.eval a) (MvPolynomial.indicator a) = 1
-- Mathlib.Analysis.Normed.Ring.Basic
NormedCommRing.toCommRing : {α : Type u_5} → [self : NormedCommRing α] → CommRing α
-- Mathlib.RingTheory.FiniteType
/-- An algebra is finitely generated if and only if it is a quotient
of a polynomial ring whose variables are indexed by a fintype.  -/
Algebra.FiniteType.iff_quotient_freeAlgebra' : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Algebra.FiniteType R A ↔ ∃ ι x f, Function.Surjective ⇑f
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mkOfUnitCounit_unit : ∀ {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 : CategoryTheory.Adjunction.CoreUnitCounit F G), (CategoryTheory.Adjunction.mkOfUnitCounit adj).unit = adj.unit
-- Mathlib.Analysis.Normed.Module.Complemented
/-- Projection to a closed submodule along a closed complement.  -/
Submodule.linearProjOfClosedCompl : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [CompleteSpace E] → (p q : Subspace 𝕜 E) → IsCompl p q → IsClosed ↑p → IsClosed ↑q → E →L[𝕜] ↥p
-- Mathlib.Algebra.Lie.Prod
LieHom.prodMap_zero : ∀ {R : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {L₃ : Type u_5} {L₄ : Type u_6} [inst : CommRing R]
  [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂]
  [inst_5 : LieRing L₃] [inst_6 : LieAlgebra R L₃] [inst_7 : LieRing L₄] [inst_8 : LieAlgebra R L₄],
  LieHom.prodMap 0 0 = 0
-- Mathlib.Analysis.Convex.Function
/-- The pointwise minimum of concave functions is concave.  -/
ConcaveOn.inf : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f g : E → β}, ConcaveOn 𝕜 s f → ConcaveOn 𝕜 s g → ConcaveOn 𝕜 s (f ⊓ g)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
/-- Given a morphism of presheaves of rings `S ⟶ F.op ⋙ R`, this is the adjunction
between associated pullback and pushforward functors on the categories
of presheaves of modules.  -/
PresheafOfModules.pullbackPushforwardAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor Dᵒᵖ RingCat} →
            {S : CategoryTheory.Functor Cᵒᵖ RingCat} →
              (φ : S ⟶ F.op.comp R) →
                [inst_2 : (PresheafOfModules.pushforward φ).IsRightAdjoint] →
                  PresheafOfModules.pullback φ ⊣ PresheafOfModules.pushforward φ
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.map_prod_swap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η], (κ.prod η).map Prod.swap = η.prod κ
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A constant. It stores the name and the arity.  -/
Lean.Meta.RefinedDiscrTree.Key.const : Lean.Name → ℕ → Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.b : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      {n : ℕ} →
        {Z : C} → AlgebraicTopology.DoldKan.MorphComponents X n Z → Fin (n + 1) → (X.obj (Opposite.op { len := n }) ⟶ Z)
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_le_map_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H K : Subgroup G},
  Subgroup.map f H ≤ Subgroup.map f K ↔ H ≤ K ⊔ f.ker
-- Mathlib.Topology.Instances.TrivSqZeroExt
_private.Mathlib.Topology.Instances.TrivSqZeroExt.0.termTsze : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `get` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.getₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [inst_1 : Std.OrientedOrd α] →
        [inst_2 : Std.LawfulEqOrd α] → (l : Std.DTreeMap.Internal.Impl α β) → (k : α) → (l.get?ₘ k).isSome = true → β k
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_filterMap_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ},
  t.WF →
    ((Std.DTreeMap.Raw.filterMap f t).isEmpty = true ↔
      ∀ (k : α) (h : k ∈ t), f (t.getKey k h) (Std.DTreeMap.Raw.Const.get t k h) = none)
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.llp_isStableUnderRetracts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C),
  T.llp.IsStableUnderRetracts
-- Mathlib.Algebra.Order.Group.Abs
abs_sub_abs_le_abs_sub : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a b : G), |a| - |b| ≤ |a - b|
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.limitToAlgEquiv_apply : ∀ {k : Type u_3} {K : Type u_4} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [inst_3 : IsGalois k K]
  (g : ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop) (a : K),
  (InfiniteGalois.limitToAlgEquiv g) a = InfiniteGalois.toAlgEquivAux✝ g a
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk : ∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) [P.toProperty.RespectsIso],
  (∀ ⦃X Y S : AlgebraicGeometry.Scheme⦄ [inst : AlgebraicGeometry.IsAffine S] [inst_1 : AlgebraicGeometry.IsAffine X]
      (f : X ⟶ S) (g : Y ⟶ S), P g → P (CategoryTheory.Limits.pullback.fst f g)) →
    P.IsStableUnderBaseChange
-- Mathlib.GroupTheory.OrderOfElement
/-- **Alias** of the reverse direction of `isOfFinOrder_iff_isUnit`. -/
IsUnit.isOfFinOrder : ∀ {G : Type u_1} [inst : Monoid G] [Finite Gˣ] {x : G}, IsUnit x → IsOfFinOrder x
-- Std.Http.Internal.IndexMultiMap
/-- Retrieves all values for the given key.
 -/
Std.Internal.IndexMultiMap.getAll : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → (map : Std.Internal.IndexMultiMap α β) → (key : α) → key ∈ map → Array β
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_compl_mul_self_apply : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] (s : Set α) (f : α → M) (a : α),
  sᶜ.mulIndicator f a * s.mulIndicator f a = f a
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instCofibrationOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : C} (f : X ⟶ Y)
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)]
  [CategoryTheory.IsIso f], HomotopicalAlgebra.Cofibration f
-- Init.Data.Array.Lemmas
/-- Variant of `any_beq` with `==` reversed.  -/
Array.any_beq' : ∀ {α : Type u_1} {a : α} [inst : BEq α] [PartialEquivBEq α] {xs : Array α}, (xs.any fun x => x == a) = xs.contains a
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightEq_inv_app_left : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (r r' : R₂ ⟶ R₁) (h : r = r') (X : CategoryTheory.Comma L R₂),
  ((CategoryTheory.Comma.mapRightEq L r r' h).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_sum_plift_of_support_toFinset_subset : ∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] {f : α → M} (hf : Function.HasFiniteSupport (f ∘ PLift.down))
  {s : Finset (PLift α)}, Set.Finite.toFinset hf ⊆ s → ∑ᶠ (i : α), f i = ∑ i ∈ s, f i.down
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `NatModule` instance for `type`  -/
Lean.Meta.Grind.Arith.Linear.NatStruct.natModuleInst : Lean.Meta.Grind.Arith.Linear.NatStruct → Lean.Expr
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_le_floor : ∀ {r s : ENNReal}, r ≤ s → ⌊r⌋ₑ ≤ ⌊s⌋ₑ
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp.eq_1 : ∀ (x : EReal), x.exp = EReal.rec 0 (fun x => ENNReal.ofReal (Real.exp x)) ⊤ x
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.GrothendieckTopology.HOneHypercover.instNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {S : C},
  Nonempty (J.HOneHypercover S)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α}, (a == b) = true → m.contains a = m.contains b
-- Mathlib.LinearAlgebra.BilinearMap
/-- A version of `Function.Bijective.comp` for composition of a bilinear map with a linear map.  -/
LinearMap.bijective_compr₂ₛₗ_of_equiv : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {R₄ : Type u_16} {M : Type u_17}
  {N : Type u_18} {P : Type u_19} {Q : Type u_20} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃]
  [inst_3 : CommSemiring R₄] [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : AddCommMonoid Q] [inst_8 : Module R M] [inst_9 : Module R₂ N] [inst_10 : Module R₃ P]
  [inst_11 : Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  {σ₄₃ : R₄ →+* R₃} [inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [inst_15 : RingHomInvPair σ₃₄ σ₄₃] [inst_16 : RingHomInvPair σ₄₃ σ₃₄]
  (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P ≃ₛₗ[σ₃₄] Q), Function.Bijective ⇑f → Function.Bijective ⇑(f.compr₂ₛₗ ↑g)
-- Mathlib.Order.Sublattice
Sublattice.map_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β) (L M : Sublattice α),
  Sublattice.map f (L ⊔ M) = Sublattice.map f L ⊔ Sublattice.map f M
-- Mathlib.CategoryTheory.MorphismProperty.IsSmall
CategoryTheory.MorphismProperty.isSmall_iff_eq_ofHoms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W ↔ ∃ ι A B f, W = CategoryTheory.MorphismProperty.ofHoms f
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.instOneSubtype : {M : Type u_1} → [inst : MulOneClass M] → One { a // IsIdempotentElem a }
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.isZero_single_comp_eval : ∀ (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι)
  (j i : ι),
  i ≠ j → CategoryTheory.Limits.IsZero ((HomologicalComplex.single V c j).comp (HomologicalComplex.eval V c i))
-- Mathlib.LinearAlgebra.Ray
sameRay_smul_right_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {v : M} {r : R},
  SameRay R v (r • v) ↔ 0 ≤ r ∨ v = 0