mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Defs
/-- Distributivity of `+ᵥ` across `+`  -/
AddDistribAddAction.vadd_add : ∀ {M : Type u_9} {N : Type u_10} {inst : AddMonoid M} {inst_1 : AddMonoid N} [self : AddDistribAddAction M N] (r : M)
  (x y : N), r +ᵥ x + y = (r +ᵥ x) + (r +ᵥ y)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.neg_iff : ∀ {p x : ℝ}, LiouvilleWith p (-x) ↔ LiouvilleWith p x
-- ProofWidgets.Component.RefreshComponent
_private.ProofWidgets.Component.RefreshComponent.0.ProofWidgets.RefreshToken.mk.inj : ∀ {state : IO.Ref ProofWidgets.RefreshComponent.RefreshState} {cancelTk : IO.CancelToken}
  {promise : IO.Ref (IO.Promise Unit)} {state_1 : IO.Ref ProofWidgets.RefreshComponent.RefreshState}
  {cancelTk_1 : IO.CancelToken} {promise_1 : IO.Ref (IO.Promise Unit)},
  { state := state, cancelTk := cancelTk, promise := promise } =
      { state := state_1, cancelTk := cancelTk_1, promise := promise_1 } →
    state = state_1 ∧ cancelTk = cancelTk_1 ∧ promise = promise_1
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.isLocalHom_algebraMap : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] [IsLocalHom (algebraMap R A)], IsLocalHom (algebraMap R (AddMonoidAlgebra A M))
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.head_lt_ord_of_isGood : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] [inst_2 : Inhabited I]
  {l : Profinite.NobelingProof.Products I} {o : Ordinal.{u}},
  Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) l →
    ↑l ≠ [] → Profinite.NobelingProof.ord I (↑l).head! < o
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumCongr_symm : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6}
  [inst_2 : TopologicalSpace X'] [inst_3 : TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y'),
  (h₁.sumCongr h₂).symm = h₁.symm.sumCongr h₂.symm
-- Init.Data.Int.OfNat
Nat.ToInt.of_dvd : ∀ (d a : ℕ) (d' a' : ℤ), ↑d = d' → ↑a = a' → d ∣ a → d' ∣ a'
-- Mathlib.Data.Set.Subsingleton
Set.monotoneOn_singleton : ∀ {α : Type u} {β : Type v} {a : α} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β), MonotoneOn f {a}
-- Lean.Language.Basic
/-- Creates snapshot message log from non-interactive message log, also allocating a mutable cell
that can be used by the server to memorize interactive diagnostics derived from the log.
 -/
Lean.Language.Snapshot.Diagnostics.ofMessageLog : Lean.MessageLog → BaseIO Lean.Language.Snapshot.Diagnostics
-- Mathlib.RingTheory.PowerBasis
/-- Construct a power basis from a basis consisting of powers of an element.
 -/
Module.Basis.PowerBasis : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_7} →
            [inst_3 : Fintype ι] →
              (B : Module.Basis ι R S) →
                {x : S} → (e : ι ≃ Fin (Fintype.card ι)) → (∀ (i : ι), B i = x ^ ↑(e i)) → PowerBasis R S
-- Mathlib.LinearAlgebra.Projection
Submodule.projection_apply_eq_zero_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) {x : E}, (p.projection q hpq) x = 0 ↔ x ∈ q
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α}, m.contains a = false → m.get? a = none
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
LinearMap.mkContinuous_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Ring 𝕜] [inst_1 : Ring 𝕜₂]
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜₂ F]
  {σ : 𝕜 →+* 𝕜₂} (f : E →ₛₗ[σ] F) (C : ℝ) (h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) (x : E), (f.mkContinuous C h) x = f x
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inverseAssociator_map_inr_inl : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : D} (f : X ⟶ Y),
  (CategoryTheory.sum.inverseAssociator C D E).map
      ((CategoryTheory.Sum.inr_ C (D ⊕ E)).map ((CategoryTheory.Sum.inl_ D E).map f)) =
    (CategoryTheory.Sum.inl_ (C ⊕ D) E).map ((CategoryTheory.Sum.inr_ C D).map f)
