mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mk.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (hom hom_1 : (i j : ι) → C.X i ⟶ D.X j)
  (e_hom : hom = hom_1) (zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0)
  (comm : ∀ (i : ι), f.f i = (dNext i) hom + (prevD i) hom + g.f i),
  { hom := hom, zero := zero, comm := comm } = { hom := hom_1, zero := ⋯, comm := ⋯ }
-- Mathlib.CategoryTheory.Pi.Basic
/-- The equivalences given by `Pi.eqToEquivalence` are compatible with reindexing.  -/
CategoryTheory.Pi.eqToEquivalenceFunctorIso : {I : Type w₀} →
  {J : Type w₁} →
    (C : I → Type u₁) →
      [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
        (f : J → I) →
          {i' j' : J} →
            (h : i' = j') →
              (CategoryTheory.Pi.eqToEquivalence C ⋯).functor ≅
                (CategoryTheory.Pi.eqToEquivalence (fun i' => C (f i')) h).functor
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.induction_on₂ : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → AddLocalization S → Prop}
  (x y : AddLocalization S), (∀ (x y : M × ↥S), p (AddLocalization.mk x.1 x.2) (AddLocalization.mk y.1 y.2)) → p x y
-- Mathlib.Order.Bounds.Image
/-- See also `Monotone.map_bddAbove`.  -/
BddAbove.image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → BddAbove s → BddAbove t → BddAbove (Set.image2 f s t)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_lt_of_forall_lt_add : ∀ (f : CircleDeg1Lift), Continuous ⇑f → ∀ {z : ℝ}, (∀ (x : ℝ), f x < x + z) → f.translationNumber < z
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
LinearMap.IsSymmetric.subsingleton_of_no_eigenvalue_finiteDimensional : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E}, T.IsSymmetric → (∀ (μ : 𝕜), Module.End.eigenspace T μ = ⊥) → Subsingleton E
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.naturality_whiskerLeft : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {p : a ⟶ b} {f : b ⟶ c} {g h : c ⟶ d} {pf : a ⟶ c}
  {pfg : a ⟶ d} {η : g ≅ h} (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf)
  (η_fg : CategoryTheory.CategoryStruct.comp pf g ≅ pfg) (η_fh : CategoryTheory.CategoryStruct.comp pf h ≅ pfg),
  CategoryTheory.Bicategory.whiskerLeftIso pf η ≪≫ η_fh = η_fg →
    CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.whiskerLeftIso f η) ≪≫
        Mathlib.Tactic.Bicategory.normalizeIsoComp η_f η_fh =
      Mathlib.Tactic.Bicategory.normalizeIsoComp η_f η_fg
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.PendingSolverPropagations : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKey!_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {l : List α} {k : α},
  k ∈ m → (Std.DHashMap.Const.insertManyIfNewUnit m l).getKey! k = m.getKey! k
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyEq.isLocalExtr_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f g : α → β} {a : α},
  f =ᶠ[nhds a] g → (IsLocalExtr f a ↔ IsLocalExtr g a)
-- ProofWidgets.Component.RefreshComponent
/-- A `RefreshToken` allows you to manage a `RefreshComponent` instance.

Use `RefreshToken.update` to update the HTML currently on display.
Use `RefreshToken.cancelTk` to check if the instance has been discarded.  -/
ProofWidgets.RefreshToken : Type
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.loadImportedModule : {α : Type} →
  Lean.Core.Context →
    Lean.Environment →
      (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
        Lean.Meta.LazyDiscrTree.ImportData →
          IO.Ref Lean.Meta.LazyDiscrTree.Cache →
            Lean.Meta.LazyDiscrTree.PreDiscrTree α →
              Lean.Name → Lean.ModuleData → optParam ℕ 0 → BaseIO (Lean.Meta.LazyDiscrTree.PreDiscrTree α)
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
dist_le_pi_dist : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  (f g : (b : β) → X b) (b : β), dist (f b) (g b) ≤ dist f g
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_zero_apply : ∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] (f : R →+* S₂)
  (p : MvPolynomial σ R), (MvPolynomial.eval₂Hom f 0) p = f (MvPolynomial.constantCoeff p)
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.commutes : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (f : 𝒜 →ₐᵍ[R] ℬ)
  (r : R), f ((algebraMap R A) r) = (algebraMap R B) r
-- Mathlib.Util.Export
Lean.Export.exportName : Lean.Name → Lean.ExportM ℕ
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.isPartial_extendFun : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M} (hx : x ∉ (↑f).domain),
  HahnEmbedding.IsPartial seed (f.extendFun hx)
