mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Int
Vector.prod_eq_foldl_int : ∀ {n : ℕ} {xs : Vector ℤ n}, xs.prod = Vector.foldl (fun x1 x2 => x1 * x2) 1 xs
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
/-- Recursively defines the sequence of coefficients for the inverse to a Witt vector whose first entry
is a unit.
 -/
WittVector.inverseCoeff : {p : ℕ} → [hp : Fact (Nat.Prime p)] → {k : Type u_1} → [inst : CommRing k] → [CharP k p] → kˣ → WittVector p k → ℕ → k
-- Mathlib.Control.Functor
/-- If `f` is a functor, if `fb : f β` and `a : α`, then `mapConstRev fb a` is the result of
applying `f.map` to the constant function `β → α` sending everything to `a`, and then
evaluating at `fb`. In other words it's `const a <$> fb`.  -/
Functor.mapConstRev : {f : Type u → Type v} → [Functor f] → {α β : Type u} → f β → α → f α
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.comp.eq_4 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithInitial C) (_Y : C),
  CategoryTheory.WithInitial.comp = fun f _g => PEmpty.elim f
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instStarModule : ∀ {n : Type u_2} {R : Type u_3} {A : Type u_5} [inst : Star R] [inst_1 : Star A] [inst_2 : SMul R A] [StarModule R A],
  StarModule R (CStarMatrix n n A)
-- Mathlib.Topology.Instances.PNat
PNat.isUniformEmbedding_coe : IsUniformEmbedding PNat.val
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.safeRule : Aesop.SafeRule → Aesop.BaseRuleSetMember
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.contains (t.minKeyD fallback) = true
-- Init.Data.String.Lemmas.Intercalate
String.intercalate_nil : ∀ {s : String}, s.intercalate [] = ""
-- Std.Sync.SharedMutex
_private.Std.Sync.SharedMutex.0.Std.SharedMutex.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (ref : IO.Ref α) (mutex : Std.BaseSharedMutex),
  sizeOf { ref := ref, mutex := mutex } = 1 + sizeOf ref + sizeOf mutex
-- Plausible.Sampleable
Plausible.NoShrink.arbitrary : {α : Type u_1} → [arb : Plausible.Arbitrary α] → Plausible.Arbitrary (Plausible.NoShrink α)
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_ofNat : ∀ {a b n : ℕ} [inst : n.AtLeastTwo],
  emultiplicity a b = OfNat.ofNat n ↔ a ^ OfNat.ofNat n ∣ b ∧ ¬a ^ (OfNat.ofNat n + 1) ∣ b
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.disjoint_val_image : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α}
  {t : Set ↥(SubAddAction.ofFixingAddSubgroup M s)}, Disjoint s (Subtype.val '' t)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.monic_X : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.Monic
-- Mathlib.Data.Finset.Basic
Finset.disjoint_disjUnion_left : ∀ {α : Type u_1} {s t u : Finset α} (h : Disjoint s t), Disjoint (s.disjUnion t h) u ↔ Disjoint s u ∧ Disjoint t u
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.map_comp_bijective_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X Y : C} (f : X ⟶ Y) (Z : D),
  (Function.Bijective fun g => CategoryTheory.CategoryStruct.comp (F.map f) g) ↔
    Function.Bijective fun g => CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Data.Setoid.Basic
