mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      {Φ : CategoryTheory.SmallObject.SuccStruct C} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] →
                [inst_5 : WellFoundedLT J] →
                  {j : J} →
                    (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
                      F.obj ⟨⊥, ⋯⟩ = Φ.X₀ →
                        (∀ (i : J) (hi : i < j),
                            CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi = Φ.toSuccArrow (F.obj ⟨i, ⋯⟩)) →
                          (∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
                              CategoryTheory.SmallObject.SuccStruct.arrowMap F k i ⋯ hij =
                                CategoryTheory.SmallObject.SuccStruct.arrowι
                                  (CategoryTheory.SmallObject.restrictionLT F hij) hi k hk) →
                            Φ.Iteration j
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.val_ofCard : ∀ {α : Type u_1} {n : ℕ} {s : Finset α} (s_card : s.card = n), ↑(Set.powersetCard.ofCard s_card) = s
-- Mathlib.Topology.Algebra.Group.Basic
continuousInv_iInf : ∀ {G : Type w} {ι' : Sort u_1} [inst : Inv G] {ts' : ι' → TopologicalSpace G},
  (∀ (i : ι'), ContinuousInv G) → ContinuousInv G
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.unop_intCast : ∀ {R : Type u_1} [inst : IntCast R] (n : ℤ), MulOpposite.unop ↑n = ↑n
-- Plausible.Testable
Plausible.TestResult.isFailure : {p : Prop} → Plausible.TestResult p → Bool
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Cones over `diagram U ⋙ F` are the same as a cones over the usual sheaf condition equalizer diagram.
 -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F) ≌
                CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)
-- Mathlib.Algebra.Notation.Prod
Prod.instZero : {M : Type u_3} → {N : Type u_4} → [Zero M] → [Zero N] → Zero (M × N)
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.isDeniedPremise : Lean.Environment → Lean.Name → optParam Bool false → Bool
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.or_right_comm : ∀ (x y z : ℕ), x ||| y ||| z = x ||| z ||| y
-- Lean.Data.Lsp.Basic
Lean.Lsp.VersionedTextDocumentIdentifier : Type
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.canonical_K : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology],
  (CategoryTheory.ShortComplex.LeftHomologyData.canonical S).K = S.cycles
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.trans_refl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  (h : Diffeomorph I I' M M' n), h.trans (Diffeomorph.refl I' M' n) = h
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, returning `none` if no such key exists.
 -/
Std.ExtDTreeMap.getKeyLE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Option α
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a `k`-linear `G`-representation `(A, ρ)` and a type `α`, this is the linear equivalence
`(A ⊗ (α →₀ k[G]))_G ≃ₗ[k] (α →₀ A)` sending
`⟦a ⊗ single x (single g r)⟧ ↦ single x (r • ρ(g⁻¹)(a)).`  -/
Rep.coinvariantsTensorFreeLEquiv : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        (α : Type u) →
          [DecidableEq α] →
            (CategoryTheory.MonoidalCategoryStruct.tensorObj A (Rep.free k G α)).ρ.Coinvariants ≃ₗ[k] α →₀ ↑A
-- Mathlib.Data.Multiset.Defs
Multiset.notMem_mono : ∀ {α : Type u_1} {s t : Multiset α} {a : α}, s ⊆ t → a ∉ t → a ∉ s
-- Mathlib.LinearAlgebra.FreeAlgebra
/-- The `FreeMonoid X` basis on the `FreeAlgebra R X`,
mapping `[x₁, x₂, ..., xₙ]` to the "monomial" `1 • x₁ * x₂ * ⋯ * xₙ`  -/
FreeAlgebra.basisFreeMonoid : (R : Type u) → (X : Type v) → [inst : CommSemiring R] → Module.Basis (FreeMonoid X) R (FreeAlgebra R X)
-- Mathlib.Order.Antichain
IsAntichain.subset : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, IsAntichain r s → t ⊆ s → IsAntichain r t
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The associativity axiom associated to an algebra.  -/
CategoryTheory.Monad.Algebra.assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra),
  CategoryTheory.CategoryStruct.comp (T.μ.app self.A) self.a = CategoryTheory.CategoryStruct.comp (T.map self.a) self.a
