mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
/-- The generating sections of the free sheaf of modules.  -/
SheafOfModules.free.generatingSections : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] → (I : Type u) → (SheafOfModules.free I).GeneratingSections
-- Mathlib.Tactic.FailIfNoProgress
_private.Mathlib.Tactic.FailIfNoProgress.0.Mathlib.Tactic.lctxIsDefEq.match_1.eq_2 : ∀ (motive : List (Option Lean.LocalDecl) → List (Option Lean.LocalDecl) → Sort u_1)
  (l₁ l₂ : List (Option Lean.LocalDecl)) (h_1 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive (none :: l₁) l₂)
  (h_2 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive l₁ (none :: l₂))
  (h_3 :
    (d₁ : Lean.LocalDecl) →
      (l₁ : List (Option Lean.LocalDecl)) →
        (d₂ : Lean.LocalDecl) → (l₂ : List (Option Lean.LocalDecl)) → motive (some d₁ :: l₁) (some d₂ :: l₂))
  (h_4 : Unit → motive [] []) (h_5 : (x x_1 : List (Option Lean.LocalDecl)) → motive x x_1),
  (∀ (l₁_1 : List (Option Lean.LocalDecl)), l₁ = none :: l₁_1 → False) →
    (match l₁, none :: l₂ with
      | none :: l₁, l₂ => h_1 l₁ l₂
      | l₁, none :: l₂ => h_2 l₁ l₂
      | some d₁ :: l₁, some d₂ :: l₂ => h_3 d₁ l₁ d₂ l₂
      | [], [] => h_4 ()
      | x, x_1 => h_5 x x_1) =
      h_2 l₁ l₂
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.instIsScalarTowerSubtypeMemSubalgebraSubalgebra : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B),
  IsScalarTower (↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)) A B
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.functorPushforward_monotone : ∀ {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 : C}, Monotone (CategoryTheory.Presieve.functorPushforward F)
-- Init.Grind.Lemmas
Lean.Grind.or_of_and_eq_false : ∀ {a b : Prop}, (a ∧ b) = False → ¬a ∨ ¬b
-- Init.Data.Iterators.Consumers.Loop
/-- Returns the first non-`none` result of applying the monadic function `f` to each output
of the iterator, in order. Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`. The outputs of `it` are
examined in order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.findSomeM?`.

Example:
```lean example
#eval [7, 6, 5, 8, 1, 2, 6].iter.findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none
```
```output
Almost! 6
Almost! 5
```
```output
some 10
```
 -/
Std.Iter.Total.findSomeM? : {α β : Type w} →
  {γ : Type x} →
    {m : Type x → Type w'} →
      [Monad m] →
        [inst : Std.Iterator α Id β] →
          [Std.IteratorLoop α Id m] → [Std.Iterators.Finite α Id] → Std.Iter.Total β → (β → m (Option γ)) → m (Option γ)
-- Lean.Meta.MkIffOfInductiveProp
/-- Generates an expression of the form `∃ (args), inner`. `args` is assumed to be a list of fvars.
When possible, `p ∧ q` is used instead of `∃ (_ : p), q`.  -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.mkExistsList : List Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_eq_ofIntClamp : ∀ {x : ℤ} {h₁ : Int8.minValue.toInt ≤ x} {h₂ : x ≤ Int8.maxValue.toInt}, Int8.ofIntLE x h₁ h₂ = Int8.ofIntClamp x
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The underlying object associated to a coalgebra.  -/
CategoryTheory.Comonad.Coalgebra.A : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {G : CategoryTheory.Comonad C} → G.Coalgebra → C
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp)
  (e_t : t = t_1) (h : t ≠ ∅), t.maxKey h = t_1.maxKey ⋯
