mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.coyonedaUnique_hom_app_hom_apply : ∀ {n : Type v} [inst : Unique n] (X : CommRingCat) (a : Opposite.unop (Opposite.op n) → ↑X),
  (CommRingCat.Hom.hom (CommRingCat.coyonedaUnique.hom.app X)) a = a default
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
/-- The square root is operator concave.  -/
CFC.concaveOn_sqrt : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A],
  ConcaveOn ℝ (Set.Ici 0) CFC.sqrt
-- Lean.Attributes
Lean.attributeExtension : Lean.AttributeExtension
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- If all elements of `s : Set A` commute pairwise, then `adjoin R s` is commutative.  -/
NonUnitalAlgebra.isMulCommutative_adjoin : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {s : Set A},
  (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → IsMulCommutative ↥(NonUnitalAlgebra.adjoin R s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanExt_hom_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.spanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingSpan.right = iZ.hom
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insertMany_list_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α},
  t.insertMany l = ∅ ↔ t = ∅ ∧ l = []
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.LaxMonoidalFunctor.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] [inst_4 : SizeOf C]
  [inst_5 : SizeOf D] (toFunctor : CategoryTheory.Functor C D)
  (laxMonoidal : autoParam toFunctor.LaxMonoidal CategoryTheory.LaxMonoidalFunctor.laxMonoidal._autoParam),
  sizeOf { toFunctor := toFunctor, laxMonoidal := laxMonoidal } = 1 + sizeOf toFunctor + sizeOf laxMonoidal
-- Mathlib.CategoryTheory.GradedObject.Single
/-- The composition of the single functor `single j : C ⥤ GradedObject J C` and the
evaluation functor `eval j` identifies to the identity functor.  -/
CategoryTheory.GradedObject.singleCompEval : {J : Type u_1} →
  (C : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Limits.HasInitial C] →
        [inst_2 : DecidableEq J] →
          (j : J) →
            (CategoryTheory.GradedObject.single j).comp (CategoryTheory.GradedObject.eval j) ≅
              CategoryTheory.Functor.id C
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackShape.Hom.term : {J : Type w} → (j : J) → CategoryTheory.Limits.WidePullbackShape.Hom (some j) none
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.insert.go.match_1.congr_eq_3 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.lt),
  x = Ordering.lt →
    (match x with
      | Ordering.eq => h_1 ()
      | Ordering.gt => h_2 ()
      | Ordering.lt => h_3 ()) ≍
      h_3 ()
-- Mathlib.Analysis.Normed.Group.Uniform
LocallyLipschitzOn.mul : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f g : α → E}
  {s : Set α}, LocallyLipschitzOn s f → LocallyLipschitzOn s g → LocallyLipschitzOn s fun x => f x * g x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Extract the cone from a binary bicone.  -/
