mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Prelude
/-- Typed syntax, which tracks the potential kinds of the `Syntax` it contains.

While syntax quotations produce or expect `TSyntax` values of the correct kinds, this is not
otherwise enforced; it can easily be circumvented by direct use of the constructor.
 -/
Lean.TSyntax : Lean.SyntaxNodeKinds → Type
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_of_lt_of_le` -/
ssubset_of_ssubset_of_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b c : α}, a ⊂ b → b ⊆ c → a ⊂ c
-- Mathlib.Order.Partition.Basic
Partition.nonempty_of_mem : ∀ {α : Type u_1} {u t : Set α} {P : Partition u}, t ∈ P → t.Nonempty
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- If `d : D₁ W Z` corresponds to the data of `f : X ⟶ Y` satisfying `W` and
of a morphism `X ⟶ Z`, this is the object `X`.  -/
CategoryTheory.OrthogonalReflection.D₁.obj₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} → {Z : C} → CategoryTheory.OrthogonalReflection.D₁ W Z → C
-- Lean.Meta.Match.Basic
Lean.Meta.Match.congrEqn1ThmSuffix : String
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.trivial_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  (x x_1 : (CategoryTheory.PreZeroHypercover.singleton (CategoryTheory.CategoryStruct.id S)).I₀) (x_2 : PUnit.{w + 1}),
  (CategoryTheory.PreOneHypercover.trivial S).p₁ x_2 = CategoryTheory.CategoryStruct.id S
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.subtype_apply : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} [inst_4 : Nonempty ↥s] (p : ↥s), s.subtype p = ↑p
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
LinearMap.IsSymmetricProjection.hasOrthogonalProjection_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {p : E →ₗ[𝕜] E}, p.IsSymmetricProjection → p.range.HasOrthogonalProjection
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.away_fst : ∀ {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S], IsLocalization.Away (1, 0) R
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.forIn'_toList_eq_forIn' : ∀ {α : Type u} {r : Std.Rci α} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_5 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)},
  forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- **Alias** of the forward direction of `ContinuousLinearMap.IsIdempotentElem.range_mem_invtSubmodule_iff`.

---

`range f` is invariant under `T` if and only if `f ∘L T ∘L f = T ∘L f`,
for idempotent `f`.  -/
ContinuousLinearMap.IsIdempotentElem.conj_eq_of_range_mem_invtSubmodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f T : M →L[R] M},
  IsIdempotentElem f → (↑f).range ∈ Module.End.invtSubmodule ↑T → f ∘SL T ∘SL f = T ∘SL f
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.reflects_filtered_colimits : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D}
  [self : CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F] (J : Type w)
  [inst_2 : CategoryTheory.Category.{w', w} J] [CategoryTheory.IsFiltered J],
  CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [h : ProbabilityTheory.IsMarkovKernel κ], ProbabilityTheory.IsZeroOrMarkovKernel κ
-- Mathlib.LinearAlgebra.Ray
sameRay_neg_smul_left_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 (r • v) (-v) ↔ r ≤ 0 ∨ v = 0
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.isoTop_hom : ∀ {R : CommRingCat} (M : ModuleCat ↑R), (AlgebraicGeometry.tilde.isoTop M).hom = AlgebraicGeometry.tilde.toOpen M ⊤
-- Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
Lean.Grind.CommRing.Expr.denoteExpr : {M : Type → Type} →
  [Monad M] →
    [Lean.MonadError M] →
      [MonadLiftT Lean.MetaM M] →
        [Lean.Meta.Sym.Arith.MonadCanon M] →
          [Lean.Meta.Grind.Arith.CommRing.MonadRing M] → Lean.Meta.Grind.Arith.CommRing.RingExpr → M Lean.Expr
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.truncateToReal_eq_toReal : ∀ {t x : ENNReal}, t ≠ ⊤ → x ≤ t → t.truncateToReal x = x.toReal
-- Std.Data.HashSet.Lemmas
Std.HashSet.insertMany_nil : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α}, m.insertMany [] = m
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.takeWhile : Substring.Raw → (Char → Bool) → Substring.Raw
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSets.iIndepSet_of_mem : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {π : ι → Set (Set Ω)}
  {f : ι → Set Ω},
  (∀ (i : ι), f i ∈ π i) →
    (∀ (i : ι), MeasurableSet (f i)) → ProbabilityTheory.iIndepSets π μ → ProbabilityTheory.iIndepSet f μ
-- Mathlib.CategoryTheory.Limits.Types.Filtered
/-- Recognizing filtered colimits of types.  -/
CategoryTheory.Limits.Types.FilteredColimit.isColimitOf : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) →
      (t : CategoryTheory.Limits.Cocone F) →
        (∀ (x : t.pt), ∃ i xi, x = (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi) →
          (∀ (i j : J) (xi : (fun X => X) (F.obj i)) (xj : (fun X => X) (F.obj j)),
              (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi =
                  (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) xj →
                ∃ k f g,
                  (CategoryTheory.ConcreteCategory.hom (F.map f)) xi =
                    (CategoryTheory.ConcreteCategory.hom (F.map g)) xj) →
            CategoryTheory.Limits.IsColimit t
-- Mathlib.Condensed.Discrete.Colimit
/-- `isColimitLocallyConstantPresheaf` in the case of `S.asLimit`.  -/
Condensed.isColimitLocallyConstantPresheafDiagram : (X : Type (u + 1)) →
  (S : Profinite) → CategoryTheory.Limits.IsColimit ((Condensed.locallyConstantPresheaf X).mapCocone S.asLimitCone.op)
-- Mathlib.Data.QPF.Univariate.Basic
/-- maps every element of the W type to a canonical representative  -/
QPF.Wrepr : {F : Type u → Type v} → [q : QPF F] → (QPF.P F).W → (QPF.P F).W
-- Init.Data.List.ToArray
Array.findSome?.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → Option β) (as : Array α),
  Array.findSome? f as = (Array.findSomeM? (fun x => pure (f x)) as).run
-- Init.Data.UInt.Lemmas
UInt32.ofNat_uInt16ToNat : ∀ (n : UInt16), UInt32.ofNat n.toNat = n.toUInt32
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- Given a cocone `c` over `F`, we can interpret the legs of `c` as costructured arrows
`F.obj - ⟶ c.pt`.  -/
CategoryTheory.Limits.Cocone.toCostructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) → CategoryTheory.Functor J (CategoryTheory.CostructuredArrow F c.pt)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.X_ne_zero : ∀ {K : Type u} [inst : Field K], RatFunc.X ≠ 0
-- Mathlib.Topology.Convenient.OpenClosed
IsClosed.isGeneratedBy : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_3}
  [inst_1 : TopologicalSpace Y] [∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), Topology.IsGeneratedBy X ↥F]
  [Topology.IsGeneratedBy X Y] {F : Set Y}, IsClosed F → Topology.IsGeneratedBy X ↑F
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.mkHomFromDouble_f₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} {f : X₀ ⟶ X₁} {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (h : i₀ ≠ i₁) {K : HomologicalComplex C c} (φ₀ : X₀ ⟶ K.X i₀) (φ₁ : X₁ ⟶ K.X i₁)
  (comm : CategoryTheory.CategoryStruct.comp φ₀ (K.d i₀ i₁) = CategoryTheory.CategoryStruct.comp f φ₁)
  (hφ : ∀ (k : ι), c.Rel i₁ k → CategoryTheory.CategoryStruct.comp φ₁ (K.d i₁ k) = 0) {Z : C} (h_1 : K.X i₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HomologicalComplex.mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ).f i₁) h_1 =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.doubleXIso₁ f hi₀₁ h).hom
      (CategoryTheory.CategoryStruct.comp φ₁ h_1)
-- Mathlib.Data.Set.Card
Set.ncard_pair : ∀ {α : Type u_1} {a b : α}, a ≠ b → {a, b}.ncard = 2
-- Std.Time.Date.Unit.Week
/-- Convert `Week.Offset` into `Day.Offset`.
 -/
Std.Time.Week.Offset.toDays : Std.Time.Week.Offset → Std.Time.Day.Offset
-- Mathlib.Topology.Order.OrderClosed
instSeparableSpaceOrderDual : ∀ {α : Type u} [inst : TopologicalSpace α] [h : TopologicalSpace.SeparableSpace α], TopologicalSpace.SeparableSpace αᵒᵈ
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.tmulEquivDep.eq_1 : ∀ {ι : Type u_1} {ι₂ : Type u_2} (R : Type u_4) [inst : CommSemiring R] (N : ι ⊕ ι₂ → Type u_12)
  [inst_1 : (i : ι ⊕ ι₂) → AddCommMonoid (N i)] [inst_2 : (i : ι ⊕ ι₂) → Module R (N i)],
  PiTensorProduct.tmulEquivDep R N =
    LinearEquiv.ofLinearMap
      (TensorProduct.lift
        {
          toFun := fun a =>
            PiTensorProduct.lift ((PiTensorProduct.lift (MultilinearMap.currySumEquiv (PiTensorProduct.tprod R))) a),
          map_add' := ⋯, map_smul' := ⋯ })
      (PiTensorProduct.lift ((PiTensorProduct.tprod R).domCoprodDep (PiTensorProduct.tprod R))) ⋯ ⋯
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.IsSplittingField.splittingField : ∀ {K : Type v} [inst : Field K] (f : Polynomial K), Polynomial.IsSplittingField K f.SplittingField f
-- Init.Data.BitVec.Bootstrap
_private.Init.Data.BitVec.Bootstrap.0.BitVec.lt_two_pow_of_le : ∀ {x m n : ℕ}, x < 2 ^ m → m ≤ n → x < 2 ^ n
-- Init.Data.UInt.Lemmas
USize.ofNat_one : USize.ofNat 1 = 1
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.not_strictAnti_of_isArtinianObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.IsArtinianObject X]
  (f : ℕ → CategoryTheory.Subobject X), ¬StrictAnti f
-- Lean.Parser.Term
Lean.Parser.Term.structInstFieldEqns : Lean.Parser.Parser
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instIsTopologicalAddGroup : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F], IsTopologicalAddGroup (ContinuousMultilinearMap 𝕜 E F)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_adj : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (H : G.Subgraph) (a a_1 : W),
  (SimpleGraph.Subgraph.map f H).Adj a a_1 = Relation.Map H.Adj (⇑f) (⇑f) a a_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.toArray_insert_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ {k : α}, (t.insert k).toArray.Perm (if k ∈ t then t.toArray else t.toArray.push k)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.le_of_add_le_add_left : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [inst_1 : LE α] [AddLeftReflectLE α], x ≠ ⊥ → x + y ≤ x + z → y ≤ z
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendMap_add : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {K L : HomologicalComplex C c} (φ φ' : K ⟶ L) (e : c.Embedding c'),
  HomologicalComplex.extendMap (φ + φ') e = HomologicalComplex.extendMap φ e + HomologicalComplex.extendMap φ' e
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.pp : Lean.Meta.Grind.Arith.Cutsat.UnsatProof → Lean.Meta.Grind.GoalM Lean.MessageData
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- Assuming `trList v` is on the front of stack `k`, remove it, and push `v.headI` onto `main`.
See the section documentation.  -/
Turing.PartrecToTM2.head : Turing.PartrecToTM2.K' → Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Lean.Meta.Tactic.Grind.Types
/-- `e` is an implication and we want to split on its antecedent.  -/
Lean.Meta.Grind.SplitInfo.imp : (e : Lean.Expr) → e.isForall = true → Lean.Meta.Grind.SplitSource → Lean.Meta.Grind.SplitInfo
-- Mathlib.Order.Hom.Bounded
BotHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Bot α] [inst_1 : Bot β] [inst_2 : Bot γ] (f : BotHom β γ)
  (g : BotHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.CategoryTheory.Bicategory.Coherence
_private.Mathlib.CategoryTheory.Bicategory.Coherence.0.CategoryTheory.FreeBicategory.inclusionPathAux.match_1.eq_2 : ∀ {B : Type u_2} [inst : Quiver B] {a : B} (motive : (x : B) → Quiver.Path a x → Sort u_3) (x b : B)
  (p : Quiver.Path a b) (f : b ⟶ x) (h_1 : Unit → motive a Quiver.Path.nil)
  (h_2 : (x b : B) → (p : Quiver.Path a b) → (f : b ⟶ x) → motive x (p.cons f)),
  (match x, p.cons f with
    | .(a), Quiver.Path.nil => h_1 ()
    | x, p.cons f => h_2 x b p f) =
    h_2 x b p f
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerRight_id_symm : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  η =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b))
        (CategoryTheory.Bicategory.rightUnitor g).hom)
-- Mathlib.SetTheory.ZFC.Basic
/-- Turns a definable function into an n-ary `PSet` function.  -/
ZFSet.Definable.out : {n : ℕ} → (f : (Fin n → ZFSet.{u}) → ZFSet.{u}) → [self : ZFSet.Definable n f] → (Fin n → PSet.{u}) → PSet.{u}
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.ins.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.hasForgetToAddCommMonCat : CategoryTheory.HasForget₂ CommRingCat CommSemiRingCat
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- Alternative constructor for `IsStableUnderBaseChange`.  -/
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} [P.RespectsIso],
  (∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback f g],
      P g → P (CategoryTheory.Limits.pullback.fst f g)) →
    P.IsStableUnderBaseChange
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.ite_ne_zero : ∀ {α : Type u_1} [inst : Zero α] (p : Prop) [inst_1 : Decidable p] {a b : α}, a ≠ 0 → b ≠ 0 → (if p then a else b) ≠ 0
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.mapArrow_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : CategoryTheory.Arrow C} (f : X ⟶ Y),
  F.mapArrow.map f =
    CategoryTheory.Arrow.homMk (F.map (CategoryTheory.Arrow.Hom.left f)) (F.map (CategoryTheory.Arrow.Hom.right f)) ⋯
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instRepr.eq_1 : ∀ {α : Type u} [inst : AddMonoid α] [inst_1 : Repr α], AddUnits.instRepr = { reprPrec := reprPrec ∘ AddUnits.val }
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.union_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ m₃ m₄ : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∪ m₂).Equiv (m₃ ∪ m₄)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.of_dist_le' : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {K : ℝ},
  (∀ (x y : α), dist (f x) (f y) ≤ K * dist x y) → LipschitzWith K.toNNReal f
-- Lean.Server.References
/-- No ilean files, no information from workers.  -/
Lean.Server.References.empty : Lean.Server.References
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.id_preservesLimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₁, u₁, u₁} (CategoryTheory.Functor.id C)
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyonedaType_map_app : ∀ {X Y : Type uᵒᵖ} (f : X ⟶ Y) (N : AddCommMonCat),
  (AddCommMonCat.coyonedaType.map f).app N =
    AddCommMonCat.ofHom
      (AddMonoidHom.pi fun i => Pi.evalAddMonoidHom (fun a => ↑N) ((CategoryTheory.ConcreteCategory.hom f.unop) i))
-- Mathlib.Algebra.BigOperators.Finprod
/-- The sum of `f y` over `y ∈ g '' s` equals the sum of `f (g i)` over `s` provided that
`g` is injective on `s`.  -/
finsum_mem_image : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set β} {g : β → α},
  Set.InjOn g s → ∑ᶠ (i : α) (_ : i ∈ g '' s), f i = ∑ᶠ (j : β) (_ : j ∈ s), f (g j)
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.instHasAffinePropertyIsAffineHomIsAffine : AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsAffineHom fun X x x_1 x_2 => AlgebraicGeometry.IsAffine X
-- Init.Data.List.Lemmas
List.getLast?_eq_some_getLast : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.getLast? = some (l.getLast h)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.instCoeOut : {X : SSet} → CoeOut X.Subcomplex SSet
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.isOpen : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α} (U : TopologicalSpace.OpenNhdsOf x), IsOpen ↑U
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- For a function on `ℝ`, the Laplacian is the second derivative: version within a set.  -/
InnerProductSpace.laplacianWithin_eq_iteratedDerivWithin_real : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {e : ℝ} {s : Set ℝ} (f : ℝ → F),
  UniqueDiffOn ℝ s → e ∈ s → InnerProductSpace.laplacianWithin f s e = iteratedDerivWithin 2 f s e
-- ImportGraph.Tools.FindHome
GoToModuleLinkProps.mk.sizeOf_spec : ∀ (modName : Lean.Name), sizeOf { modName := modName } = 1 + sizeOf modName
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIoc_zero_coe_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜] {p : 𝕜}
  [hp : Fact (0 < p)] [inst_3 : Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜}, x ∈ Set.Ioc 0 p → AddCircle.liftIoc p 0 f ↑x = f x
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {n : ℕ} {N : Submodule R M} (snf : Module.Basis.SmithNormalForm N ι n) (m : ↥N) {i : Fin n},
  (snf.bM.repr ↑m) (snf.f i) = (snf.bN.repr (snf.a i • m)) i
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_iUnion : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅),
  m ∅ P0 = 0 →
    ∀ (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
      (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
          Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
        ∀ {β : Type u_2} [Countable β] {f : β → Set α},
          Pairwise (Function.onFun Disjoint f) →
            (∀ (i : β), P (f i)) → MeasureTheory.extend m (⋃ i, f i) = ∑' (i : β), MeasureTheory.extend m (f i)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  (h : (CategoryTheory.MorphismProperty.isomorphisms C).TransfiniteCompositionOfShape J f), CategoryTheory.IsIso f
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Ioc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (Set.Ioc a b)⁻¹ = Set.Ico b⁻¹ a⁻¹
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_obj_mor₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2),
  (X.ω₂.obj j).mor₂ =
    X.ω₁.map
      (CategoryTheory.ComposableArrows.homMk₁ (j.map (CategoryTheory.homOfLE ⋯))
        (CategoryTheory.CategoryStruct.id (j.obj ⟨2, ⋯⟩)) ⋯)
-- Mathlib.Algebra.Algebra.Hom
Algebra.ext_id_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {f g : R →ₐ[R] A},
  f = g ↔ True
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- `map₂` is invariant under isomorphisms.  -/
CategoryTheory.CostructuredArrow.map₂Congr : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {S : CategoryTheory.Functor C D} →
            {A : Type u₃} →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                {B : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] →
                    {U : CategoryTheory.Functor A B} →
                      {V : B} →
                        {F : CategoryTheory.Functor C A} →
                          {G : CategoryTheory.Functor D B} →
                            (α : F.comp U ⟶ S.comp G) →
                              (β : G.obj T ⟶ V) →
                                {F' : CategoryTheory.Functor C A} →
                                  {G' : CategoryTheory.Functor D B} →
                                    (e₁ : F ≅ F') →
                                      (e₂ : G ≅ G') →
                                        (α' : F'.comp U ⟶ S.comp G') →
                                          (β' : G'.obj T ⟶ V) →
                                            CategoryTheory.CategoryStruct.comp α (S.whiskerLeft e₂.hom) =
                                                CategoryTheory.CategoryStruct.comp
                                                  (CategoryTheory.Functor.whiskerRight e₁.hom U) α' →
                                              β = CategoryTheory.CategoryStruct.comp (e₂.hom.app T) β' →
                                                (CategoryTheory.CostructuredArrow.map₂ α β ≅
                                                  CategoryTheory.CostructuredArrow.map₂ α' β')