-- Init.Data.List.Pairwise
List.nodup_cons : ∀ {α : Type u_1} {a : α} {l : List α}, (a :: l).Nodup ↔ a ∉ l ∧ l.Nodup
-- Std.Http.Data.Version
Std.Http.Version.v10.sizeOf_spec : sizeOf Std.Http.Version.v10 = 1
-- Mathlib.Topology.Order.Lattice
ContinuousAt.finset_sup_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [inst_3 : OrderBot L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {x : X},
  (∀ i ∈ s, ContinuousAt (f i) x) → ContinuousAt (fun a => s.sup fun x => f x a) x
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- The **Binomial Inverse Theorem** (`⅟` version).

See `Matrix.invOf_add_mul_mul` for the Woodbury identity.  -/
Matrix.invOf_add_mul_mul' : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] [inst_4 : Ring α] (A : Matrix n n α) (U : Matrix n m α) (C : Matrix m m α) (V : Matrix m n α)
  [inst_5 : Invertible A] [inst_6 : Invertible (C + C * V * ⅟A * U * C)] [inst_7 : Invertible (A + U * C * V)],
  ⅟(A + U * C * V) = ⅟A - ⅟A * U * C * ⅟(C + C * V * ⅟A * U * C) * C * V * ⅟A
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates finite colimits, then `F.leftOp : Cᵒᵖ ⥤ D` creates finite
limits.  -/
CategoryTheory.Limits.createsFiniteLimitsLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteColimits F] → CategoryTheory.Limits.CreatesFiniteLimits F.leftOp
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The proposition that the function preserves multiplication  -/
MulEquiv.map_mul' : ∀ {M : Type u_9} {N : Type u_10} [inst : Mul M] [inst_1 : Mul N] (self : M ≃* N) (x y : M),
  self.toFun (x * y) = self.toFun x * self.toFun y
-- Init.Data.AC
Lean.Data.AC.removeNeutrals.loop : {α : Sort u_1} → [info : Lean.Data.AC.ContextInformation α] → α → List ℕ → List ℕ
-- Mathlib.CategoryTheory.RepresentedBy
/-- A presheaf `F` is represented by `X` with universal element `x : F.obj X`
if the natural transformation `yoneda.obj X ⟶ F` induced by `x` is an isomorphism.
For better universe generality, we state this manually as for every `Y`, the
induced map `(Y ⟶ X) → F.obj Y` is bijective.
 -/
CategoryTheory.Functor.IsRepresentedBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type w)) → {X : C} → F.obj (Opposite.op X) → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetry_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [F.Faithful] {Z : C} (h : a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (CategoryTheory.CategoryStruct.comp (hg.fst' f') h) =
    CategoryTheory.CategoryStruct.comp (hf'.snd g) h
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_insertList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k toInsert = false →
    Std.Internal.List.getEntry? k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getEntry? k l
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
_private.Mathlib.Analysis.CStarAlgebra.CStarMatrix.0.CStarMatrix.antilipschitzWith_toMatrixAux : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalCStarAlgebra A] [inst_3 : PartialOrder A] [inst_4 : StarOrderedRing A],
  AntilipschitzWith (↑(Fintype.card n) * ↑(Fintype.card m)) ⇑CStarMatrix.ofMatrixₗ.symm
-- Init.Data.UInt.Lemmas
USize.toUInt16_ofBitVec : ∀ (b : BitVec System.Platform.numBits), { toBitVec := b }.toUInt16 = { toBitVec := BitVec.setWidth 16 b }
-- Init.Data.SInt.Lemmas
Int64.toNatClampNeg_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofInt n).toNatClampNeg = n.toNat
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
/-- The roots of `g.fixpointPolynomial` are the fixed points of `g ∈ GL(2, K)` acting on the finite
part of `OnePoint K`.

See also `gl_smul_eq_self_iff_quadratic` for a similar lemma
about the fixed points of the action of `GL(2, ℝ)` on the upper half-plane.  -/
Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq K] {c : K} {g : GL (Fin 2) K},
  (Polynomial.aeval c) g.fixpointPolynomial = 0 ↔ g • ↑c = ↑c
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- `L₃.X₃` is the cokernel of `v₁₂.τ₃ : L₁.X₃ ⟶ L₂.X₃`.  -/
CategoryTheory.ShortComplex.SnakeInput.h₃τ₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (S : CategoryTheory.ShortComplex.SnakeInput C) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.v₂₃.τ₃ ⋯)
-- Mathlib.Logic.Unique
/-- `Unique α` expresses that `α` is a type with a unique term `default`.

This is implemented as a type, rather than a `Prop`-valued predicate,
for good definitional properties of the default term.  -/
Unique : Sort u → Sort (max 1 u)
-- Mathlib.Algebra.Group.Subgroup.Defs
HasMemOrNegMem.mem_of_neg_notMem : ∀ {S : Type u_3} {G : Type u_4} [inst : Neg G] [inst_1 : SetLike S G] (s : S) [HasMemOrNegMem s] (x : G), -x ∉ s → x ∈ s
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.pi_bot : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)], (Subgroup.pi Set.univ fun i => ⊥) = ⊥
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.add_neg_eq_iff_eq_add : ∀ {α : Type u} [inst : AddMonoid α] (b : AddUnits α) {a c : α}, a + ↑(-b) = c ↔ a = c + ↑b
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.dual : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β},
  StrictConcaveOn 𝕜 s f → StrictConvexOn 𝕜 s (⇑OrderDual.toDual ∘ f)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
/-- The function `fun (x, y) => x ^ y` is infinitely smooth at `(x, y)` unless `x = 0`.  -/
Real.contDiffAt_rpow_of_ne : ∀ (p : ℝ × ℝ), p.1 ≠ 0 → ∀ {n : WithTop ℕ∞}, ContDiffAt ℝ n (fun p => p.1 ^ p.2) p