CategoryTheory.Limits.BinaryBicone.toCone : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → CategoryTheory.Limits.BinaryBicone P Q → CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair P Q)
-- Mathlib.Algebra.Order.Group.Abs
mabs_div_mabs_le_mabs_mul : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a b : G), |a|ₘ / |b|ₘ ≤ |a * b|ₘ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C), ((t.triangleLTGE n).obj j).mor₁ = (t.truncLTι n).app j
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.exists_separating_of_ne : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V] [SeparatingDual R V] {x y : V}, x ≠ y → ∃ f, f x ≠ f y
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.coe_mk' : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : ↑sg = s)
  {sa : AddSubmonoid R} (ha : ↑sa = s), ↑(NonUnitalSubsemiring.mk' s sg hg sa ha) = s
-- Lean.Data.Json.FromToJson.Extra
_private.Lean.Data.Json.FromToJson.Extra.0.Lean.TreeMap.toJson : {α : Type u_1} → [Lean.ToJson α] → Std.TreeMap String α compare → Lean.Json
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
instIsContMDiffRiemannianBundleOfSomeENatTopOfLEInfty : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [inst_3 : TopologicalSpace B]
  [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_8 : (x : B) → NormedAddCommGroup (E x)]
  [inst_9 : (x : B) → InnerProductSpace ℝ (E x)] [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E]
  {a : WithTop ℕ∞} [IsContMDiffRiemannianBundle IB (↑⊤) F E] [h : ENat.LEInfty a], IsContMDiffRiemannianBundle IB a F E
-- Mathlib.Tactic.Eqns
eqnsAttribute : Lean.NameMapExtension (Array Lean.Name)
-- Init.Data.Nat.Control
/-- Checks whether the monadic predicate `p` returns `true` for all numbers less that the given bound.
Numbers are checked in increasing order until `p` returns false, after which no further are checked.
 -/
Nat.allM : {m : Type → Type u_1} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → m Bool) → m Bool
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- A ring with finite quotients has dimension `≤ 1`.  -/
Ring.HasFiniteQuotients.instDimensionLEOne : ∀ {R : Type u_1} [inst : CommRing R] [Ring.HasFiniteQuotients R], Ring.DimensionLEOne R
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- Given `Z : C` and three graded objects `X₁`, `X₂` and `X₃` in `GradedObject I C`,
this typeclass expresses that functor `Z ⊗ _` commutes with the coproduct of
the objects `X₁ i₁ ⊗ (X₂ i₂ ⊗ X₃ i₃)` such that `i₁ + i₂ + i₃ = j` for a certain `j`.
See lemma `left_tensor_tensorObj₃_ext`.  -/
CategoryTheory.GradedObject.HasLeftTensor₃ObjExt : {I : Type u} →
  [AddMonoid I] →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [CategoryTheory.MonoidalCategory C] →
          C →
            CategoryTheory.GradedObject I C →
              CategoryTheory.GradedObject I C → CategoryTheory.GradedObject I C → I → Prop
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.Extension.tensorToH1Cotangent_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S) (T : Type u_3) [inst_3 : CommRing T] [inst_4 : Algebra R T] (t : T) (x : P.H1Cotangent),
  ↑((P.tensorToH1Cotangent T) (t ⊗ₜ[R] x)) = t • (Algebra.Extension.Cotangent.map (Algebra.Extension.toBaseChange T)) ↑x
-- Mathlib.Data.Set.SMulAntidiagonal
/-- `vaddAntidiagonal s t a` is the set of all pairs of an element in `s` and an
element in `t` that vector-add to `a`.  -/
Set.vaddAntidiagonal : {G : Type u_1} → {P : Type u_2} → [VAdd G P] → Set G → Set P → P → Set (G × P)
-- Mathlib.Order.Hom.Basic
OrderEmbedding.le_map_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (f : α ↪o β) (x y : α),
  f x ⊔ f y ≤ f (x ⊔ y)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_one : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F], ContinuousLinearMapWOT.ofCLM 1 = 1
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] {a : α}
  {f : Option (β a) → Option (β a)} {t : Std.DTreeMap.Raw α β cmp}, t.WF → (t.alter a f).WF
