mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is a subset of `s`.  -/
SimpleGraph.isBipartiteWith_neighborFinset_subset' : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet w)],
  G.IsBipartiteWith ↑s ↑t → w ∈ t → G.neighborFinset w ⊆ s
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instMonoidOfContinuousMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : Monoid β] → [ContinuousMul β] → Monoid C(α, β)
-- Mathlib.Data.Finset.Basic
Finset.ssubset_iff_exists_subset_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ⊂ t ↔ ∃ a ∈ t, s ⊆ t.erase a
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.nonempty_iso_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C), Nonempty (X ≅ X)
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.proper.injEq : ∀ {s : String.Slice} (needle : String.Slice) (table : Vector ℕ needle.utf8ByteSize)
  (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) (stackPos needlePos : String.Pos.Raw)
  (hn : needlePos < needle.rawEndPos) (needle_1 : String.Slice) (table_1 : Vector ℕ needle_1.utf8ByteSize)
  (ht_1 : table_1 = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle_1)
  (stackPos_1 needlePos_1 : String.Pos.Raw) (hn_1 : needlePos_1 < needle_1.rawEndPos),
  (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =
      String.Slice.Pattern.ForwardSliceSearcher.proper needle_1 table_1 ht_1 stackPos_1 needlePos_1 hn_1) =
    (needle = needle_1 ∧ table ≍ table_1 ∧ stackPos = stackPos_1 ∧ needlePos = needlePos_1)
-- Mathlib.LinearAlgebra.Contraction
dualTensorHomEquivOfBasis_symm_cancel_left : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (b : Module.Basis ι R M)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (x : TensorProduct R (Module.Dual R M) N),
  (dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x
-- Mathlib.Topology.Sequences
Topology.IsQuotientMap.sequentialSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [SequentialSpace X]
  {f : X → Y}, Topology.IsQuotientMap f → SequentialSpace Y
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertEntry_le : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  (Std.Internal.List.insertEntry k v l).length ≤ l.length + 1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The identity determines a cocone on the coequalizer diagram of `f` and `g`, if `f = g`.  -/
CategoryTheory.Limits.idCofork : {C : Type u} →
  {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → {f g : X ⟶ Y} → f = g → CategoryTheory.Limits.Cofork f g
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- Universal property from localized module:
If `(M', f : M ⟶ M')` is a localized module then it satisfies the following universal property:
For every `R`-module `M''` which every `s : S`-scalar multiplication is invertible and for every
`R`-linear map `g : M ⟶ M''`, there is a unique `R`-linear map `l : M' ⟶ M''` such that
`l ∘ f = g`.
```
M -----f----> M'
|           /
|g       /
|     /   l
v   /
M''
```
 -/
IsLocalizedModule.is_universal : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') [IsLocalizedModule S f] (g : M →ₗ[R] M''),
  (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) → ∃! l, l ∘ₗ f = g
-- Init.Data.UInt.Bitwise
USize.toNat_or : ∀ (a b : USize), (a ||| b).toNat = a.toNat ||| b.toNat
-- Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
_private.Lean.Meta.Tactic.Grind.MarkNestedSubsingletons.0.Lean.Meta.Grind.markNestedSubsingletons.preprocess : Lean.Expr → Lean.Meta.Grind.M✝ Lean.Expr
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.addAction_stabilizer_coe : ∀ {G : Type u_1} [inst : AddGroup G] {α : Type u_2} [inst_1 : AddAction G α] [inst_2 : DecidableEq α] {n : ℕ}
  (s : ↑(Set.powersetCard α n)), AddAction.stabilizer G s = AddAction.stabilizer G ↑s
-- Mathlib.Topology.MetricSpace.HolderNorm
HolderWith.memHolder : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C : NNReal}, HolderWith C r f → MemHolder r f
-- Mathlib.Probability.Notation
/-- `X ≤ₐₛ Y` if `X ≤ Y` almost surely.  -/
ProbabilityTheory.«term_≤ₐₛ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Limits.Preorder
/-- A functor has a limit iff there exists a glb.  -/
Preorder.hasLimit_iff_hasGLB : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C), CategoryTheory.Limits.HasLimit F ↔ ∃ x, IsGLB (Set.range F.obj) x
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffWithinAt.prodMap : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {f : M → M'} {s : Set M} {x : M} {n : WithTop ℕ∞} {g : N → N'} {r : Set N} {y : N},
  ContMDiffWithinAt I I' n f s x →
    ContMDiffWithinAt J J' n g r y → ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) (x, y)
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
/-- The isomorphism `(ofCocone c).obj ⟨i, _⟩ ≅ F.obj ⟨i, _⟩` when `i < j`.  -/
CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso : {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} →
            (c : CategoryTheory.Limits.Cocone F) →
              (i : J) → (hi : i < j) → (CategoryTheory.SmallObject.SuccStruct.ofCocone c).obj ⟨i, ⋯⟩ ≅ F.obj ⟨i, hi⟩
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.get?_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {a : α}, m.get? a = Std.DHashMap.Internal.Raw₀.get? ⟨m, ⋯⟩ a
-- Mathlib.Analysis.Convex.Radon
/-- **Helly's theorem** for finite families of convex sets.