/-- Given a map f from α to β, the natural map from the quotient of α by the kernel of f is
injective.  -/
Setoid.kerLift_injective : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Function.Injective (Setoid.kerLift f)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concatRecAux.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1}
  (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil)
  (Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)) {u : V},
  SimpleGraph.Walk.concatRecAux Hnil Hconcat SimpleGraph.Walk.nil = Hnil
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
PowerBasis.ofAdjoinEqTop'_dim : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : Algebra R S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree R S] {x : S}
  (hx : IsIntegral R x) (hx' : R[x] = ⊤), (PowerBasis.ofAdjoinEqTop' hx hx').dim = (minpoly R x).natDegree
-- Mathlib.Data.Nat.Factorial.Basic
_private.Mathlib.Data.Nat.Factorial.Basic.0.Nat.factorial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Order.Heyting.Basic
/-- Transfer `HeytingAlgebra` across an `Equiv`.  -/
Equiv.heytingAlgebra : {α : Type u_2} → {β : Type u_3} → α ≃ β → [HeytingAlgebra β] → HeytingAlgebra α
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_subsingleton : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Subsingleton R]
  (p : Submodule R M), p.spanRank = 0
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.toMulEquiv_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β],
  Function.Injective OrderMonoidIso.toMulEquiv
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.integral_congr : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {c : ℂ} {R : ℝ},
  0 ≤ R → Set.EqOn f g (Metric.sphere c R) → ∮ (z : ℂ) in C(c, R), f z = ∮ (z : ℂ) in C(c, R), g z
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `LocallyPathConnectedSpace`.

---

A topological space is locally path connected if, at every point, path connected
neighborhoods form a neighborhood basis.  -/
LocPathConnectedSpace : (X : Type u_4) → [TopologicalSpace X] → Prop
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.union_eq_unionₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.union m₂ = m₁.unionₘ m₂
-- Init.Data.String.Search
/-- Returns the first character in `s`. If `s = ""`, returns `(default : Char)`.

Examples:

* `"abc".front = 'a'`

* `"".front = (default : Char)`
 -/
String.front : String → Char
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_inter_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioo b a ∩ Set.Ioi c = Set.Ioo (max b c) a
-- Lean.Meta.Sym.SymM
_private.Lean.Meta.Sym.SymM.0.Lean.Meta.Sym.SymExtension.getStateCoreImpl : {σ : Type} → Lean.Meta.Sym.SymExtension σ → Array Lean.Meta.Sym.SymExtensionState → IO σ
-- Mathlib.Data.Multiset.Fold
/-- `fold op b s` folds a commutative associative operation `op` over
the multiset `s`.  -/
Multiset.fold : {α : Type u_1} → (op : α → α → α) → [hc : Std.Commutative op] → [ha : Std.Associative op] → α → Multiset α → α
-- Mathlib.Algebra.Divisibility.Basic
/-- **Alias** of `dvd_pow`. -/
Dvd.dvd.pow : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a ∣ b → ∀ {n : ℕ}, n ≠ 0 → a ∣ b ^ n
-- Mathlib.NumberTheory.Chebyshev
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.c : ℝ → ℕ → ℝ
-- Mathlib.Data.EReal.Basic
EReal.natCast_mul : ∀ (m n : ℕ), ↑(m * n) = ↑m * ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.lift_fst_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.instUniqueCarrierObjTopCatToTop₀MkOfNatNat : Unique ↑(SimplexCategory.toTop₀.obj { len := 0 })
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.range_inr : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W},
  Representation.IntertwiningMap.range σ (ρ.prod σ) (Representation.IntertwiningMap.inr A ρ σ) =
    Representation.IntertwiningMap.ker (ρ.prod σ) ρ (Representation.IntertwiningMap.fst A ρ σ)
-- Mathlib.Algebra.Module.Projective
Module.Projective.directSum_iff : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)],
  Module.Projective R (DirectSum ι fun i => M i) ↔ ∀ (i : ι), Module.Projective R (M i)
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.id_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (x : CategoryTheory.SpectralSequence C c r₀) (x_1 : ℤ) (x_2 : r₀ ≤ x_1),
  (CategoryTheory.CategoryStruct.id x).hom x_1 x_2 = CategoryTheory.CategoryStruct.id (x.page x_1 ⋯)
-- Mathlib.Analysis.Calculus.Deriv.Prod
hasDerivWithinAt_finCons : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {n : ℕ} {F' : Fin n.succ → Type u_1}
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : 𝕜 → F' 0} {φs : 𝕜 → (i : Fin n) → F' i.succ} {φ' : (i : Fin n.succ) → F' i},
  HasDerivWithinAt (fun x => Fin.cons (φ x) (φs x)) φ' s x ↔
    HasDerivWithinAt φ (φ' 0) s x ∧ HasDerivWithinAt φs (fun i => φ' i.succ) s x
-- Mathlib.GroupTheory.Coset.Basic
/-- If `s ≤ t`, then there is a map `α ⧸ s → α ⧸ t`.  -/
AddSubgroup.quotientMapOfLE : {α : Type u_1} → [inst : AddGroup α] → {s t : AddSubgroup α} → s ≤ t → α ⧸ s → α ⧸ t
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsUniformAddGroup.cauchy_map_iff_tendsto : ∀ {ι : Type u_3} {G : Type u_4} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] (𝓕 : Filter ι)
  (f : ι → G), Cauchy (Filter.map f 𝓕) ↔ 𝓕.NeBot ∧ Filter.Tendsto (fun p => f p.1 - f p.2) (𝓕 ×ˢ 𝓕) (nhds 0)
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- For vector spaces, `f.dualMap` is surjective if and only if `f` is injective  -/
LinearMap.dualMap_surjective_iff : ∀ {K : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V₁ →ₗ[K] V₂},
  Function.Surjective ⇑f.dualMap ↔ Function.Injective ⇑f
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.instIsLocallyFreeFree : ∀ {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]
  [inst_3 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] [CategoryTheory.Limits.HasBinaryProducts C]
  [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (I : Type u),
  (SheafOfModules.free I).IsLocallyFree
-- Mathlib.Topology.Algebra.Group.Basic
instIsTopologicalGroupMultiplicativeOfIsTopologicalAddGroup : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G],
  IsTopologicalGroup (Multiplicative G)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.adjugate : ∀ {α : Type u_1} {m : Type u_3} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype m] [inst_3 : DecidableEq m]
  {A : Matrix m m α}, A.IsHermitian → A.adjugate.IsHermitian
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eq_some_getValue! : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] {l : List ((_ : α) × β)} {a : α},
  Std.Internal.List.containsKey a l = true → Std.Internal.List.getValue? a l = some (Std.Internal.List.getValue! a l)
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.Context.maxDepth? : Aesop.RuleTac.ForwardM.Context → Option ℕ
-- Std.Data.Internal.List.Associative
Std.Internal.List.foldrM_eq_foldrM_toProd' : ∀ {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m']
  {l : List ((_ : α) × β)} {f : δ → α → β → m' δ} {init : δ},
  List.foldrM (fun a b => f b a.fst a.snd) init l =
    List.foldrM (fun a b => f b a.1 a.2) init (List.map (fun x => (x.fst, x.snd)) l)
-- Mathlib.Computability.Primrec.List
/-- Bounded existential quantifiers are primitive recursive.  -/
PrimrecPred.exists_lt : ∀ {p : ℕ → Prop}, PrimrecPred p → PrimrecPred fun n => ∃ x < n, p x
-- Mathlib.LinearAlgebra.Basis.MulOpposite
/-- The multiplicative opposite of a basis: `b.mulOpposite i ↦ op (b i)`.  -/
Module.Basis.mulOpposite : {R : Type u_1} →
  {H : Type u_2} →
    {ι : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid H] → [inst_2 : Module R H] → Module.Basis ι R H → Module.Basis ι R Hᵐᵒᵖ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α} {h : k ∈ Std.ExtTreeMap.filterMap f t},
  (Std.ExtTreeMap.filterMap f t)[k] = (f (t.getKey k ⋯) t[k]).get ⋯
-- Init.Prelude
/-- Applies a function to the current state that both computes a new state and a value. The new state
replaces the current state, and the value is returned.

It is equivalent to `do let (a, s) := f (← get); set s; pure a`. However, using `modifyGet` may
lead to higher performance because it doesn't add a new reference to the state value. Additional
references can inhibit in-place updates of data.
 -/
