mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.coeff_of_coeff : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W] (f : Γ → V →ₗ[R] W)
  (hf : ∀ (x : V), (Function.support fun g => (f g) x).IsPWO), HVertexOperator.coeff (HVertexOperator.of_coeff f hf) = f
-- Mathlib.Algebra.Order.GroupWithZero.Lex
LinearOrderedCommGroupWithZero.inl_mul_inr_eq_coe_toLex : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedCommGroupWithZero α] [inst_1 : LinearOrderedCommGroupWithZero β]
  {m : α} {n : β} (hm : m ≠ 0) (hn : n ≠ 0),
  (LinearOrderedCommGroupWithZero.inl α β) m * (LinearOrderedCommGroupWithZero.inr α β) n =
    ↑(toLex (Units.mk0 m hm, Units.mk0 n hn))
-- Mathlib.Algebra.Category.Grp.Adjunctions
AddCommGrpCat.free_obj_coe : ∀ {α : Type u}, ↑(AddCommGrpCat.free.obj α) = FreeAbelianGroup α
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.instComp_id : ∀ {N : Type u_4} {P : Type u_5} [inst : Monoid N] [inst_1 : Monoid P] {φ : N →* N} [MonoidHom.CompTriple.IsId φ]
  {ψ : N →* P}, φ.CompTriple ψ ψ
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.mk_inv : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M} (ha : a ≠ 1),
  FiniteMulArchimedeanClass.mk a⁻¹ ⋯ = FiniteMulArchimedeanClass.mk a ha
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.uniformContinuousOn_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  {f : α → β} {g : β → γ} {S : Set α}, IsUniformInducing g → (UniformContinuousOn f S ↔ UniformContinuousOn (g ∘ f) S)
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.isClosedEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Topology.IsClosedEmbedding f
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The nonunits of a valuation subring of `K`, as a nonunital subring of `K`  -/
ValuationSubring.nonunits : {K : Type u} → [inst : Field K] → ValuationSubring K → NonUnitalSubring K
-- Lean.DocString.Extension
/-- An inline element with a deferred check. The `index` is a 0-based index into the current docstring's
deferred checks, in source order. Block and inline deferred elements share a counter.
 -/
Lean.Doc.Inline.deferred : ℕ → Array (Lean.Doc.Inline Lean.ElabInline) → Lean.Doc.Inline Lean.ElabInline
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.divMonomial.eq_1 : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (p : MvPolynomial σ R) (s : σ →₀ ℕ),
  p.divMonomial s = AddMonoidAlgebra.divOf p s
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Whether a given finset is 3GP-free is decidable.  -/
ThreeGPFree.instDecidable : {α : Type u_2} → [inst : Monoid α] → [DecidableEq α] → {s : Finset α} → Decidable (ThreeGPFree ↑s)
-- Mathlib.RingTheory.Int.Basic
Int.Prime.dvd_pow' : ∀ {n : ℤ} {k p : ℕ}, Nat.Prime p → ↑p ∣ n ^ k → ↑p ∣ n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The square `precomposeObjTransformOBjSquare` respects identities.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_id : ∀ {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} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁) (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CatCommSq.iso
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj (CategoryTheory.Functor.id X))
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj
            (CategoryTheory.Functor.id X))).hom
      (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).whiskerLeft
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F₁ G₁ X).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight
        (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId F G X).hom
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).leftUnitor.hom
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).rightUnitor.inv)
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Eta-expanded form of `MeromorphicOn.divisor_closedBall_comp_sub_const_eq_divisor_closedBall`

---