-- Std.Http.Test.Helpers
Std.Http.Internal.Test.r417 : String
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.μ_δ : ∀ {G : Type v} [inst : Monoid G] (X Y : Action (Type w) G) {k : Type u} [inst_1 : CommSemiring k],
  (Representation.LinearizeMonoidal.μ X Y).comp (Representation.LinearizeMonoidal.δ X Y) =
    Representation.IntertwiningMap.id
      (Representation.linearize k G (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Preimages are respected by equivalence.  -/
PartialEquiv.EqOnSource.source_inter_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {e e' : PartialEquiv α β},
  e ≈ e' → ∀ (s : Set β), e.source ∩ ↑e ⁻¹' s = e'.source ∩ ↑e' ⁻¹' s
-- Mathlib.Order.Bounds.Basic
isLeast_singleton : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsLeast {a} a
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.Channel.mk.injEq : ∀ {α : Type} (inner inner_1 : Std.CloseableChannel α), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Topology.LocallyFinite
LocallyFinite.prod_left : ∀ {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {g : ι → Set Y}, LocallyFinite g → ∀ (f : ι → Set X), LocallyFinite fun i => f i ×ˢ g i
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey he ∈ t
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.coe_continuousLinearEquivAt_eq : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] {b : B}
  (hb : b ∈ e.baseSet),
  ⇑(Bundle.Trivialization.continuousLinearEquivAt R e b hb) = ⇑(Bundle.Trivialization.continuousLinearMapAt R e b)
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceInrOfIsStableUnderCobaseChangeTrivialCofibrationsOfCofibration : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [(HomotopicalAlgebra.trivialCofibrations C).IsStableUnderCobaseChange]
  [HomotopicalAlgebra.Cofibration f] [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_lift : ∀ {c : Cardinal.{u}}, Cardinal.toENat (Cardinal.lift.{v, u} c) = Cardinal.toENat c
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).max? = some (t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k')
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.orderIsoEquivIso_apply : ∀ {α β : PartOrdEmb} (e : α ≅ β), PartOrdEmb.orderIsoEquivIso e = PartOrdEmb.orderIsoOfIso e
-- Mathlib.Data.Finsupp.Single
Finsupp.single_eq_update : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] (a : α) (b : M),
  (⇑fun₀ | a => b) = Function.update 0 a b
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Addition version.  -/
Finset.ruzsa_triangle_inequality_add_add_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] (A B C : Finset G),
  (A + C).card * B.card ≤ (A + B).card * (B + C).card
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_div : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ] (f g : α →ₘ[μ] γ), ↑(f / g) =ᵐ[μ] ↑f / ↑g
-- Mathlib.Topology.Order.AtTopBotIxx
comap_coe_nhdsGT_of_Ioo_subset : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {s : Set X} {a : X},
  s ⊆ Set.Ioi a →
    (s.Nonempty → ∃ b > a, Set.Ioo a b ⊆ s) →
      autoParam (Order.IsPredPrelimit a) comap_coe_nhdsGT_of_Ioo_subset._auto_1 →
        Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot
-- Mathlib.Algebra.Group.Basic
mul_eq_of_eq_mul_inv : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a = c * b⁻¹ → a * b = c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.mk.injEq : ∀ {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] (fst : CategoryTheory.Functor X A) (snd : CategoryTheory.Functor X C)
  (iso : fst.comp F ≅ snd.comp G) (fst_1 : CategoryTheory.Functor X A) (snd_1 : CategoryTheory.Functor X C)
  (iso_1 : fst_1.comp F ≅ snd_1.comp G),
  ({ fst := fst, snd := snd, iso := iso } = { fst := fst_1, snd := snd_1, iso := iso_1 }) =
    (fst = fst_1 ∧ snd = snd_1 ∧ iso ≍ iso_1)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- `CliffordAlgebra.reverse` and `CliffordAlgebra.involute` commute. Note that the composition
is sometimes referred to as the "clifford conjugate".  -/
CliffordAlgebra.reverse_involute_commute : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, Function.Commute ⇑CliffordAlgebra.reverse ⇑CliffordAlgebra.involute
-- Lean.Level
_private.Lean.Level.0.Lean.Level.normLtAux.match_1.eq_2 : ∀ (motive : Lean.Level → ℕ → Lean.Level → ℕ → Sort u_1) (l₁ : Lean.Level) (k₁ : ℕ) (l₂ : Lean.Level) (k₂ : ℕ)
  (h_1 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁.succ k₁ l₂ k₂)
  (h_2 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂.succ k₂)
  (h_3 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.max l₁₂ →
        (k₁ : ℕ) → (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.max l₂₂ → (k₂ : ℕ) → motive (l₁₁.max l₁₂) k₁ (l₂₁.max l₂₂) k₂)
  (h_4 :
    (l₁ l₁₁ l₁₂ : Lean.Level) →
      l₁ = l₁₁.imax l₁₂ →
        (k₁ : ℕ) →
          (l₂ l₂₁ l₂₂ : Lean.Level) → l₂ = l₂₁.imax l₂₂ → (k₂ : ℕ) → motive (l₁₁.imax l₁₂) k₁ (l₂₁.imax l₂₂) k₂)
  (h_5 :
    (n₁ : Lean.Name) →
      (k₁ : ℕ) → (n₂ : Lean.Name) → (k₂ : ℕ) → motive (Lean.Level.param n₁) k₁ (Lean.Level.param n₂) k₂)
  (h_6 :
    (n₁ : Lean.LMVarId) →
      (k₁ : ℕ) → (n₂ : Lean.LMVarId) → (k₂ : ℕ) → motive (Lean.Level.mvar n₁) k₁ (Lean.Level.mvar n₂) k₂)
  (h_7 : (l₁ : Lean.Level) → (k₁ : ℕ) → (l₂ : Lean.Level) → (k₂ : ℕ) → motive l₁ k₁ l₂ k₂),
  (∀ (l₁_1 : Lean.Level), l₁ = l₁_1.succ → False) →
    (match l₁, k₁, l₂.succ, k₂ with
      | l₁.succ, k₁, l₂, k₂ => h_1 l₁ k₁ l₂ k₂
      | l₁, k₁, l₂.succ, k₂ => h_2 l₁ k₁ l₂ k₂
      | l₁@h:(l₁₁.max l₁₂), k₁, l₂@h_8:(l₂₁.max l₂₂), k₂ => h_3 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
      | l₁@h:(l₁₁.imax l₁₂), k₁, l₂@h_8:(l₂₁.imax l₂₂), k₂ => h_4 l₁ l₁₁ l₁₂ h k₁ l₂ l₂₁ l₂₂ h_8 k₂
      | Lean.Level.param n₁, k₁, Lean.Level.param n₂, k₂ => h_5 n₁ k₁ n₂ k₂
      | Lean.Level.mvar n₁, k₁, Lean.Level.mvar n₂, k₂ => h_6 n₁ k₁ n₂ k₂
      | l₁, k₁, l₂, k₂ => h_7 l₁ k₁ l₂ k₂) =
      h_2 l₁ k₁ l₂ k₂
-- Mathlib.Algebra.Group.Fin.Basic
Fin.lt_add_one_of_succ_lt : ∀ {n : ℕ} [inst : NeZero n] {a : Fin n}, ↑a + 1 < n → a < a + 1
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If `dist (f n) (f (n+1))` is bounded by `C * r^n`, `r < 1`, then `f` is a Cauchy sequence.
Note that this lemma does not assume `0 ≤ C` or `0 ≤ r`.  -/
cauchySeq_of_le_geometric : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (r C : ℝ) {f : ℕ → α},
  r < 1 → (∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) → CauchySeq f
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.tensorObj.match_1.eq_3 : ∀ (motive : AugmentedSimplexCategory → AugmentedSimplexCategory → Sort u_1) (x : AugmentedSimplexCategory)
  (h_1 : (m n : SimplexCategory) → motive (CategoryTheory.WithInitial.of m) (CategoryTheory.WithInitial.of n))
  (h_2 : (x : AugmentedSimplexCategory) → motive CategoryTheory.WithInitial.star x)
  (h_3 : (x : AugmentedSimplexCategory) → motive x CategoryTheory.WithInitial.star),
  (x = CategoryTheory.WithInitial.star → False) →
    (match x, CategoryTheory.WithInitial.star with
      | CategoryTheory.WithInitial.of m, CategoryTheory.WithInitial.of n => h_1 m n
      | CategoryTheory.WithInitial.star, x => h_2 x
      | x, CategoryTheory.WithInitial.star => h_3 x) =
      h_3 x
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderSubobjects : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsSerreClass], P.IsClosedUnderSubobjects
-- Mathlib.Order.RelSeries
/-- An alternative constructor of `LTSeries` from a strictly monotone function.  -/
LTSeries.mk : {α : Type u_1} → [inst : Preorder α] → (length : ℕ) → (toFun : Fin (length + 1) → α) → StrictMono toFun → LTSeries α
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : Inhabited α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {k : α}, k ∉ m₂ → (m₁ ∪ m₂).get! k = m₁.get! k
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.id.eq_1 : ∀ (α : Type u_2) [inst : InfSet α], sInfHom.id α = { toFun := id, map_sInf' := ⋯ }
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_smul_right : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) (r : NNReal),
  r ≠ 0 → μ.singularPart (r • ν) = μ.singularPart ν
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinite.mul : ∀ {x y : ℝ*}, x.Infinite → y.Infinite → (x * y).Infinite
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instSubsingletonOfIsEmpty : ∀ {α : Type u} [IsEmpty α], Subsingleton (WithZero α)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.whiskering`.

---

Whiskering on the left by `E : K ⥤ J` gives a functor from `Cocone F` to `Cocone (E ⋙ F)`.
 -/
CategoryTheory.Limits.Cocones.whiskering : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              (E : CategoryTheory.Functor K J) →
                CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone (E.comp F))
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.instIsZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.UniversallyOpen
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.Admissible.eq_1 : ∀ (pqr : Multiset ℕ+),
  ADEInequality.Admissible pqr =
    ((∃ q r, ADEInequality.A' q r = pqr) ∨
      (∃ r, ADEInequality.D' r = pqr) ∨ ADEInequality.E' 3 = pqr ∨ ADEInequality.E' 4 = pqr ∨ ADEInequality.E' 5 = pqr)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.ext_iff : ∀ {M : Type u_1} [inst : MulOneClass M] {s₁ s₂ : SaturatedSubmonoid M}, s₁ = s₂ ↔ s₁.toSubmonoid = s₂.toSubmonoid
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.instAlgebra : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → Algebra R (CliffordAlgebra Q)
-- Mathlib.Topology.Order
tendsto_nhds_true : ∀ {α : Type u_1} {l : Filter α} {p : α → Prop}, Filter.Tendsto p l (nhds True) ↔ ∀ᶠ (x : α) in l, p x
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- The function `a ↦ (condCDF ρ a).measure` is measurable.  -/
ProbabilityTheory.measurable_measure_condCDF : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)),
  Measurable fun a => (ProbabilityTheory.condCDF ρ a).measure
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If two functions coincide on a set `s`, then their iterated differentials within this set
coincide. See also `Filter.EventuallyEq.iteratedFDerivWithin_eq` and
`Filter.EventuallyEq.iteratedFDerivWithin`.  -/
Set.EqOn.iteratedFDerivWithin : ∀ {𝕜 : 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 : Set E}
  {f f₁ : E → F}, Set.EqOn f₁ f s → ∀ (n : ℕ), Set.EqOn (iteratedFDerivWithin 𝕜 n f₁ s) (iteratedFDerivWithin 𝕜 n f s) s
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
hasFDerivWithinAt_tangentCoordChange : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {x y z : M},
  z ∈ (extChartAt I x).source ∩ (extChartAt I y).source →
    HasFDerivWithinAt (↑(extChartAt I y) ∘ ↑(extChartAt I x).symm) (tangentCoordChange I x y z) (Set.range ↑I)
      (↑(extChartAt I x) z)
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
CategoryTheory.JointlyReflectIsomorphisms.shortExact_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [inst_2 : CategoryTheory.Abelian C] [inst_3 : (i : I) → CategoryTheory.Abelian (D i)]
      [CategoryTheory.CategoryWithHomology C] [inst_5 : ∀ (i : I), CategoryTheory.Limits.PreservesFiniteLimits (F i)]
      [∀ (i : I), CategoryTheory.Limits.PreservesFiniteColimits (F i)] (S : CategoryTheory.ShortComplex C),
      S.ShortExact ↔ ∀ (i : I), (S.map (F i)).ShortExact
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticCode.string.inj : ∀ {s s_1 : String}, Lean.Lsp.DiagnosticCode.string s = Lean.Lsp.DiagnosticCode.string s_1 → s = s_1
-- Std.Data.ExtHashSet.Basic
/-- Returns `true` if the hash set contains no elements.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
lawful, then it is possible that this function returns `false` even though `m.contains a = false`
for all `a`.
 -/
Std.ExtHashSet.isEmpty : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashSet α → Bool
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.sliceTo_cast : ∀ {s t : String.Slice} {hst : s.copy = t.copy} (p q : s.Pos) {h : q.cast hst ≤ p.cast hst},
  (p.cast hst).sliceTo (q.cast hst) h = (p.sliceTo q ⋯).cast ⋯
-- Init.Data.Nat.Lemmas
Nat.pos_of_mul_pos_left : ∀ {a b : ℕ}, 0 < a * b → 0 < b
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_mem_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k : α}, m.WF → k ∈ Std.HashMap.Raw.filter f m → k ∈ m
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.one_emod_eq_one : ∀ {a : ℤ}, a > 1 → 1 % a = 1
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_union_both : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ≤ b → Set.Ioo a b ∪ {a, b} = Set.Icc a b
-- Init.Data.Int.Linear
Int.Internal.Linear.not_le_norm_expr : ∀ (ctx : Int.Internal.Linear.Context) (lhs rhs : Int.Internal.Linear.Expr) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.not_le_norm_expr_cert lhs rhs p = true →
    ¬Int.Internal.Linear.Expr.denote ctx lhs ≤ Int.Internal.Linear.Expr.denote ctx rhs →
      Int.Internal.Linear.Poly.denote' ctx p ≤ 0
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
_private.Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas.0.ZMod.gauss_lemma_aux₁ : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {a : ℤ},
  ↑a ≠ 0 →
    ↑a ^ (p / 2) * ↑(p / 2).factorial =
      (-1) ^ {x ∈ Finset.Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}.card * ↑(p / 2).factorial
-- Mathlib.Order.Filter.Pointwise
Filter.map₂_sub : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α}, Filter.map₂ (fun x1 x2 => x1 - x2) f g = f - g
-- Lean.Elab.ConfigEval.Types
/-- Class for evaluation of `Term` syntax directly to a runtime value.
 -/
Lean.Elab.ConfigEval.EvalTerm : Type → Type
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instAddGroupWithOne : {k : Type u_1} → {G : Type u_2} → [inst : AddGroupWithOne k] → [One G] → AddGroupWithOne (SkewMonoidAlgebra k G)
-- Mathlib.Order.PFilter
Order.PFilter.nonempty : ∀ {P : Type u_1} [inst : Preorder P] (F : Order.PFilter P), (↑F).Nonempty
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- The congruence generated by `Rel`.  -/
DividedPowerAlgebra.ringCon : (R : Type u_2) →
  (M : Type u_3) →
    [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → RingCon (MvPolynomial (ℕ × M) R)
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.continuous_iff : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Z : Type v'} [inst_1 : TopologicalSpace Z]
  {T : Type v''} [inst_2 : TopologicalSpace T] {A : Type u_1} [inst_3 : TopologicalSpace A]
  {φ : A → Topology.ContinuousMapGeneratedBy X Z T},
  Continuous φ ↔ ∀ (i : ι) (f : C(X i, Z)), Continuous (Topology.ContinuousMapGeneratedBy.precomp f ∘ φ)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The linear isometry version of `TensorProduct.mapIncl`.  -/
TensorProduct.mapInclIsometry : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] →
                (E' : Submodule 𝕜 E) → (F' : Submodule 𝕜 F) → TensorProduct 𝕜 ↥E' ↥F' →ₗᵢ[𝕜] TensorProduct 𝕜 E F