mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableWithinAt_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_6} {F' : ι → Type u_7}
  [inst_1 : (i : ι) → NormedAddCommGroup (F' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (F' i)] (i : ι) (f : (i : ι) → F' i)
  (s' : Set ((i : ι) → F' i)), DifferentiableWithinAt 𝕜 (fun f => f i) s' f
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- All edges must be subsets of the vertex set  -/
Hypergraph.subset_vertexSet_of_mem_edgeSet' : ∀ {α : Type u_4} (self : Hypergraph α) ⦃e : Set α⦄, e ∈ self.edgeSet → e ⊆ self.vertexSet
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.wideCospan_map_term : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (CategoryTheory.Subobject A))
  (j : ↑(⇑(equivShrink (CategoryTheory.Subobject A)) '' s)),
  (CategoryTheory.Subobject.wideCospan s).map (CategoryTheory.Limits.WidePullbackShape.Hom.term j) =
    ((equivShrink (CategoryTheory.Subobject A)).symm ↑j).arrow
-- Mathlib.Analysis.Convex.Birkhoff
/-- If M is a scalar multiple of a doubly stochastic matrix, then it is a conical combination of
permutation matrices. This is most useful when M is a doubly stochastic matrix, in which case
the combination is convex.

This particular formulation is chosen to make the inductive step easier: we no longer need to
rescale each time a permutation matrix is subtracted.
 -/
_private.Mathlib.Analysis.Convex.Birkhoff.0.doublyStochastic_sum_perm_aux : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Field R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] (M : Matrix n n R) (s : R),
  0 ≤ s →
    (∃ M' ∈ doublyStochastic R n, M = s • M') →
      ∃ w, (∀ (σ : Equiv.Perm n), 0 ≤ w σ) ∧ ∑ σ, w σ • Equiv.Perm.permMatrix R σ = M
-- Mathlib.Data.Nat.ModEq
Nat.add_mod_add_of_le_add_mod : ∀ {a b c : ℕ}, c ≤ a % c + b % c → (a + b) % c + c = a % c + b % c
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.lift_apply' : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (F : M →* A) (f : MonoidAlgebra R M),
  ((MonoidAlgebra.lift R A M) F) f = f.coeff.sum fun a b => (algebraMap R A) b * F a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBicone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C}
  (b : CategoryTheory.Limits.Bicone f), (F.mapBicone b).pt = F.obj b.pt