Divisors are invariant under translation, special case where the set is a closed ball.  -/
MeromorphicOn.divisor_closedBall_fun_comp_sub_const_eq_divisor_closedBall : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜} {R : ℝ} {f : 𝕜 → E},
  (MeromorphicOn.divisor (fun x => f (x - c)) (Metric.closedBall c R)) (z + c) =
    (MeromorphicOn.divisor f (Metric.closedBall 0 R)) z
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A version of `stronglyMeasurable_const` that assumes `f x = f y` for all `x, y`.
This version works for functions between empty types.  -/
MeasureTheory.stronglyMeasurable_const' : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {f : α → β} [inst : TopologicalSpace β],
  (∀ (x y : α), f x = f y) → MeasureTheory.StronglyMeasurable f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {fallback : β k}, k ∉ m₂ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_add : ∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] {p : α → Prop} [inst_1 : DecidablePred p] {v v' : α →₀ M},
  Finsupp.filter p (v + v') = Finsupp.filter p v + Finsupp.filter p v'
-- Mathlib.Algebra.Category.Ring.Basic
/-- Turn a morphism in `SemiRingCat` back into a `RingHom`.  -/
SemiRingCat.Hom.hom : {R S : SemiRingCat} → R.Hom S → ↑R →+* ↑S
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_15.splitter : (motive : Std.Tactic.BVDecide.BVUnOp → Sort u_1) →
  (op : Std.Tactic.BVDecide.BVUnOp) →
    (Unit → motive Std.Tactic.BVDecide.BVUnOp.not) →
      ((distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateLeft distance)) →
        ((distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.rotateRight distance)) →
          ((distance : ℕ) → motive (Std.Tactic.BVDecide.BVUnOp.arithShiftRightConst distance)) →
            (Unit → motive Std.Tactic.BVDecide.BVUnOp.reverse) →
              (Unit → motive Std.Tactic.BVDecide.BVUnOp.clz) →
                (Unit → motive Std.Tactic.BVDecide.BVUnOp.cpop) → motive op
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piOptionEquivProd_apply : ∀ {ι : Type u_7} {R : Option ι → Type u_8} [inst : (i : Option ι) → NonUnitalNonAssocSemiring (R i)]
  (f : (a : Option ι) → R a), RingEquiv.piOptionEquivProd f = (f none, fun a => f (some a))
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_inv_mul_iff_le : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b : α}, 1 ≤ b⁻¹ * a ↔ b ≤ a
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapCyclesIso_hom_iCycles : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasLeftHomology]
  [inst_6 : F.PreservesLeftHomologyOf S],
  CategoryTheory.CategoryStruct.comp (S.mapCyclesIso F).hom (F.map S.iCycles) = (S.map F).iCycles
-- Mathlib.Topology.Algebra.Group.Basic
IsTopologicalAddGroup.ext : ∀ {G : Type u_1} [inst : AddGroup G] {t t' : TopologicalSpace G},
  IsTopologicalAddGroup G → IsTopologicalAddGroup G → nhds 0 = nhds 0 → t = t'
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_inv_index : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] [inst_2 : DecidableEq ι]
  [inst_3 : InvolutiveInv ι] (s : Finset ι) (f : ι → M), (s⁻¹.expect fun i => f i) = s.expect fun i => f i⁻¹
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.emptyOn_indep_iff : ∀ {α : Type u_1} {I : Set α}, (Matroid.emptyOn α).Indep I ↔ I = ∅
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHomClass.mk : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : FunLike F α β] [toMulHomClass : MulHomClass F α β]
  [toAddMonoidHomClass : AddMonoidHomClass F α β], NonUnitalRingHomClass F α β
-- Mathlib.Order.Bounds.Basic
upperBounds_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, upperBounds (Set.Iic a) = Set.Ici a
-- Mathlib.LinearAlgebra.Trace
LinearMap.isNilpotent_trace_of_isNilpotent : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : M →ₗ[R] M},
  IsNilpotent f → IsNilpotent ((LinearMap.trace R M) f)
-- Mathlib.Data.TypeVec
/-- left projection of a `prod` vector  -/
TypeVec.prod.fst : {n : ℕ} → {α β : TypeVec.{u} n} → (α.prod β).Arrow α
-- Mathlib.Data.Finset.Prod
Finset.mk_mem_product : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {a : α} {b : β}, a ∈ s → b ∈ t → (a, b) ∈ s ×ˢ t
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_val : ∀ {α : Type u_2} {s t : Finset α}, Disjoint s.val t.val ↔ Disjoint s t
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.done : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Zipper α β
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkColEq.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.instEpiMap'KernelCokernelCompSequenceOfNatNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.Epi
    ((CategoryTheory.kernelCokernelCompSequence f g).map' 4 5
      CategoryTheory.instEpiMap'KernelCokernelCompSequenceOfNatNat._proof_2
      CategoryTheory.instEpiMap'KernelCokernelCompSequenceOfNatNat._proof_3)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_symm : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1),
  AffineMap.lineMap p₀ p₁ = (AffineMap.lineMap p₁ p₀).comp (AffineMap.lineMap 1 0)
-- Init.Data.Array.Count
Array.countP_true : ∀ {α : Type u_1}, (Array.countP fun x => true) = Array.size
-- Mathlib.GroupTheory.GroupAction.Hom
DistriMulActionHom.coe_zero : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_11}
  [inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_12} [inst_4 : AddMonoid B]
  [inst_5 : DistribMulAction N B], ⇑0 = 0
-- Mathlib.Algebra.Group.Action.Faithful
/-- Typeclass for faithful actions.  -/
FaithfulSMul : (M : Type u_4) → (α : Type u_5) → [SMul M α] → Prop
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.homCategory_id_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : Bᵒᵖ) (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.id f).unop2 = CategoryTheory.CategoryStruct.id f.unop
-- Mathlib.Analysis.Normed.Module.Completion
UniformSpace.Completion.instNormedFieldOfCompletableTopField : (A : Type u_3) → [inst : NormedField A] → [CompletableTopField A] → NormedField (UniformSpace.Completion A)
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.overEquivOfIsInitial_unitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.overEquivOfIsInitial.{w, v_1, u_1} X h).unitIso =
    CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Over.isoMk (CategoryTheory.asIso A.hom) ⋯) ⋯