-- Mathlib.Util.Export
Lean.Export.runExportM : {α : Type} → Lean.ExportM α → Lean.CoreM α
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLT_iff_getElem_lt_getElem_of_lt`. -/
List.SortedLT.getElem_lt_getElem_of_lt : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  l.SortedLT → ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i < j → l[i] < l[j]
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.isSt_st : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r → x.IsSt x.st
-- Lean.Server.Completion.CompletionInfoSelection
_private.Lean.Server.Completion.CompletionInfoSelection.0.Lean.Server.Completion.computePrioritizedCompletionPartitions : Array (Lean.Server.Completion.ContextualizedCompletionInfo × ℕ) →
  Array (Array (Lean.Server.Completion.ContextualizedCompletionInfo × ℕ))
-- Mathlib.Topology.Covering.AddCircle
AddCircle.isAddQuotientCoveringMap_zsmul_of_ne_zero : ∀ {𝕜 : Type u_1} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)]
  [Algebra ℚ 𝕜] (n : ℤ) [NeZero n], IsAddQuotientCoveringMap (fun x => n • x) ↥(zsmulAddGroupHom n).ker
-- Lean.Expr
_private.Lean.Expr.0.Lean.intDivFn : Lean.Expr
-- Mathlib.Analysis.Normed.Operator.Completeness
ContinuousLinearMap.ofTendstoOfBoundedRange_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6}
  [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂] {α : Type u_7}
  {l : Filter α} [inst_7 : l.NeBot] (f : E' → F) (g : α → E' →SL[σ₁₂] F)
  (hf : Filter.Tendsto (fun a x => (g a) x) l (nhds f)) (hg : Bornology.IsBounded (Set.range g)),
  ⇑(ContinuousLinearMap.ofTendstoOfBoundedRange f g hf hg) = f
-- Lean.Expr
Lean.ExprStructMap : Type → Type
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_toPartialHomeomorph : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y'),
  (eX.prod eY).toPartialHomeomorph =
    { toPartialEquiv := eX.prod eY.toPartialEquiv, continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.ComputableSmall.inflate_deflate : ∀ {α : Type v} [self : Std.Internal.ComputableSmall α] {a : α},
  Std.Internal.ComputableSmall.inflate (Std.Internal.ComputableSmall.deflate a) = a
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.isOpen_freeLocus : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FinitePresentation R M], IsOpen (Module.freeLocus R M)
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.invertiblePD : (l : Type u_4) →
  (R : Type u₂) →
    [inst : DecidableEq l] →
      [inst_1 : CommRing R] → [inst_2 : Fintype l] → [Invertible 2] → Invertible (LieAlgebra.Orthogonal.PD l R)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.inl_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc f g) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Algebra.Star.StarAlgHom
/-- The right injection into a product is a non-unital algebra homomorphism.  -/
NonUnitalStarAlgHom.inr : (R : Type u_1) →
  (A : Type u_2) →
    (B : Type u_3) →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : StarAddMonoid A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] → [inst_6 : StarAddMonoid B] → B →⋆ₙₐ[R] A × B
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_erase_eq_of_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).maxKey? = t.maxKey?
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_smul' : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [inst : SMul M β] (c : α → M) (f : α → β),
  ↑(c • f) = ↑c • ↑f
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.mem_nhds_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α}, s ∈ nhds x ↔ ∃ ε > 0, Metric.eball x ε ⊆ s
-- Mathlib.Algebra.Category.Grp.Adjunctions
GrpCat.instIsRightAdjointForgetMonoidHomCarrier : (CategoryTheory.forget GrpCat).IsRightAdjoint
-- Mathlib.GroupTheory.Commutator.Basic
commutatorElement_mul_left_mul : ∀ {G : Type u_1} [inst : Group G] (a b c : G), ⁅a * b, c⁆ * ⁅c * a, b⁆ * ⁅b * c, a⁆ = 1
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (i : X ≅ X),
  ((hf.autMulEquivOfFullyFaithful X) i).inv = f.map i.inv
-- Mathlib.GroupTheory.OrderOfElement
finEquivPowers_symm_apply : ∀ {G : Type u_1} [inst : Monoid G] {x : G} (hx : IsOfFinOrder x) (n : ℕ),
  (finEquivPowers hx).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf x, ⋯⟩
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The canonical projection into the colimit, as a quotient type.  -/
GrpCat.FilteredColimits.G.mk : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J GrpCat) → (j : J) × ↑(F.obj j) → ↑(GrpCat.FilteredColimits.G F)
-- Lean.Parser.Types
/-- Create a simple parser combinator that inherits the `info` of the nested parser.  -/
Lean.Parser.withFn : (Lean.Parser.ParserFn → Lean.Parser.ParserFn) → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Analysis.Complex.Norm
Complex.norm_le_abs_re_add_abs_im : ∀ (z : ℂ), ‖z‖ ≤ |z.re| + |z.im|
-- Mathlib.Algebra.Quaternion
Quaternion.im_coe : ∀ {R : Type u_3} [inst : CommRing R] (x : R), (↑x).im = 0
-- Mathlib.Data.List.Dedup
List.dedup_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), (a :: l).dedup = if a ∈ l then l.dedup else a :: l.dedup
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.alter!.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (sz : ℕ) (k' : α)
  (v' : β) (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β) →
          (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) → motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.inner sz k' v' l' r' with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r' => h_2 sz k' v' l' r') =
    h_2 sz k' v' l' r'
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.ruleExprName : Aesop.CoreRuleBuilderOutput → Lean.Name
-- Mathlib.FieldTheory.Galois.Profinite
/-- `Gal(K/k)` as a profinite group as there is
a `ContinuousMulEquiv` to a `ProfiniteGrp` given above  -/
InfiniteGalois.profiniteGalGrp : (k : Type u_3) →
  (K : Type u_4) → [inst : Field k] → [inst_1 : Field K] → [inst_2 : Algebra k K] → [IsGalois k K] → ProfiniteGrp.{u_4}
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_real_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α) {s : Set β},
  MeasurableSet s → (κ.fst a).real s = (κ a).real {p | p.1 ∈ s}
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.tr.match_1.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      (M : Λ → Turing.TM1.Stmt Γ Λ σ) →
        (motive : Turing.TM1to0.Λ' M → Γ → Sort u_4) →
          (x : Turing.TM1to0.Λ' M) →
            (x_1 : Γ) →
              ((snd : σ) → (x : Γ) → motive (none, snd) x) →
                ((q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (s : Γ) → motive (some q, v) s) → motive x x_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Counters.mk.sizeOf_spec : ∀ (thm : Lean.PHashMap Lean.Meta.Grind.Origin ℕ) (fvarUserNames : Lean.PHashMap Lean.FVarId Lean.Name)
  (case apps : Lean.PHashMap Lean.Name ℕ),
  sizeOf { thm := thm, fvarUserNames := fvarUserNames, case := case, apps := apps } =
    1 + sizeOf thm + sizeOf fvarUserNames + sizeOf case + sizeOf apps
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- A function `f` has derivative `f'` at `z` iff `conj ∘ f ∘ conj` has derivative `conj f'` at
`conj z`.  -/
hasDerivAt_conj_conj_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜} {x f' : 𝕜},
  HasDerivAt (⇑(starRingEnd 𝕜) ∘ f ∘ ⇑(starRingEnd 𝕜)) f' x ↔ HasDerivAt f ((starRingEnd 𝕜) f') ((starRingEnd 𝕜) x)
-- Init.Data.List.Basic
List.replicate_zero : ∀ {α : Type u} {a : α}, List.replicate 0 a = []
-- Mathlib.Topology.Order
instDiscreteTopologyFin : ∀ {n : ℕ}, DiscreteTopology (Fin n)
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.HoverInfo.inside.inj : ∀ {delta delta_1 : ℕ},
  Lean.Server.Completion.HoverInfo.inside delta = Lean.Server.Completion.HoverInfo.inside delta_1 → delta = delta_1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `X` represents a presheaf of additive monoids, then `X` is an additive monoid object.  -/
CategoryTheory.AddMonObj.ofRepresentableBy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) →
        (F : CategoryTheory.Functor Cᵒᵖ AddMonCat) →
          (F.comp (CategoryTheory.forget AddMonCat)).RepresentableBy X → CategoryTheory.AddMonObj X
-- Mathlib.Data.Real.Basic
Real.mk.eq_1 : ∀ (x : CauSeq ℚ abs), Real.mk x = { cauchy := CauSeq.Completion.mk x }
-- Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
Submonoid.LocalizationMap.lift₀_def : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  {P : Type u_3} [inst_2 : CommMonoidWithZero P] (f : S.LocalizationMap N) (g : M →*₀ P)
  (hg : ∀ (y : ↥S), IsUnit (g ↑y)), ⇑(f.lift₀ g hg) = ⇑(f.lift hg)
-- Mathlib.Order.Hom.Lattice
InfHom.copy.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] (f : InfHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = { toFun := f', map_inf' := ⋯ }
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.coeff_toAdditiveBialgEquiv_apply : ∀ (R : Type u_1) (A : Type u_3) (M : Type u_8) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : Monoid M] (a : MonoidAlgebra A M),
  ((MonoidAlgebra.toAdditiveBialgEquiv R A M) a).coeff = Finsupp.mapDomain (⇑Additive.ofMul) a.coeff
-- Mathlib.Util.Notation3
/-- Matcher that assigns the current `SubExpr` into the match state;
if a value already exists, then it checks for equality.  -/
Mathlib.Notation3.matchVar : Lean.Name → Mathlib.Notation3.Matcher
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.inducedCategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      {D : Type u'} → (F : D → C) → CategoryTheory.Preadditive (CategoryTheory.InducedCategory C F)
-- Std.Data.DTreeMap.Internal.Cell
/-- Create a cell with a matching key. Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Cell.ofEq : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {k : α → Ordering} →
        (k' : α) → β k' → (∀ [Std.OrientedOrd α], k k' = Ordering.eq) → Std.DTreeMap.Internal.Cell α β k
-- Mathlib.Order.CompleteLattice.Defs
/-- Create a `CompleteLattice` from a `PartialOrder` and `InfSet`
that returns the greatest lower bound of a set. Usually this constructor provides
poor definitional equalities.  If other fields are known explicitly, they should be
provided; for example, if `inf` is known explicitly, construct the `CompleteLattice`
instance as
```
instance : CompleteLattice my_T where
  inf := better_inf
  le_inf := ...
  inf_le_right := ...
  inf_le_left := ...
  -- don't care to fix sup, sSup, bot, top
  __ := completeLatticeOfInf my_T _