-- Mathlib.Topology.Compactness.CompactSystem
IsCompactSystem.iff_nonempty_iInter : ∀ {α : Type u_1} (S : Set (Set α)),
  IsCompactSystem S ↔
    ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (Set.dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
-- Lean.Parser.Term
Lean.Parser.Term.letIdDecl : Lean.Parser.Parser
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.mk_penultimate_end_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, ¬p.Nil → s(p.penultimate, w) ∈ p.edges
-- Init.Data.String.Lemmas.Splits
String.Slice.copy_sliceTo_cast : ∀ {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos}, (t.sliceTo (pos.cast hst)).copy = (s.sliceTo pos).copy
-- Mathlib.Algebra.Group.TypeTags.Basic
ofMul_mul : ∀ {α : Type u} [inst : Mul α] (x y : α), Additive.ofMul (x * y) = Additive.ofMul x + Additive.ofMul y
-- Aesop.RuleSet
_private.Aesop.RuleSet.0.Aesop.LocalRuleSet.postprocessPatSubstMap : Aesop.LocalRuleSet → Aesop.RulePatternSubstMap → Array (Aesop.ForwardRule × Aesop.Substitution)
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- When `C` has pullbacks, a morphism `f : X ⟶ Y` induces a functor `MonoOver Y ⥤ MonoOver X`,
by pulling back a monomorphism along `f`.  -/
CategoryTheory.MonoOver.pullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [CategoryTheory.Limits.HasPullbacks C] →
        (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.MonoOver Y) (CategoryTheory.MonoOver X)
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
/-- Auxiliary definition for `ofCocone`.  -/
CategoryTheory.SmallObject.SuccStruct.ofCocone.obj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        {j : J} → {F : CategoryTheory.Functor (↑(Set.Iio j)) C} → CategoryTheory.Limits.Cocone F → J → C
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.leaf.inj : ∀ {α : Type u} {vs vs_1 : Array α}, Lean.PersistentArrayNode.leaf vs = Lean.PersistentArrayNode.leaf vs_1 → vs = vs_1
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsWeakLimit t) {W : C} (h : W ⟶ X)
  (k : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.IsWeakLimit.lift ht h k w) t.fst = h
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult.exprArgs : Lean.Meta.Closure.MkValueTypeClosureResult → Array Lean.Expr
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.det_four_sub_cartanMatrix_ne_zero : ∀ {ι : 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} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] [inst_9 : DecidableEq ι] [P.IsRootSystem],
  (4 - b.cartanMatrix).det ≠ 0
-- Mathlib.Data.Erased
Erased.mk.eq_1 : ∀ {α : Sort u_1} (a : α), Erased.mk a = ⟨fun b => a = b, ⋯⟩
-- Mathlib.Algebra.Ring.Equiv
MulEquiv.isLeftCancelMulZero_iff : ∀ {A : Type u_7} {B : Type u_8} [inst : MulZeroClass A] [inst_1 : MulZeroClass B] (e : A ≃* B),
  IsLeftCancelMulZero A ↔ IsLeftCancelMulZero B
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₂ → (m₁ ∩ m₂).getD k fallback = fallback
-- Mathlib.Topology.Homotopy.HSpaces
HSpace.hmul : {X : Type u} → {inst : TopologicalSpace X} → [self : HSpace X] → C(X × X, X)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.coe_mkL_apply : ∀ {𝕜 : 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] (x : E),
  ⇑((TensorProduct.mkL 𝕜 E F) x) = ⇑((TensorProduct.mk 𝕜 E F) x)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.union_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s₁ s₂ : Finset α} {t : Finset β}
  [inst_2 : DecidableEq α], (s₁ ∪ s₂) +ᵥ t = (s₁ +ᵥ t) ∪ (s₂ +ᵥ t)