-- Mathlib.Analysis.Normed.Ring.Basic
ULift.seminormedCommRing : {α : Type u_2} → [SeminormedCommRing α] → SeminormedCommRing (ULift.{u_5, u_2} α)
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_le_card_sub_one : ∀ {V : Type u_1} {G : SimpleGraph V}, G.vertexCoverNum ≤ ENat.card V - 1
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If a presieve `R` on `X` has a subsieve `S` such that:

* `P` is a sheaf for `S`.
* For every `f` in `R`, `P` is separated for the pullback of `S` along `f`,

then `P` is a sheaf for `R`.

This is closely related to [Elephant] C2.1.6(i).
 -/
CategoryTheory.Presieve.isSheafFor_subsieve_aux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w))
  {S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X},
  S.arrows ≤ R →
    CategoryTheory.Presieve.IsSheafFor P S.arrows →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
          R f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f S).arrows) →
        CategoryTheory.Presieve.IsSheafFor P R
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_le_iff_le : ∀ {a b : ℤ} (ha₁ : Int16.minValue.toInt ≤ a) (ha₂ : a ≤ Int16.maxValue.toInt) (hb₁ : Int16.minValue.toInt ≤ b)
  (hb₂ : b ≤ Int16.maxValue.toInt), Int16.ofIntLE a ha₁ ha₂ ≤ Int16.ofIntLE b hb₁ hb₂ ↔ a ≤ b
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_map_map_of_injective : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] {f : G →+ G'} (H K : AddSubgroup G),
  Function.Injective ⇑f → (AddSubgroup.map f H).relIndex (AddSubgroup.map f K) = H.relIndex K
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_disjoint_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {δ ε : ℝ},
  δ + ε ≤ dist x y → Disjoint (Metric.ball x δ) (Metric.ball y ε)
-- Mathlib.Algebra.Polynomial.Module.AEval
/-- Construct an `R[X]`-linear map out of `AEval R M a` from an `R`-linear map out of `M`.  -/
LinearMap.ofAEval : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          (a : A) →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : Module A M] →
                  [inst_5 : Module R M] →
                    [inst_6 : IsScalarTower R A M] →
                      {N : Type u_4} →
                        [inst_7 : AddCommMonoid N] →
                          [inst_8 : Module R N] →
                            [inst_9 : Module (Polynomial R) N] →
                              [IsScalarTower R (Polynomial R) N] →
                                (f : M →ₗ[R] N) →
                                  (∀ (m : M), f (a • m) = Polynomial.X • f m) → Module.AEval R M a →ₗ[Polynomial R] N
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Restrict the codomain of a continuous alternating map to a submodule.  -/
ContinuousAlternatingMap.codRestrict : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] →
                      (f : M [⋀^ι]→L[R] N) → (p : Submodule R N) → (∀ (v : ι → M), f v ∈ p) → M [⋀^ι]→L[R] ↥p
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)),
  (s.map f.toAffineMap ⋯).altitudeFoot i = f (s.altitudeFoot i)
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.isNaN_unpack_iff_of_valid : ∀ {spec : Float.Model.Format} {b : BitVec spec.numBits},
  spec.Valid b →
    autoParam (2 ≤ spec.exponentBits) Float.Model.UnpackedFloat.isNaN_unpack_iff_of_valid._auto_1 →
      ((Float.Model.UnpackedFloat.unpack spec b).isNaN = true ↔ b = Float.Model.UnpackedFloat.packedNaN spec)
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
SemiSimplexCategory.toSimplexCategory_obj : ∀ (n : ℕ), SemiSimplexCategory.toSimplexCategory.obj { len := n } = { len := n }
-- Mathlib.CategoryTheory.Subobject.Comma
CategoryTheory.CostructuredArrow.liftQuotient.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} {A : CategoryTheory.CostructuredArrow S T}
  (P : CategoryTheory.Subobject (Opposite.op A.left))
  {q : S.obj (Opposite.unop (CategoryTheory.Subobject.underlying.obj P)) ⟶ T}
  (hq : CategoryTheory.CategoryStruct.comp (S.map P.arrow.unop) q = A.hom),
  CategoryTheory.CostructuredArrow.liftQuotient P hq =
    CategoryTheory.Subobject.mk (CategoryTheory.CostructuredArrow.homMk P.arrow.unop hq).op