If `F` is a finite family of convex sets in a vector space of finite dimension `d`, and any
`k ≤ d + 1` sets of `F` intersect nontrivially, then all sets of `F` intersect nontrivially.  -/
Convex.helly_theorem' : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : ι → Set E} {s : Finset ι},
  (∀ i ∈ s, Convex 𝕜 (F i)) →
    (∀ I ⊆ s, I.card ≤ Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → (⋂ i ∈ s, F i).Nonempty
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_top : ↑⊤ = ⊤
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mul_power : ∀ {a b c : Cardinal.{u_1}}, (a * b) ^ c = a ^ c * b ^ c
-- Lean.Structure
Lean.StructureInfo.mk.injEq : ∀ (structName : Lean.Name) (fieldNames : Array Lean.Name) (fieldInfo : Array Lean.StructureFieldInfo)
  (parentInfo : Array Lean.StructureParentInfo) (structName_1 : Lean.Name) (fieldNames_1 : Array Lean.Name)
  (fieldInfo_1 : Array Lean.StructureFieldInfo) (parentInfo_1 : Array Lean.StructureParentInfo),
  ({ structName := structName, fieldNames := fieldNames, fieldInfo := fieldInfo, parentInfo := parentInfo } =
      { structName := structName_1, fieldNames := fieldNames_1, fieldInfo := fieldInfo_1,
        parentInfo := parentInfo_1 }) =
    (structName = structName_1 ∧ fieldNames = fieldNames_1 ∧ fieldInfo = fieldInfo_1 ∧ parentInfo = parentInfo_1)
-- Aesop.Forward.Match.Types
Aesop.instInhabitedForwardRuleMatch.default : Aesop.ForwardRuleMatch
-- Mathlib.Control.Applicative
instLawfulApplicativeAddConst : ∀ {α : Type u_1} [inst : AddMonoid α], LawfulApplicative (Functor.AddConst α)
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.continuous_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] {N : Subgroup G}, Continuous QuotientGroup.mk
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_hom_ι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens)
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f U).hom
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U).ι h) =
    CategoryTheory.CategoryStruct.comp U.ι (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.map_mapRingHom_evalEval : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : Polynomial (Polynomial R))
  (x y : R),
  Polynomial.evalEval (f x) (f y) (Polynomial.map (Polynomial.mapRingHom f) p) = f (Polynomial.evalEval x y p)
-- Mathlib.Data.List.Basic
List.disjoint_reverse_right : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.Disjoint l₂.reverse ↔ l₁.Disjoint l₂
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- `LinearMap.normDet` of a linear isometry is 1.
 -/
LinearIsometry.normDet_eq_one : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] (f : U →ₗᵢ[𝕜] V), f.normDet = 1
-- Mathlib.Data.Setoid.Partition
/-- The empty set is not an equivalence class.  -/
Setoid.empty_notMem_classes : ∀ {α : Type u_1} {r : Setoid α}, ∅ ∉ r.classes
-- Lean.Meta.Sym.Arith.Poly
/-- Returns the S-polynomial of polynomials `p₁` and `p₂`, and coefficients&terms used to construct it.
Given polynomials with leading terms `k₁*m₁` and `k₂*m₂`, the S-polynomial is defined as:
```
S(p₁, p₂) = (k₂/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₁) * p₁ - (k₁/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₂) * p₂
```
Remark: if `char? = some c`, then `c` is the characteristic of the ring.
 -/