-- Mathlib.Order.Bounds.Basic
IsLUB.exists_between' : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {a b : α}, IsLUB s a → a ∉ s → b < a → ∃ c ∈ s, b < c ∧ c < a
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.π₀Functor_obj : ∀ (X : SSet), SSet.π₀Functor.obj X = X.π₀
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instSemiring : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Semiring Y] → Semiring (LocallyConstant X Y)
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.nth_mk : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : List Γ) (n : ℕ), (Turing.ListBlank.mk l).nth n = l.getI n
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis.eRk_eq_eRk : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → M.eRk I = M.eRk X
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.mk.inj : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} {inst : L.Structure M} {inst_1 : L.Structure N}
  {toEmbedding : M ↪ N}
  {map_fun' :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEmbedding.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEmbedding.toFun ∘ x))
      FirstOrder.Language.Embedding.map_fun'._autoParam}
  {map_rel' :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEmbedding.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Embedding.map_rel'._autoParam}
  {toEmbedding_1 : M ↪ N}
  {map_fun'_1 :
    autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        toEmbedding_1.toFun (FirstOrder.Language.Structure.funMap f x) =
          FirstOrder.Language.Structure.funMap f (toEmbedding_1.toFun ∘ x))
      FirstOrder.Language.Embedding.map_fun'._autoParam}
  {map_rel'_1 :
    autoParam
      (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r (toEmbedding_1.toFun ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x)
      FirstOrder.Language.Embedding.map_rel'._autoParam},
  { toEmbedding := toEmbedding, map_fun' := map_fun', map_rel' := map_rel' } =
      { toEmbedding := toEmbedding_1, map_fun' := map_fun'_1, map_rel' := map_rel'_1 } →
    toEmbedding = toEmbedding_1
-- Init.Data.RArray
/-- `RArray.get`, implemented conventionally  -/
Lean.RArray.getImpl : {α : Type u} → Lean.RArray α → ℕ → α
-- Std.Time.Format
/-- Parses a time string in the 24-hour format (`HH:mm:ss`) and returns a `PlainTime`.
 -/
Std.Time.PlainTime.fromTime24Hour : String → Except String Std.Time.PlainTime
-- Init.Data.Vector.Algebra
Vector.add_zero : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Add α], (∀ (x : α), x + 0 = x) → ∀ (xs : Vector α n), xs + 0 = xs
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeWhileTR.go.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (a : Array α), List.takeWhileTR.go✝ p l [] a = l
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ofCLM_mul : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (f g : F →L[𝕜₂] F),
  ContinuousLinearMapWOT.ofCLM (f * g) = ContinuousLinearMapWOT.ofCLM f * ContinuousLinearMapWOT.ofCLM g
-- Mathlib.Topology.Homotopy.Path
/-- The constant path homotopy class at a point. This is `Path.refl` descended to the quotient.  -/
Path.Homotopic.Quotient.refl : {X : Type u} → [inst : TopologicalSpace X] → (x : X) → Path.Homotopic.Quotient x x
-- Mathlib.GroupTheory.HNNExtension
/-- `Cancels u w` is a predicate expressing whether `t^u` cancels with some occurrence
of `t^-u` when we multiply `t^u` by `w`.  -/
HNNExtension.NormalWord.Cancels : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} → {d : HNNExtension.NormalWord.TransversalPair G A B} → ℤˣ → HNNExtension.NormalWord d → Prop
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.brecOn_2.go : {motive_1 : Aesop.Frontend.RuleExpr → Sort u} →
  {motive_2 : Array Aesop.Frontend.RuleExpr → Sort u} →
    {motive_3 : List Aesop.Frontend.RuleExpr → Sort u} →
      (t : List Aesop.Frontend.RuleExpr) →
        ((t : Aesop.Frontend.RuleExpr) → t.below → motive_1 t) →
          ((t : Array Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_1 t → motive_2 t) →
            ((t : List Aesop.Frontend.RuleExpr) → Aesop.Frontend.RuleExpr.below_2 t → motive_3 t) →
              motive_3 t ×' Aesop.Frontend.RuleExpr.below_2 t
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioi_eq_empty : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α], Finset.Ioi a = ∅ ↔ IsMax a
-- Mathlib.Data.Fintype.Card
Finset.card_add_card_compl : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset α), s.card + sᶜ.card = Fintype.card α
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- The function underlying this additive map.  -/
BoxIntegral.BoxAdditiveMap.toFun : {ι : Type u_3} →
  {M : Type u_4} →
    [inst : AddCommMonoid M] →
      {I : WithTop (BoxIntegral.Box ι)} → BoxIntegral.BoxAdditiveMap ι M I → BoxIntegral.Box ι → M
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.termSum_of_lt : ∀ (N : ℕ) {s : ℝ},
  1 < s →
    ZetaAsymptotics.termSum s N =
      1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
-- Mathlib.Algebra.Algebra.Operations
/-- Sub-R-modules of an R-algebra form an idempotent semiring.  -/
Submodule.idemSemiring : {R : Type u} →
  [inst : CommSemiring R] → {A : Type v} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → IdemSemiring (Submodule R A)
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
/-- This is a def because once we have that both `(e' e).inverse` and `(e' e).functor` are
braided, this causes a diamond.
 -/