-- Mathlib.Logic.Equiv.List
Denumerable.denumerable_list_aux : ∀ {α : Type u_1} [inst : Denumerable α] (n : ℕ), ∃ a ∈ Encodable.decodeList n, Encodable.encodeList a = n
-- Init.Data.SInt.Bitwise
Int8.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : Int8}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.WF.mk : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.inner.WF → t.WF
-- Mathlib.Data.Nat.Choose.Multinomial
Multiset.multinomial_nsmul : ∀ (k : ℕ) (m : Multiset ℕ), (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x => m.sum) * m.multinomial ^ k
-- Mathlib.RingTheory.Ideal.Basic
Ideal.bot_lt_of_maximal : ∀ {R : Type u_5} [inst : CommSemiring R] [Nontrivial R] (M : Ideal R) [hm : M.IsMaximal], ¬IsField R → ⊥ < M
-- Mathlib.SetTheory.Cardinal.Aleph
/-- **Alias** of `Ordinal.type_lt_cardinal`. -/
Cardinal.type_cardinal : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.univ.{u, u + 1}
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- Construct a hom in `TopModuleCat` from a continuous linear map.  -/
TopModuleCat.ofHom : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {X Y : Type v} →
        [inst_2 : AddCommGroup X] →
          [inst_3 : Module R X] →
            [inst_4 : TopologicalSpace X] →
              [inst_5 : ContinuousAdd X] →
                [inst_6 : ContinuousSMul R X] →
                  [inst_7 : AddCommGroup Y] →
                    [inst_8 : Module R Y] →
                      [inst_9 : TopologicalSpace Y] →
                        [inst_10 : ContinuousAdd Y] →
                          [inst_11 : ContinuousSMul R Y] → (X →L[R] Y) → (TopModuleCat.of R X ⟶ TopModuleCat.of R Y)
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_nonneg_iff_of_le : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : LinearOrder k] [IsStrictOrderedRing k] [inst_5 : PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E]
  {f : k → E} {x y : k}, x ≤ y → (0 ≤ slope f x y ↔ f x ≤ f y)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The braiding isomorphism is symmetric.  -/
CategoryTheory.Limits.prod.symmetry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : C) [inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q]
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct Q P],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.braiding P Q).hom
      (CategoryTheory.Limits.prod.braiding Q P).hom =
    CategoryTheory.CategoryStruct.id (P ⨯ Q)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_unzero_iff : ∀ {α : Type u_1} [inst : LT α] {y : WithZero α} {a : α} (hy : y ≠ 0), a < WithZero.unzero hy ↔ ↑a < y
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.ext : ∀ {R : Type u} {a b : R} {x y : QuadraticAlgebra R a b}, x.re = y.re → x.im = y.im → x = y
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.mk.inj : ∀ {name : String} {type? docString? doc_url? kind? : Option String} {name_1 : String}
  {type?_1 docString?_1 doc_url?_1 kind?_1 : Option String},
  { name := name, type? := type?, docString? := docString?, doc_url? := doc_url?, kind? := kind? } =
      { name := name_1, type? := type?_1, docString? := docString?_1, doc_url? := doc_url?_1, kind? := kind?_1 } →
    name = name_1 ∧ type? = type?_1 ∧ docString? = docString?_1 ∧ doc_url? = doc_url?_1 ∧ kind? = kind?_1
-- Mathlib.Algebra.Module.Presentation.Differentials
/-- The shape of the presentation by generators and relations of the `S`-module `Ω[S⁄R]`
that is obtained from a presentation of `S` as an `R`-algebra.  -/
Algebra.Presentation.differentialsRelations : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Presentation R S ι σ → Module.Relations S
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_eq_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Zero α] {M : Matrix m n α}, M.transpose = 0 ↔ M = 0
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.instRingHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β], RingHomClass (α →+*o β) α β
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.BitVec.sdiv_eq.match_1.eq_1 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, false with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_1 ()
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α},
  Std.ExtDHashMap.Const.get? (m₁.union m₂) k = (Std.ExtDHashMap.Const.get? m₂ k).or (Std.ExtDHashMap.Const.get? m₁ k)