Lean.Grind.CommRing.Poly.spol : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → optParam (Option ℕ) none → Lean.Grind.CommRing.SPolResult
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instCommRing : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [CommRing R] → CommRing (l.Germ R)
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.NonnegCoeffs.nil : Lean.Grind.Linarith.Poly.nil.NonnegCoeffs
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientEquivAlgOfEq_mk : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I J : Ideal A}
  [inst_3 : I.IsTwoSided] [inst_4 : J.IsTwoSided] (h : I = J) (x : A),
  (Ideal.quotientEquivAlgOfEq R₁ h) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) x
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.quasiMeasurePreserving_inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving Inv.inv μ μ
-- Lean.Linter.UnusedVariables
/-- Collects into `fvarUses` all `fvar`s occurring in the `Expr`s in `assignments`.
This implementation respects subterm sharing in both the `PersistentHashMap` and the `Expr`
to ensure that pointer-equal subobjects are not visited multiple times, which is important
in practice because these expressions are very frequently highly shared.
 -/
Lean.Linter.UnusedVariables.visitAssignments : IO.Ref (Std.HashSet USize) →
  IO.Ref (Std.HashSet Lean.FVarId) → Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr) → IO Unit
-- Mathlib.Topology.Bornology.BoundedOperation
boundedSub_of_lipschitzWith_sub : ∀ {R : Type u_1} [inst : PseudoMetricSpace R] [inst_1 : Sub R] {K : NNReal},
  (LipschitzWith K fun p => p.1 - p.2) → BoundedSub R
-- Mathlib.Algebra.Group.Subgroup.Map
/-- The image under an `AddMonoid` hom of the `AddSubgroup` generated by a set equals
the `AddSubgroup` generated by the image of the set.  -/
AddMonoidHom.map_closure : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (s : Set G),
  AddSubgroup.map f (AddSubgroup.closure s) = AddSubgroup.closure (⇑f '' s)
-- Mathlib.Topology.Algebra.Group.Torsor
IsTopologicalTorsor.continuous_sdiv : ∀ {V : Type u_1} {inst : Group V} {inst_1 : TopologicalSpace V} {P : Type u_2} {inst_2 : Torsor V P}
  {inst_3 : TopologicalSpace P} [self : IsTopologicalTorsor P], Continuous fun x => x.1 /ₛ x.2
-- Mathlib.Order.Defs.PartialOrder
/-- `WCovBy a b` means that `a = b` or `b` covers `a`.
This means that `a ≤ b` and there is no element in between. This is denoted `a ⩿ b`.
 -/