CategoryTheory.Monoidal.transportedFunctorCompInverseLaxBraided : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) →
          [inst_2 : CategoryTheory.MonoidalCategory C] →
            [inst_3 : CategoryTheory.BraidedCategory C] →
              ((CategoryTheory.Monoidal.equivalenceTransported e).functor.comp
                  (CategoryTheory.Monoidal.equivalenceTransported e).inverse).LaxBraided
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- The function supported at `i`, with value `x` there, and `0` elsewhere.  -/
RestrictedProduct.single : {ι : Type u_1} →
  {S : ι → Type u_3} →
    {G : ι → Type u_4} →
      [inst : (i : ι) → SetLike (S i) (G i)] →
        (A : (i : ι) → S i) →
          [DecidableEq ι] →
            [inst_2 : (i : ι) → Zero (G i)] →
              [∀ (i : ι), ZeroMemClass (S i) (G i)] →
                (i : ι) → G i → RestrictedProduct (fun i => G i) (fun i => ↑(A i)) Filter.cofinite
-- Lean.Structure
/-- Data about a type created with the `structure` command.
 -/
Lean.StructureInfo : Type
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The trivial norm on a ring `R` is the `MulRingNorm` taking value `0` at `0` and `1` at every
other element.  -/
MulRingNorm.instOne : (R : Type u_1) → [inst : NonAssocRing R] → [DecidableEq R] → [NoZeroDivisors R] → [Nontrivial R] → One (MulRingNorm R)
-- Mathlib.Data.FinEnum
FinEnum.card_fin : ∀ {n : ℕ} [inst : FinEnum (Fin n)], FinEnum.card (Fin n) = n
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.adjoint_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E], ContinuousLinearMap.adjoint (ContinuousLinearMap.id 𝕜 E) = ContinuousLinearMap.id 𝕜 E
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `AddMonoidWithOne` across an `Equiv`  -/
Equiv.addMonoidWithOne : {α : Type u_1} → {β : Type u_2} → α ≃ β → [AddMonoidWithOne β] → AddMonoidWithOne α
-- Init.Data.Array.OfFn
Array.ofFnM_succ' : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α},
  Array.ofFnM f = do
    let a ← f 0
    let as ← Array.ofFnM fun i => f i.succ
    pure (#[a] ++ as)
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.ExceptType.noConfusionType : Sort v✝ → Mathlib.Tactic.Ring.ExceptType → Mathlib.Tactic.Ring.ExceptType → Sort v✝
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableOn.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  DifferentiableOn 𝕜 f s → s ∈ nhds x → DifferentiableAt 𝕜 f x
-- Mathlib.Data.Multiset.Fintype
Multiset.cast_apply_snd : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} (h : s = t) (x : s.ToType),
  ((Multiset.cast h) x).snd = Fin.cast ⋯ x.snd
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isExtTangent_comm : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P}, s₁.IsExtTangent s₂ ↔ s₂.IsExtTangent s₁
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.dual_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s → AntivaryOn f (⇑OrderDual.toDual ∘ g) s
-- Mathlib.Order.ScottContinuity
/-- Eta-expanded form of `ScottContinuousOn.id` -/
ScottContinuousOn.fun_id : ∀ {α : Type u_1} [inst : Preorder α] {D : Set (Set α)}, ScottContinuousOn D fun x => x
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- If `v : ι → M` is a family of vectors and there exists a family of linear forms
`f : ι → Dual R M` such that `f i (v j)` is `1` for `i = j` and `0` for `i ≠ j`, then
`v` is linearly independent.  -/
LinearIndependent.of_pairwise_dual_eq_zero_one : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (v : ι → M) (f : ι → Module.Dual R M),
  (Pairwise fun i j => (f i) (v j) = 0) → (∀ (i : ι), (f i) (v i) = 1) → LinearIndependent R v