-- Lean.Parser.Basic
Lean.Parser.nonReservedSymbolInfo : String → Bool → Lean.Parser.ParserInfo
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
UpperHalfPlane.denom_continuous : Continuous ↿UpperHalfPlane.denom
-- Mathlib.Order.Defs.Unbundled
/-- `IsPreorder X r` means that the binary relation `r` on `X` is a pre-order, that is, reflexive
and transitive.  -/
IsPreorder : (α : Sort u_1) → (α → α → Prop) → Prop
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The lax monoidal functor induced by a lax braided functor.  -/
CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                CategoryTheory.LaxBraidedFunctor C D → CategoryTheory.LaxMonoidalFunctor C D
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabFootnote.mk.injEq : ∀ (name name_1 : Lean.StrLit), ({ name := name } = { name := name_1 }) = (name = name_1)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.map_id : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [inst_2 : IsStrictOrderedRing R]
  (f : Convexity.StdSimplex R M), Convexity.StdSimplex.map id f = f
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.localFrameCoeff_apply_of_mem_baseSet : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F)
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x : M} (hx : x ∈ e.baseSet) (s : (x : M) → V x) (i : ι),
  (Bundle.Trivialization.localFrameCoeff I e b i x) (s x) = ((e.basisAt b hx).repr (s x)) i
-- Mathlib.Data.Set.Lattice
Set.iUnion_empty : ∀ {α : Type u_1} {ι : Sort u_5}, ⋃ x, ∅ = ∅
-- Mathlib.Algebra.Torsor.Defs
/-- If subtracting two points produces 0, they are equal.  -/
eq_of_vsub_eq_zero : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ : P}, p₁ -ᵥ p₂ = 0 → p₁ = p₂
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- In a locally compact space, any integrable function can be approximated by compactly supported
continuous functions, version in terms of `∫`.  -/
MeasureTheory.Integrable.exists_hasCompactSupport_integral_sub_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [R1Space α]
  [WeaklyLocallyCompactSpace α] [μ.Regular] {f : α → E},
  MeasureTheory.Integrable f μ →
    ∀ {ε : ℝ},
      0 < ε → ∃ g, HasCompactSupport g ∧ ∫ (x : α), ‖f x - g x‖ ∂μ ≤ ε ∧ Continuous g ∧ MeasureTheory.Integrable g μ
-- Mathlib.Algebra.Homology.EulerCharacteristic
ComplexShape.EulerCharSigns.mk : {ι : Type u_1} → {c : ComplexShape ι} → (χ : ι → ℤˣ) → (∀ {i j : ι}, c.Rel i j → χ j = -χ i) → c.EulerCharSigns
-- Mathlib.ModelTheory.Order
/-- The theory of preorders.  -/
FirstOrder.Language.preorderTheory : (L : FirstOrder.Language) → [L.IsOrdered] → L.Theory
-- Init.Meta.Defs
Lean.TSyntax.instCoeCharLitTerm : Coe Lean.CharLit Lean.Term
-- Mathlib.GroupTheory.Congruence.Defs
Con.comap_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M → N),
  Function.Surjective f → ∀ (hf' : ∀ (x y : M), f (x * y) = f x * f y), Function.Injective (Con.comap f hf')
-- Mathlib.Data.List.Chain
List.isChain_cons_pmap : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {p : β → Prop} (f : (b : β) → p b → α) {l : List β}
  (hl : ∀ b ∈ l, p b) {a : β} (ha : p a),
  List.IsChain R (f a ha :: List.pmap f l hl) ↔
    List.IsChain (fun a b => ∃ (ha : p a) (hb : p b), R (f a ha) (f b hb)) (a :: l)
-- Mathlib.Topology.ExtremallyDisconnected
/-- An extremally disconnected topological space is a space
in which the closure of every open set is open.  -/
ExtremallyDisconnected : (X : Type u) → [TopologicalSpace X] → Prop
-- Mathlib.Data.Nat.Dist
Nat.dist_tri_left : ∀ (n m : ℕ), m ≤ n.dist m + n
-- Mathlib.Algebra.Opposites
MulOpposite.instSub : {α : Type u_1} → [Sub α] → Sub αᵐᵒᵖ
-- Mathlib.Geometry.Manifold.Instances.Icc
/-- The inclusion map from a closed segment to `ℝ` is a smooth embedding  -/
isSmoothEmbedding_subtypeVal_Icc : ∀ {x y : ℝ} [h : Fact (x < y)] {n : WithTop ℕ∞},
  Manifold.IsSmoothEmbedding (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ ℝ) n fun z => ↑z
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderCobaseChangeAlongOfIsStableUnderCobaseChange : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C)
  [P.IsStableUnderCobaseChange] {X Y : C} (f : X ⟶ Y), P.IsStableUnderCobaseChangeAlong f