-- Mathlib.Data.Subtype
/-- Restatement of `Subtype.mk.injEq` as an iff.  -/
Subtype.mk_eq_mk : ∀ {α : Sort u_1} {p : α → Prop} {a : α} {h : p a} {a' : α} {h' : p a'}, ⟨a, h⟩ = ⟨a', h'⟩ ↔ a = a'
-- Mathlib.Data.Set.Defs
Set.instEmptyCollection : {α : Type u} → EmptyCollection (Set α)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos : ∀ {c : ENNReal}, c ≠ ⊤ → ∀ {y : ℝ}, 0 < y → Filter.Tendsto (fun x => c * x ^ y) (nhds 0) (nhds 0)
-- Init.Data.Ord.Basic
compareOfLessAndEq_eq_eq : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [inst_2 : DecidableLT α] [DecidableLE α] [inst_4 : DecidableEq α],
  (∀ (x : α), x ≤ x) → (∀ {x y : α}, ¬x ≤ y ↔ y < x) → ∀ {x y : α}, compareOfLessAndEq x y = Ordering.eq ↔ x = y
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_Φ_le : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), (W.Φ n).natDegree ≤ n.natAbs ^ 2
-- Mathlib.Algebra.Ring.Prod
RingHom.coe_prodMap : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [inst : NonAssocSemiring R]
  [inst_1 : NonAssocSemiring S] [inst_2 : NonAssocSemiring R'] [inst_3 : NonAssocSemiring S'] (f : R →+* R')
  (g : S →+* S'), ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.Algebra.Homology.Bifunctor
/-- Given `K₁ : HomologicalComplex C₁ c₁`, `K₂ : HomologicalComplex C₂ c₂`,
a bifunctor `F : C₁ ⥤ C₂ ⥤ D` and a complex shape `ComplexShape J` such that we have
`[TotalComplexShape c₁ c₂ c]`, this `mapBifunctor K₁ K₂ F c : HomologicalComplex D c`
is the total complex of the bicomplex obtained by applying `F` to `K₁` and `K₂`.  -/
HomologicalComplex.mapBifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            (K₁ : HomologicalComplex C₁ c₁) →
                              (K₂ : HomologicalComplex C₂ c₂) →
                                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  [inst_6 : F.PreservesZeroMorphisms] →
                                    [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      (c : ComplexShape J) →
                                        [inst_8 : TotalComplexShape c₁ c₂ c] →
                                          [K₁.HasMapBifunctor K₂ F c] → [DecidableEq J] → HomologicalComplex D c
-- Mathlib.Data.Sym.Basic
Sym.coe_injective : ∀ {α : Type u_1} {n : ℕ}, Function.Injective Sym.toMultiset
-- Mathlib.Order.Interval.Set.Image
Monotone.mapsTo_Iic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  Monotone f → Set.MapsTo f (Set.Iic b) (Set.Iic (f b))
-- Mathlib.Data.Fin.Tuple.Finset
Fin.snoc_mem_piFinset_snoc : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {x_last : α (Fin.last n)} {x_init : (i : Fin n) → α i.castSucc}
  {s_last : Finset (α (Fin.last n))} {s_init : (i : Fin n) → Finset (α i.castSucc)},
  Fin.snoc x_init x_last ∈ Fintype.piFinset (Fin.snoc s_init s_last) ↔
    x_last ∈ s_last ∧ x_init ∈ Fintype.piFinset s_init
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.ext_iff : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] {f g : P →ᵃⁱ[𝕜] P₂}, f = g ↔ ∀ (x : P), f x = g x
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize Int16
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
Std.IterM.forIn_empty : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  [inst_2 : Monad n] [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n] {init : γ}
  {f : β → γ → n (ForInStep γ)}, forIn (Std.IterM.empty m β) init f = pure init
-- Mathlib.Algebra.Group.Subgroup.Lattice
Additive.mem_toAddSubgroup : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) (g : Additive G), g ∈ Subgroup.toAddSubgroup S ↔ Additive.toMul g ∈ S
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.of_subsingleton : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Subsingleton M], IsAdicComplete I M
-- Lean.Meta.Basic
Lean.Meta.SynthInstanceCacheKey.localInsts : Lean.Meta.SynthInstanceCacheKey → Lean.LocalInstances
-- Mathlib.Data.Finset.Basic
Equiv.Finset.disjUnionEquiv_symm_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (h : Disjoint s t) {i : α} (hi : i ∈ t)
  (hi' : i ∈ s.disjUnion t h), (Equiv.Finset.disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inr ⟨i, hi⟩
-- Mathlib.Data.Tree.Basic
BinaryTree.map.eq_2 : ∀ {α : Type u} {β : Type u_1} (f : α → β) (a : α) (l r : BinaryTree α),
  BinaryTree.map f (BinaryTree.node a l r) = BinaryTree.node (f a) (BinaryTree.map f l) (BinaryTree.map f r)
-- Mathlib.RingTheory.Coalgebra.TensorProduct
TensorProduct.comul_tmul : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid B] [inst_4 : Algebra R S] [inst_5 : Module R A]
  [inst_6 : Module S A] [inst_7 : Module R B] [inst_8 : IsScalarTower R S A] [inst_9 : CoalgebraStruct R B]
  [inst_10 : CoalgebraStruct S A] (x : A) (y : B),
  CoalgebraStruct.comul (x ⊗ₜ[R] y) =
    (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
      (CoalgebraStruct.comul x ⊗ₜ[R] CoalgebraStruct.comul y)
-- Mathlib.Algebra.Polynomial.Eval.Coeff
/-- **Alias** of the reverse direction of `Polynomial.zero_isRoot_iff_coeff_zero_eq_zero`. -/
Polynomial.zero_isRoot_of_coeff_zero_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.coeff 0 = 0 → p.IsRoot 0
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.num.inj : ∀ {k k_1 : ℤ}, Lean.Grind.CommRing.Expr.num k = Lean.Grind.CommRing.Expr.num k_1 → k = k_1
-- Mathlib.Tactic.Translate.Core
/-- The name that we are translating to.  -/
Mathlib.Tactic.Translate.TranslationInfo.translation : Mathlib.Tactic.Translate.TranslationInfo → Lean.Name
-- Batteries.Lean.PersistentHashSet
/-- Obtain a `PersistentHashSet` from a list.
 -/
Lean.PersistentHashSet.ofList : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → List α → Lean.PersistentHashSet α
-- Init.SimpLemmas
eq_false' : ∀ {p : Prop}, (p → False) → p = False
-- Std.Tactic.BVDecide.Syntax
/-- Handle equality on enum inductives by turning them into `BitVec`.
 -/
Lean.Elab.Tactic.BVDecide.BVDecideConfig.enums : Lean.Elab.Tactic.BVDecide.BVDecideConfig → Bool
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- a choice of a left adjoint to `R`  -/
CategoryTheory.Reflective.L : {C : Type u₁} →
  {D : Type u₂} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        (R : CategoryTheory.Functor D C) → [self : CategoryTheory.Reflective R] → CategoryTheory.Functor C D
-- Mathlib.MeasureTheory.Group.Action
/-- If measure `μ` is invariant under an additive group action and is nonzero on a compact set `K`,
then it is positive on any nonempty open set. In case of a regular measure, one can assume `μ ≠ 0`
instead of `μ K ≠ 0`, see `MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_ne_zero`.  -/
MeasureTheory.measure_isOpen_pos_of_vaddInvariant_of_compact_ne_zero : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {K U : Set α},
  IsCompact K → μ K ≠ 0 → IsOpen U → U.Nonempty → 0 < μ U
-- Mathlib.MeasureTheory.Measure.PreVariation
/-- The `VectorMeasure X ℝ≥0∞` built from a σ-subadditive function.  -/
MeasureTheory.ennrealPreVariation : {X : Type u_1} →
  [inst : MeasurableSpace X] →
    (f : Set X → ENNReal) → MeasureTheory.IsSigmaSubadditiveSetFun f → f ∅ = 0 → MeasureTheory.VectorMeasure X ENNReal
-- Mathlib.Order.KrullDimension
Order.le_krullDim_iff : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ}, ↑n ≤ Order.krullDim α ↔ ∃ l, l.length = n
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.topEquiv_symm_apply_coe : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (a : E),
  ↑(IntermediateField.topEquiv.symm a) = a
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
/-- Bijection between a subalgebra `S` and `MulOpposite` of its opposite.  -/
Subalgebra.algEquivOpMop : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → ↥S ≃ₐ[R] (↥S.op)ᵐᵒᵖ
-- Batteries.Util.ExtendedBinder
/-- A single (unparenthesized) binder, or a list of parenthesized binders  -/
Batteries.ExtendedBinder.extBinders : Lean.ParserDescr
-- Std.Sync.Broadcast
/-- Queue of consumers blocked waiting for new messages to be broadcast.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.waiters : {α : Type} → Std.Bounded.State✝ α → Std.Queue (Std.Broadcast.Consumer✝ α)
-- Init.Data.SInt.Lemmas
UInt16.toBitVec_toInt16 : ∀ (x : UInt16), x.toInt16.toBitVec = x.toBitVec
-- Mathlib.Data.PNat.Factors
/-- The number of occurrences of p in the factor multiset of m
is the same as the p-adic valuation of m.  -/
PNat.count_factorMultiset : ∀ (m : ℕ+) (p : Nat.Primes) (k : ℕ), ↑p ^ k ∣ m ↔ k ≤ Multiset.count p m.factorMultiset
-- Mathlib.Order.Filter.NAry
Filter.map₂_comm : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β} {n : β → α → γ},
  (∀ (a : α) (b : β), m a b = n b a) → Filter.map₂ m f g = Filter.map₂ n g f
-- Mathlib.Order.Ideal
Order.Ideal.mem_compl_of_ge : ∀ {P : Type u_1} [inst : LE P] {I : Order.Ideal P} {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_eventually_congr_set : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s t : Set E}
  {f : E → F} {x : E}, s =ᶠ[nhds x] t → ∀ (n : ℕ), iteratedFDerivWithin 𝕜 n f s =ᶠ[nhds x] iteratedFDerivWithin 𝕜 n f t
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.mk : {α : Type u} → Option α → Std.Rxi.Iterator α
-- Init.Data.Int.Lemmas
Int.eq_of_mul_eq_mul_right : ∀ {a b c : ℤ}, a ≠ 0 → b * a = c * a → b = c
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRight_isIso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c)
  [CategoryTheory.IsIso η], CategoryTheory.IsIso (CategoryTheory.Bicategory.whiskerRight η h)
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocSemiring.toMul : {α : Type u} → [self : NonUnitalNonAssocSemiring α] → Mul α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toArray_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.keys.toArray = t.keysArray
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂_fderiv.eq_1 : ∀ (z τ : ℂ), jacobiTheta₂_fderiv z τ = ∑' (n : ℤ), jacobiTheta₂_term_fderiv n z τ
-- Init.Prelude
Lean.Syntax.brecOn_2.go : {motive_1 : Lean.Syntax → Sort u} →
  {motive_2 : Array Lean.Syntax → Sort u} →
    {motive_3 : List Lean.Syntax → Sort u} →
      (t : List Lean.Syntax) →
        ((t : Lean.Syntax) → t.below → motive_1 t) →
          ((t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t) →
            ((t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t) → motive_3 t ×' Lean.Syntax.below_2 t
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.inj : Lean.Meta.Grind.ExtensionState → Lean.Meta.Grind.Theorems Lean.Meta.Grind.InjectiveTheorem
-- Mathlib.Logic.Lemmas
Prop.exists : ∀ {f : Prop → Prop}, (∃ p, f p) ↔ f True ∨ f False
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.mem_antidiagonal : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO} {a : α} {x : α × α}, x ∈ Finset.antidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 + x.2 = a
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- A distinguished subalgebra corresponding to a Cartan subalgebra of the Geck construction.

See also `RootPairing.GeckConstruction.cartanSubalgebra'`.  -/
RootPairing.GeckConstruction.cartanSubalgebra : {ι : 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} →
                    [P.IsCrystallographic] →
                      (b : P.Base) →
                        [inst_6 : Fintype ι] →
                          [inst_7 : DecidableEq ι] → LieSubalgebra R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafifyLift.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  {P Q : CategoryTheory.Functor Cᵒᵖ D} (η η_1 : P ⟶ Q),
  η = η_1 →
    ∀ (hQ : CategoryTheory.Presheaf.IsSheaf J Q),
      CategoryTheory.sheafifyLift J η hQ = CategoryTheory.sheafifyLift J η_1 hQ
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
/-- The localizer morphism (relative to quasi-isomorphisms) that is
given by the "inclusion functor"
`CochainComplex.Plus (InjectiveObject C) ⥤ CochainComplex.Plus C`.  -/
CochainComplex.Plus.localizerMorphism : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.LocalizerMorphism
        ((CochainComplex.Plus.quasiIso C).inverseImage (CategoryTheory.InjectiveObject.ι C).mapCochainComplexPlus)
        (CochainComplex.Plus.quasiIso C)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instFromJsonHashSet : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → [Lean.FromJson α] → Lean.FromJson (Std.HashSet α)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeConstantResult.mk : Option Lean.Language.SnapshotTree → Option Lean.Exception → Lean.Meta.RealizeConstantResult✝
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.eq_one : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E], ↑f c = 1
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Atom.mk.inj : ∀ {e : Lean.Expr} {src tgt : Mathlib.Tactic.BicategoryLike.Mor₁} {e_1 : Lean.Expr}
  {src_1 tgt_1 : Mathlib.Tactic.BicategoryLike.Mor₁},
  { e := e, src := src, tgt := tgt } = { e := e_1, src := src_1, tgt := tgt_1 } → e = e_1 ∧ src = src_1 ∧ tgt = tgt_1
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.Presieve.IsSheafFor.singleton_of_isRepresentable_of_effectiveEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.EffectiveEpi f]
  (F : CategoryTheory.Functor Cᵒᵖ (Type u_1)) [F.IsRepresentable],
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton f)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.of_mono_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Mono f], f = 0 → CategoryTheory.Limits.IsZero X
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `Section` is a right inverse to `S.rightHom`  -/
AddGroupExtension.Splitting.rightInverse_rightHom : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} (self : S.Splitting), Function.RightInverse (↑self.toAddMonoidHom).toFun ⇑S.rightHom
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.kextract.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (a : α) →
      (motive : Option (β a) × List (Sigma β) → Sort u_3) →
        (x : Option (β a) × List (Sigma β)) → ((b' : Option (β a)) → (l' : List (Sigma β)) → motive (b', l')) → motive x
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] [inst_1 : Preorder α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α]
  (s : NonemptyInterval α) (n : ℕ), (n • s).toProd.2 = n • s.toProd.2