MonadState.modifyGet : {σ : outParam (Type u)} → {m : Type u → Type v} → [self : MonadState σ m] → {α : Type u} → (σ → α × σ) → m α
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.curry₂.inj : ∀ {ak : Mathlib.Tactic.ITauto.AndKind} {p q : Mathlib.Tactic.ITauto.Proof} {ak_1 : Mathlib.Tactic.ITauto.AndKind}
  {p_1 q_1 : Mathlib.Tactic.ITauto.Proof},
  Mathlib.Tactic.ITauto.Proof.curry₂ ak p q = Mathlib.Tactic.ITauto.Proof.curry₂ ak_1 p_1 q_1 →
    ak = ak_1 ∧ p = p_1 ∧ q = q_1
-- Mathlib.Analysis.Convex.StdSimplex
/-- The barycenter of a standard simplex is the center of mass of
the set of vertices (equally weighted).  -/
stdSimplex.barycenter : {X : Type u_2} →
  [inst : Fintype X] →
    {𝕜 : Type u_5} →
      [inst_1 : Field 𝕜] → [inst_2 : LinearOrder 𝕜] → [IsStrictOrderedRing 𝕜] → [Nonempty X] → ↑(stdSimplex 𝕜 X)
-- Init.Data.Range.Polymorphic.UInt
UInt16.rxcHasSize_eq_toBitVec : ∀ {lo : BitVec 16} {hi : UInt16}, Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instAdd : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] → [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → Add (SchwartzMap E F)
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedOrderRingHom_toFun : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Field β] [inst_4 : ConditionallyCompleteLinearOrder β] [inst_5 : IsStrictOrderedRing β]
  [inst_6 : Archimedean α] (a : α),
  (ConditionallyCompleteLinearOrderedField.inducedOrderRingHom α β) a =
    (ConditionallyCompleteLinearOrderedField.inducedAddHom α β) a
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.coevaluation_comp_leftAdjointMate_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y] (f : X ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (ᘁX) Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (η_ (ᘁY) Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (ᘁf) Y) h) =
    CategoryTheory.CategoryStruct.comp (η_ (ᘁX) X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (ᘁX) f) h)
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.Homotopy.smul_h₀ : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R), (h.smul a).h₀ = a • h.h₀
-- Mathlib.Order.GaloisConnection.Basic
/-- `toDual ∘ Ici` and `sInf ∘ ofDual` form a Galois coinsertion.  -/
gciIciSInf : {α : Type u} →
  [inst : CompleteSemilatticeInf α] → GaloisCoinsertion (⇑OrderDual.toDual ∘ Set.Ici) (sInf ∘ ⇑OrderDual.ofDual)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.mk.sizeOf_spec : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : SizeOf R] [inst_8 : SizeOf A] [inst_9 : SizeOf B] (toAlgEquiv : A ≃ₐ[R] B)
  (continuous_toFun : autoParam (Continuous toAlgEquiv.toFun) Homeomorph.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toAlgEquiv.invFun) Homeomorph.continuous_invFun._autoParam),
  sizeOf { toAlgEquiv := toAlgEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
    1 + sizeOf toAlgEquiv + sizeOf continuous_toFun + sizeOf continuous_invFun
-- Lean.Linter.Init
Lean.Linter.instEmptyCollectionLinterSets : EmptyCollection Lean.Linter.LinterSets
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.app_invApp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace) {Z : C}
  (h :
    Y.presheaf.obj
        (Opposite.op
          ((AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor f).obj
            ((TopologicalSpace.Opens.map f.hom.base).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (f.hom.c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.hom.base).obj U)) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_union_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (contains_right : k ∈ m₂), (m₁ ∪ m₂)[k] = m₂[k]
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.mul_right : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s t : Set α},
  IsLowerSet s → IsLowerSet (s * t)
-- Qq.Match
Qq.Impl.elabPat : Lean.Term →
  Lean.LocalContext →
    Lean.LocalInstances →
      Lean.Expr → List Lean.Name → Lean.Elab.TermElabM (Lean.Expr × Array Lean.LocalDecl × Array Lean.Name)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCoseparating.of_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsCoseparating → ∀ {Q : CategoryTheory.ObjectProperty C}, P ≤ Q → Q.IsCoseparating
-- Mathlib.Data.Finset.Card
/-- A three-element finset `{a, b, c}` has cardinality `3` iff `a`, `b`, `c` are pairwise
distinct.  -/
Finset.card_triple_eq_three_iff : ∀ {α : Type u_1} {a b c : α} [inst : DecidableEq α], {a, b, c}.card = 3 ↔ a ≠ b ∧ a ≠ c ∧ b ≠ c
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.isCompact_closedBall : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {x : E}
  {r : ℝ}, IsCompact (Euclidean.closedBall x r)
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_iUnion : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  {ι : Sort u_3} (f : ι → Set M), N.colon (⋃ i, f i) = ⨅ i, N.colon (f i)
-- Init.Data.List.Count
List.countP_cons_of_pos : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, p a = true → List.countP p (a :: l) = List.countP p l + 1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.stRun.match_1.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_3} {k : K} (motive : Turing.TM2to1.StAct K Γ σ k → Sort u_4)
  (f : σ → Option (Γ k) → σ) (h_1 : (f : σ → Γ k) → motive (Turing.TM2to1.StAct.push f))
  (h_2 : (f : σ → Option (Γ k) → σ) → motive (Turing.TM2to1.StAct.peek f))
  (h_3 : (f : σ → Option (Γ k) → σ) → motive (Turing.TM2to1.StAct.pop f)),
  (match Turing.TM2to1.StAct.peek f with
    | Turing.TM2to1.StAct.push f => h_1 f
    | Turing.TM2to1.StAct.peek f => h_2 f
    | Turing.TM2to1.StAct.pop f => h_3 f) =
    h_2 f
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.lift_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : CategoryTheory.Functor C (Type w)}
  (φ : G ⟶ A.toFunctor) (w : CategoryTheory.CategoryStruct.comp φ f = CategoryTheory.CategoryStruct.comp φ g)
  {Z : CategoryTheory.Functor C (Type w)} (h : A.toFunctor ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.lift f g φ w)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subfunctor.equalizer.ι f g) h) =
    CategoryTheory.CategoryStruct.comp φ h
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.compLeftAddMonoidHom.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} (N : Type u_6) [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {E'' : Type u_7} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E''] {H'' : Type u_8}
  [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {n : WithTop ℕ∞} {G' : Type u_10}
  [inst_12 : AddMonoid G'] [inst_13 : TopologicalSpace G'] [inst_14 : ChartedSpace H' G']
  [inst_15 : ContMDiffAdd I' n G'] {G'' : Type u_11} [inst_16 : AddMonoid G''] [inst_17 : TopologicalSpace G'']
  [inst_18 : ChartedSpace H'' G''] [inst_19 : ContMDiffAdd I'' n G''] (φ : G' →+ G'') (hφ : ContMDiff I' I'' n ⇑φ),
  ContMDiffMap.compLeftAddMonoidHom I N φ hφ = { toFun := fun f => ⟨⇑φ ∘ ⇑f, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_union_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₂ = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) = true},
  Std.DTreeMap.Internal.Impl.Const.get (m₁.union m₂ ⋯ ⋯) k h' = Std.DTreeMap.Internal.Impl.Const.get m₁ k ⋯
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Auxiliary function for `RefinedDiscrTree.format`.  -/
Lean.Meta.RefinedDiscrTree.format.go : {α : Type} → [Std.ToFormat α] → Lean.Meta.RefinedDiscrTree α → Lean.Meta.RefinedDiscrTree.TrieIndex → Std.Format
-- Std.Http.Server
/-- The context used for shutting down all connections and the server.
 -/
Std.Http.Server.context : Std.Http.Server → Std.CancellationContext
-- Mathlib.SetTheory.Lists
/-- Converts a `List` of ZFA lists to a proper ZFA prelist.  -/
Lists'.ofList : {α : Type u_1} → List (Lists α) → Lists' α true
-- Mathlib.Algebra.Ring.Commute
Commute.lie_eq : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {x y : R}, Commute x y → ⁅x, y⁆ = 0