-- Init.Data.Float.Model.Float
/-- Pack an `UnpackedFloat` into the corresponding `Float.Model`.
This operation only gives a meaningful result if the float is
already correctly rounded for the `Format.binary64` format.
 -/
Float.Model.pack : Float.Model.UnpackedFloat → Float.Model
-- Lean.Server.Rpc.Basic
Lean.Server.WithRpcRef.val : {α : Type u} → Lean.Server.WithRpcRef α → α
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.submodule_span_le_lieSpan : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L},
  Submodule.span R s ≤ (LieSubalgebra.lieSpan R L s).toSubmodule
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- Auxiliary definition for `vComp`.  -/
CategoryTheory.Oplax.LaxTrans.vCompApp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.OplaxFunctor B C} →
          CategoryTheory.Oplax.LaxTrans F G → CategoryTheory.Oplax.LaxTrans G H → (a : B) → F.obj a ⟶ H.obj a
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The ring isomorphism between the stalk of the structure sheaf of `R` at a point `p`
corresponding to a prime ideal in `R` and the localization of `R` at `p`.  -/
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.stalkIsoₗ : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          (AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x ≅
            ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)
-- Mathlib.Probability.Distributions.Binomial
/-- The binomial probability distribution with parameter `p`.  -/
ProbabilityTheory.«termBin(_,_)» : Lean.ParserDescr
-- Mathlib.Condensed.Light.TopCatAdjunction
LightCondSet.topCatAdjunctionCounit_bijective : ∀ (X : TopCat), Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom (LightCondSet.topCatAdjunctionCounit X))
-- Mathlib.Data.EReal.Inv
EReal.mul_le_of_forall_lt_of_nonneg : ∀ {a b c : EReal}, 0 ≤ a → 0 ≤ c → (∀ a' ∈ Set.Ioo 0 a, ∀ b' ∈ Set.Ioo 0 b, a' * b' ≤ c) → a * b ≤ c
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The composition of morphisms in `Φ.LeftResolution X₂`.  -/
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comp : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → {L L' L'' : Φ.LeftResolution X₂} → L.Hom L' → L'.Hom L'' → L.Hom L''
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.zeroBasis_apply : ∀ {𝕜 : Type u_1} {α : Type u_3} [inst : NormedRing 𝕜] [inst_1 : DecidableEq α] (i : α), lp.zeroBasis i = lp.single 0 i 1
-- Mathlib.Topology.ContinuousMap.Compact
/-- An arbitrarily chosen modulus of uniform continuity for a given function `f` and `ε > 0`.  -/
ContinuousMap.modulus : {α : Type u_1} →
  {β : Type u_2} →
    [inst : PseudoMetricSpace α] → [CompactSpace α] → [inst_2 : PseudoMetricSpace β] → C(α, β) → (ε : ℝ) → 0 < ε → ℝ
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformly.neg` -/
TendstoUniformly.fun_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {g : β → α},
  TendstoUniformly f g l → TendstoUniformly (fun i i_1 => -f i i_1) (fun i => -g i) l
-- Lean.Syntax
Lean.Syntax.modifyArg : Lean.Syntax → ℕ → (Lean.Syntax → Lean.Syntax) → Lean.Syntax
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_assoc : ∀ (x y z : ℕ), x &&& y &&& z = x &&& (y &&& z)
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.lapMatrix_ker_basis_aux.eq_1 : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  [inst_3 : DecidableEq G.ConnectedComponent] (c : G.ConnectedComponent),
  G.lapMatrix_ker_basis_aux c = ⟨fun i => if G.connectedComponentMk i = c then 1 else 0, ⋯⟩
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.Triangle.rotate_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle C), T.rotate.mor₁ = T.mor₂
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The unit morphism of a monoid object.  -/
CategoryTheory.MonObj.termη : Lean.ParserDescr
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapCLM.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (n : ℕ∞) {K : TopologicalSpace.Compacts E} (i : ℕ),
  ContDiffMapSupportedIn.structureMapCLM 𝕜 n i =
    { toLinearMap := ContDiffMapSupportedIn.structureMapLM 𝕜 n i, cont := ⋯ }
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stepAux.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (x : σ) (x_1 : Turing.Tape Γ) (a : Γ → σ → Γ)
  (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stepAux (Turing.TM1.Stmt.write a q) x x_1 = Turing.TM1.stepAux q x (Turing.Tape.write (a x_1.head x) x_1)
-- Mathlib.Algebra.Group.Action.Defs
AddCommute.vadd_right : ∀ {M : Type u_1} {α : Type u_5} [inst : VAdd M α] [inst_1 : Add α] [VAddCommClass M α α] [VAddAssocClass M α α]
  {a b : α}, AddCommute a b → ∀ (r : M), AddCommute a (r +ᵥ b)
-- Mathlib.Algebra.Star.Module
IsSelfAdjoint.coe_selfAdjointPart_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] {x : A}, IsSelfAdjoint x → ↑((selfAdjointPart R) x) = x
-- Mathlib.Algebra.Star.LinearMap
/-- A linear map `f : (m → R) →ₗ (n → R)` is self-adjoint (with respect to the intrinsic star)
iff its corresponding matrix `f.toMatrix'` has all self-adjoint elements.
So star-preserving maps correspond to their matrices containing only self-adjoint elements.  -/
LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix' : ∀ {R : Type u_4} {m : Type u_5} {n : Type u_6} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] (f : WithConv ((m → R) →ₗ[R] n → R)),
  IsSelfAdjoint f ↔ ∀ (i : n) (j : m), IsSelfAdjoint (LinearMap.toMatrix' f.ofConv i j)
-- Mathlib.Algebra.Group.Submonoid.Defs
ZeroMemClass.zero_def : ∀ {A : Type u_3} {M₁ : Type u_4} [inst : SetLike A M₁] [inst_1 : Zero M₁] [hA : ZeroMemClass A M₁] (S' : A), 0 = ⟨0, ⋯⟩
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instInhabited : Inhabited LightProfinite
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P.ind.IsClosedUnderIsomorphisms
-- Mathlib.Analysis.Complex.Basic
Complex.mem_slitPlane_iff_not_le_zero : ∀ {z : ℂ}, z ∈ Complex.slitPlane ↔ ¬z ≤ 0
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.of_subsingleton : ∀ {𝕜 : 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} {f' : E →L[𝕜] F} {x : E} {s : Set E} [T1Space E],
  s.Subsingleton → HasFDerivWithinAt f f' s x
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.eval.eq_2 : ∀ (fs : Turing.ToPartrec.Code) (as : List ℕ) (k : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.cons₁ fs as k).eval = fun v => do
    let ns ← fs.eval as
    k.eval (v.headI :: ns)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_involutive : ∀ {ι : 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) (i : ι),
  Function.Involutive ⇑(P.reflectionPerm i)
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.support_erase : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α) [inst_1 : DecidableEq α],
  ((SkewMonoidAlgebra.erase a) f).support = f.support.erase a
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instFiniteHom : ∀ {a b : SimplexCategory}, Finite (a ⟶ b)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- Turn an exact functor into a left exact functor.  -/
CategoryTheory.RightExactFunctor.ofExact : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C ⥤ₑ D) (C ⥤ᵣ D)
-- Mathlib.Algebra.Lie.Basic
LieEquiv.instOne : {R : Type u} →
  {L₁ : Type v} → [inst : CommRing R] → [inst_1 : LieRing L₁] → [inst_2 : LieAlgebra R L₁] → One (L₁ ≃ₗ⁅R⁆ L₁)
-- Mathlib.Order.Hom.Basic
OrderHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → FunLike (α →o β) α β