-- Init.Data.Array.Attach
Array.mem_attachWith : ∀ {α : Type u_1} {xs : Array α} {q : α → Prop} (H : ∀ x ∈ xs, q x) (x : { x // q x }), x ∈ xs.attachWith q H ↔ ↑x ∈ xs
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- To check whether two maps are equalized by both maps of a fork, it suffices to check it for the
first map  -/
CategoryTheory.Limits.Fork.equalizer_ext : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (s : CategoryTheory.Limits.Fork f g)
  {W : C} {k l : W ⟶ s.pt},
  CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι →
    ∀ (j : CategoryTheory.Limits.WalkingParallelPair),
      CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp l (s.π.app j)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNonAssocRing : {n : Type u_2} → {A : Type u_5} → [Fintype n] → [DecidableEq n] → [NonAssocRing A] → NonAssocRing (CStarMatrix n n A)
-- Mathlib.Topology.Order.Compact
/-- If `f : γ → β → α` is a function that is continuous as a function on `γ × β`, `α` is a
conditionally complete linear order, and `K : Set β` is a compact set, then
`fun x ↦ sSup (f x '' K)` is a continuous function.  -/
IsCompact.continuous_sSup : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : TopologicalSpace β] [inst_4 : TopologicalSpace γ] {f : γ → β → α} {K : Set β},
  IsCompact K → Continuous ↿f → Continuous fun x => sSup (f x '' K)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- Given a function `f : α → ι`, it induces a continuous linear function by right composition on
product types. For `f = Subtype.val`, this corresponds to forgetting some set of variables.  -/
Pi.compRightL : (R : Type u_1) →
  [inst : Semiring R] →
    {ι : Type u_4} →
      (φ : ι → Type u_5) →
        [inst_1 : (i : ι) → TopologicalSpace (φ i)] →
          [inst_2 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_3 : (i : ι) → Module R (φ i)] → {α : Type u_6} → (f : α → ι) → ((i : ι) → φ i) →L[R] (i : α) → φ (f i)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k a : α} {v : β},
  (m.insert k v)[a]! = if (k == a) = true then v else m[a]!
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.eq_right : ∀ {s : String} {p : s.Pos} {t₁ t₂ t₃ t₄ : String}, p.Splits t₁ t₂ → p.Splits t₃ t₄ → t₂ = t₄
-- Mathlib.Algebra.Field.Defs
Field.toZPow : {K : Type u} → [self : Field K] → ZPow K
-- Mathlib.Tactic.NormNum.NatFactorial
/-- Calculate `n.ascFactorial l` and return this value along with a proof of the result.  -/
Mathlib.Meta.NormNum.proveAscFactorial : ℕ → ℕ → (en el : Q(ℕ)) → ℕ × (eresult : Q(ℕ)) × Q(«$en».ascFactorial «$el» = «$eresult»)
-- Mathlib.RingTheory.Flat.CategoryTheory
Module.Flat.instPreservesFiniteLimitsModuleCatTensorLeftOfCarrier : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) [Module.Flat R ↑M],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft M)
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.instHSubOffset : HSub Std.Time.PlainDate Std.Time.Day.Offset Std.Time.PlainDate
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- Disjoint unions of locally path-connected spaces are locally path-connected.  -/
Sum.locallyPathConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyPathConnectedSpace X]
  [LocallyPathConnectedSpace Y], LocallyPathConnectedSpace (X ⊕ Y)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instAdd : {E : Type u_3} → [inst : AddGroup E] → Add (AddGroupSeminorm E)
-- Mathlib.Data.Fin.SuccPred
/-- `castPred i` sends `i : Fin (n + 1)` to `Fin n` as long as i ≠ last n.  -/
Fin.castPred : {n : ℕ} → (i : Fin (n + 1)) → i ≠ Fin.last n → Fin n
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.δ_hom : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X Y : Action (Type u) G},
  Rep.Hom.hom (CategoryTheory.Functor.OplaxMonoidal.δ (Rep.linearization k G) X Y) =
    Representation.LinearizeMonoidal.δ X Y
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} (f : ContIntertwiningMap π₁ π₂) (v : V),
  f.toContinuousLinearMap v = f v
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.LocallyIntegrableOn.mono : ∀ {X : Type u_1} {E : Type u_6} {F : Type u_7} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAddCommGroup F] {μ : MeasureTheory.Measure X} {s : Set X} {f : X → E},
  MeasureTheory.LocallyIntegrableOn f s μ →
    ∀ {g : X → F},
      MeasureTheory.AEStronglyMeasurable g μ → (∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖) → MeasureTheory.LocallyIntegrableOn g s μ
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.nondegenerate_toBilin'_iff : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {M : Matrix ι ι R₂},
  (Matrix.toBilin' M).Nondegenerate ↔ M.Nondegenerate
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Run `simp_all? +suggestions` at every step in proofs, reporting where it succeeds.  -/
linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions : Lean.Option Bool