-- Init.Data.UInt.Lemmas
UInt16.toFin_ofNat : ∀ (n : ℕ), (OfNat.ofNat n).toFin = OfNat.ofNat n
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_functor'_obj_obj : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X}
  (f :
    CategoryTheory.ObjectProperty.FullSubcategory fun f =>
      (CategoryTheory.Sieve.generate (TopCat.Presheaf.presieveOfCoveringAux U Y)).arrows f.hom),
  ((TopCat.Presheaf.generateEquivalenceOpensLe_functor' U).obj f).obj = f.obj.left
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffAt_id : ∀ {𝕜 : 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] {x : M} {n : WithTop ℕ∞}, ContMDiffAt I I n id x
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.right_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C),
  CategoryTheory.CategoryStruct.comp (self.δ.app X) (self.map (self.ε.app X)) =
    CategoryTheory.CategoryStruct.id (self.obj X)
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.trivialTo_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.Bimon C), A.trivialTo.hom = default
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.NormalizedHom.nil.sizeOf_spec : ∀ (e : Mathlib.Tactic.BicategoryLike.Mor₁) (a : Mathlib.Tactic.BicategoryLike.Obj),
  sizeOf (Mathlib.Tactic.BicategoryLike.NormalizedHom.nil e a) = 1 + sizeOf e + sizeOf a
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The range of a morphism of algebras is a fintype, if the domain is a fintype.

Note that this instance can cause a diamond with `Subtype.fintype` if `B` is also a fintype.  -/
AlgHom.fintypeRange : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R B] → [Fintype A] → [DecidableEq B] → (φ : A →ₐ[R] B) → Fintype ↥φ.range
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- **Alias** of `ContinuousLinearMapWOT.continuous_ofCLM`.

---

The weak operator topology is coarser than the bounded convergence topology, i.e. the inclusion
map is continuous.  -/
ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] [ContinuousSMul 𝕜₁ E], Continuous ContinuousLinearMapWOT.ofCLM
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- The maps `hσ' q n m hnm` are natural on the simplicial object  -/
AlgebraicTopology.DoldKan.hσ'_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q n m : ℕ)
  (hnm : AlgebraicTopology.DoldKan.c.Rel m n) {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) (AlgebraicTopology.DoldKan.hσ' q n m hnm) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.hσ' q n m hnm) (f.app (Opposite.op { len := m }))
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from variables to their denotations.  -/
Lean.Meta.Grind.Arith.Cutsat.State.vars : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray Lean.Expr