```
 -/
completeLatticeOfInf : (α : Type u_8) → [H1 : PartialOrder α] → [H2 : InfSet α] → (∀ (s : Set α), IsGLB s (sInf s)) → CompleteLattice α
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Pos.revSkip?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String} {pos res : s.Pos},
  pos.revSkip? p = some res ↔ ∃ (h : pos ≠ s.startPos), res = pos.prev h ∧ p ((pos.prev h).get ⋯) = true
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.id_apply_self : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (M : CategoryTheory.Mat_ C) (i : M.ι),
  CategoryTheory.CategoryStruct.id M i i = CategoryTheory.CategoryStruct.id (M.X i)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_int_add : ∀ (f : CircleDeg1Lift) (m : ℤ) (x : ℝ), f (↑m + x) = ↑m + f x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.one? : Lean.Meta.Grind.Arith.CommRing.Ring → Option Lean.Expr
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.mem_upperCentralSeriesStep`. -/
mem_upperCentralSeriesStep : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [inst_1 : N.Normal] (x : G),
  x ∈ N.upperCentralSeriesStep ↔ ∀ (y : G), ⁅x, y⁆ ∈ N
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_of_le_mul_right₀ : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosReflectLE α],
  0 < b → b ≤ a * b → 1 ≤ a
-- Mathlib.Algebra.Order.Group.PartialSups
partialSups_const_mul : ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeSup α] [inst_1 : Group α] [inst_2 : Preorder ι]
  [inst_3 : LocallyFiniteOrderBot ι] [MulLeftMono α] (f : ι → α) (c : α) (i : ι),
  (partialSups fun x => c * f x) i = c * (partialSups f) i