«term_⩿_» : Lean.TrailingParserDescr
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess.0.Finset.orderEmbOfFinWithBot_zero : ∀ {T : Type u_1} [inst : LinearOrder T] (I : Finset T) [inst_1 : Bot T], Finset.orderEmbOfFinWithBot✝ I 0 = ⊥
-- Init.Data.List.Lemmas
List.map_singleton : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α}, List.map f [a] = [f a]
-- Lean.Meta.Tactic.Grind.Action
_private.Lean.Meta.Tactic.Grind.Action.0.Lean.Meta.Grind.Action.skipIfNA.eq_1 : ∀ (x : Lean.Meta.Grind.Action) (goal : Lean.Meta.Grind.Goal) (x_1 kp : Lean.Meta.Grind.ActionCont),
  x.skipIfNA goal x_1 kp = x goal kp kp
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS₂_zero : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), complEDS₂ b c d 0 = 2
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_sshiftRight : ∀ {w : ℕ} {x : BitVec w} {i n : ℕ},
  (x.sshiftRight n).getMsbD i = (decide (i < w) && if i < n then x.msb else x.getMsbD (i - n))
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.isOpen_ofLowerSet_preimage : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsOpen (⇑Topology.WithLowerSet.ofLowerSet ⁻¹' s) ↔ IsLowerSet s
-- Init.Data.Vector.Basic
Vector.mapFinIdxM.map : {n : ℕ} →
  {α : Type u} →
    {β : Type v} →
      {m : Type v → Type w} →
        [Monad m] → Vector α n → ((i : ℕ) → α → i < n → m β) → (i j : ℕ) → i + j = n → Vector β (n - i) → m (Vector β n)
-- Mathlib.Algebra.Category.Ring.Colimits
/-- An inductive type representing all commutative ring expressions (without Relations)
on a collection of types indexed by the objects of `J`.
 -/
CommRingCat.Colimits.Prequotient : {J : Type v} → [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J CommRingCat → Type v
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndep_zero_right : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {m : ι → MeasurableSpace Ω}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}, ProbabilityTheory.Kernel.iIndep m κ 0
-- Lean.Data.Lsp.Basic
/-- The string to be inserted. For delete operations use an empty string.  -/
Lean.Lsp.TextEdit.newText : Lean.Lsp.TextEdit → String
-- Lean.Elab.Term.TermElabM
/-- If `mayPostpone == true`, throw `Exception.postpone`.  -/
Lean.Elab.Term.tryPostpone : Lean.Elab.TermElabM Unit
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- Relationship between the Fibonacci Sequence, the golden ratio, and its exponents.  -/
Real.goldenRatio_mul_fib_succ_add_fib : ∀ (n : ℕ), Real.goldenRatio * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = Real.goldenRatio ^ (n + 1)
-- Init.Data.List.TakeDrop
List.take_append_drop : ∀ {α : Type u_1} (i : ℕ) (l : List α), List.take i l ++ List.drop i l = l
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.Represents.algebraMap : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] {R : Type u_3} [inst_2 : CommRing R]
  [inst_3 : Module R M] {b : ι → M} [inst_4 : DecidableEq ι] (r : R),
  Matrix.Represents b ((algebraMap R (Matrix ι ι R)) r) ((algebraMap R (Module.End R M)) r)
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.eq_inv_iff_mul_eq_one : ∀ {k : Type u_2} [inst : Field k] {φ ψ : PowerSeries k}, PowerSeries.constantCoeff ψ ≠ 0 → (φ = ψ⁻¹ ↔ φ * ψ = 1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).getKey k ⋯ = k
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instIsLeftCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsLeftCancelMul α], IsLeftCancelMul (Lex α)
-- Mathlib.Topology.Connected.PathConnected
ZerothHomotopy.lift_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X] {T : Type u_4} (f : X → T) (hf : ∀ ⦃x y : X⦄ (x_1 : Path x y), f x = f y)
  (x : X), ZerothHomotopy.lift f hf (ZerothHomotopy.mk x) = f x
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n+1`-th iterated derivative can be obtained by taking the `n`-th derivative of the
derivative.  -/
iteratedDeriv_succ' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F}, iteratedDeriv (n + 1) f = iteratedDeriv n (deriv f)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Uniform structure of `𝔖`-convergence, i.e uniform convergence on the elements of `𝔖`,
declared as an instance on `α →ᵤ[𝔖] β`. It is defined as the infimum, for `S ∈ 𝔖`, of the pullback
by `S.domRestrict`, the map of restriction to `S`, of the uniform structure `𝒰(s, β, uβ)` on
`↥S →ᵤ β`. We will denote it `𝒱(α, β, 𝔖, uβ)`, where `uβ` is the uniform structure on `β`.  -/
UniformOnFun.uniformSpace : (α : Type u_1) → (β : Type u_2) → [UniformSpace β] → (𝔖 : Set (Set α)) → UniformSpace (UniformOnFun α β 𝔖)
-- Mathlib.Analysis.Normed.Ring.Basic
MulOpposite.instNormedCommRing : {α : Type u_2} → [NormedCommRing α] → NormedCommRing αᵐᵒᵖ
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_comp_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (g : P →ₗ[R] Q)
  (f : N →ₗ[R] P) (x : TensorProduct R M N),
  (LinearMap.lTensor M (g ∘ₗ f)) x = (LinearMap.lTensor M g) ((LinearMap.lTensor M f) x)
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.divInt_le_divInt : ∀ {a b c d : ℤ}, 0 < b → 0 < d → (Rat.divInt a b ≤ Rat.divInt c d ↔ a * d ≤ c * b)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.EIsoH_hom_opcyclesIsoH_inv_assoc : ∀ {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.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂) {i j : ι}
  (f : i ⟶ j) {Z : C} (h : X.opcycles f (CategoryTheory.CategoryStruct.id j) n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.EIsoH f n₀ n₁ n₂ hn₁ hn₂).hom
      (CategoryTheory.CategoryStruct.comp (X.opcyclesIsoH f n₀ n₁ hn₁).inv h) =
    CategoryTheory.CategoryStruct.comp
      (X.ιE (CategoryTheory.CategoryStruct.id i) f (CategoryTheory.CategoryStruct.id j) n₀ n₁ n₂ hn₁ hn₂) h
-- Mathlib.Algebra.DirectSum.Internal
multisetProd_apply_eq_zero : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : AddCommMonoid ι] [inst_1 : LinearOrder ι] [IsOrderedAddMonoid ι]
  [inst_3 : DecidableEq ι] [CanonicallyOrderedAdd ι] [inst_5 : CommSemiring R] [inst_6 : SetLike σ R]
  [inst_7 : AddSubmonoidClass σ R] {A : ι → σ} [inst_8 : SetLike.GradedMonoid A]
  {s : Multiset (DirectSum ι fun i => ↥(A i))} {m : ι},
  (∀ x ∈ s, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < s.card • m → s.prod n = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} [inst_1 : Inhabited (β k')],
      List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l → ⟨k, v⟩ ∈ l → (t.insertMany l).get! k' = cast ⋯ v
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometry.lTensor_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : F →ₗᵢ[𝕜] G) (x : TensorProduct 𝕜 E F),
  (LinearIsometry.lTensor E f) x = (LinearMap.lTensor E f.toLinearMap) x
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vaddCommClass_set : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α γ] [inst_1 : VAdd β γ] [VAddCommClass α β γ],
  VAddCommClass α β (Set γ)
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.coe_mk : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {c : RingCon R}, ↑(TwoSidedIdeal.mk c) = {x | c x 0}
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_insert_le_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (cmp ((t.insert k v).minKey ⋯) k).isLE = true
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.exists_rat_eq_nth_num : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K) (n : ℕ),
  ∃ q, (GenContFract.of v).nums n = ↑q
-- Mathlib.Data.Set.Function
Set.SurjOn.union_union : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.SurjOn f s₁ t₁ → Set.SurjOn f s₂ t₂ → Set.SurjOn f (s₁ ∪ s₂) (t₁ ∪ t₂)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.relabel_id : ∀ {L : FirstOrder.Language} {α : Type u'} (t : L.Term α), FirstOrder.Language.Term.relabel id t = t
-- Mathlib.Analysis.Convex.Extreme
isExtreme_iff : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] (A B : Set E),
  IsExtreme 𝕜 A B ↔ B ⊆ A ∧ ∀ ⦃x : E⦄, x ∈ A → ∀ ⦃y : E⦄, y ∈ A → ∀ ⦃z : E⦄, z ∈ B → z ∈ openSegment 𝕜 x y → x ∈ B
-- Init.Data.Array.Lex.Lemmas
Array.append_left_lt : ∀ {α : Type u_1} [inst : LT α] {xs ys zs : Array α}, ys < zs → xs ++ ys < xs ++ zs
-- Init.Data.UInt.Lemmas
USize.toFin_toUInt64 : ∀ (n : USize), n.toUInt64.toFin = Fin.castLE USize.size_le_uint64Size n.toFin
-- Mathlib.Topology.Algebra.MulAction
ContinuousAt.smul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} {b : Y},
  ContinuousAt f b → ContinuousAt g b → ContinuousAt (f • g) b
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.associated_den_num_inv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K),
  x ≠ 0 → Associated (↑(IsFractionRing.den A x)) (IsFractionRing.num A x⁻¹)