-- Mathlib.Topology.Separation.Basic
disjoint_nhds_pure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X}, x ≠ y → Disjoint (nhds x) (pure y)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.keysArray.isEmpty = t.isEmpty
-- Mathlib.Geometry.Manifold.Bordism
/-- The manifold `M` is a topological space.  -/
SingularManifold.topSpaceM : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_2} →
        {H : Type u_3} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] →
                  {I : ModelWithCorners ℝ E H} → (self : SingularManifold X k I) → TopologicalSpace self.M
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- A choice of an affine open cover of a scheme.  -/
AlgebraicGeometry.Scheme.affineOpenCover : (X : AlgebraicGeometry.Scheme) → X.AffineOpenCover
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.sum_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} {ι : Type u'}
  (f : ι → (A ⟶ B)) (s : Finset ι), Rep.Hom.hom (∑ i ∈ s, f i) = ∑ i ∈ s, Rep.Hom.hom (f i)
-- ProofWidgets.Component.FilterDetails
ProofWidgets.FilterDetailsProps.mk.inj : ∀ {summary filtered all : ProofWidgets.Html} {initiallyFiltered : Bool} {summary_1 filtered_1 all_1 : ProofWidgets.Html}
  {initiallyFiltered_1 : Bool},
  { summary := summary, filtered := filtered, all := all, initiallyFiltered := initiallyFiltered } =
      { summary := summary_1, filtered := filtered_1, all := all_1, initiallyFiltered := initiallyFiltered_1 } →
    summary = summary_1 ∧ filtered = filtered_1 ∧ all = all_1 ∧ initiallyFiltered = initiallyFiltered_1
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If `f` is a collection of continuous linear maps, then the construction
`ContinuousMultilinearMap.compContinuousLinearMap`
sending a continuous multilinear map `g` to `g (f₁ ·, ..., fₙ ·)` is continuous-linear in `g` and
continuous-multilinear in `f₁, ..., fₙ`.  -/
ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear : (𝕜 : Type u) →
  {ι : Type v} →
    (E : ι → Type wE) →
      (E₁ : ι → Type wE₁) →
        (G : Type wG) →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] →
                  [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        [Fintype ι] →
                          ContinuousMultilinearMap 𝕜 (fun i => E i →L[𝕜] E₁ i)
                            (ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalClosure_subset_iff : ∀ {G : Type u_1} [inst : Group G] {s : Set G} {N : Subgroup G} [N.Normal], s ⊆ ↑N ↔ Subgroup.normalClosure s ≤ N
-- Lean.Parser.Command
Lean.Parser.Command.mutual.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.preservesColimitNatIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape J G] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape J C] (X : CategoryTheory.Functor J C),
  (CategoryTheory.preservesColimitNatIso G).inv.app X = (CategoryTheory.preservesColimitIso G X).inv
-- Init.Data.String.Defs
String.ValidPos : String → Type
-- Lean.Elab.Deriving.Util
/-- Return implicit binder syntaxes for the given `argNames`. The output matches `implicitBinder*`.

For example, ``#[`foo,`bar]`` gives `` `({foo} {bar})``.  -/
Lean.Elab.Deriving.mkImplicitBinders : Array Lean.Name → Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.implicitBinder))
-- Mathlib.CategoryTheory.Galois.Examples
/-- The inclusion from the complement of the image of `f : X ⟶ Y` into `Y`.  -/
CategoryTheory.FintypeCat.imageComplementIncl : {X Y : FintypeCat} → (f : X ⟶ Y) → CategoryTheory.FintypeCat.imageComplement f ⟶ Y
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.InducedWideCategory.category_comp_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} D] (F : C → D)
  (P : CategoryTheory.MorphismProperty D) [inst_1 : P.IsMultiplicative]
  {x x_1 x_2 : CategoryTheory.InducedWideCategory D F P} (f : x.Hom x_1) (g : x_1.Hom x_2),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom