mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Scalar multiplication by a non-zero element of a group with zero acting on `α` is a
homeomorphism from `α` onto itself.  -/
Homeomorph.smulOfNeZero : {α : Type u_2} →
  {G₀ : Type u_4} →
    [inst : TopologicalSpace α] →
      [inst_1 : GroupWithZero G₀] → [inst_2 : MulAction G₀ α] → [ContinuousConstSMul G₀ α] → (c : G₀) → c ≠ 0 → α ≃ₜ α
-- Mathlib.Analysis.Normed.Field.WithAbs
AbsoluteValue.Completion.instCoe : {K : Type u_1} → [inst : Field K] → (v : AbsoluteValue K ℝ) → Coe K v.Completion
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_functions_apply₂ : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {f : L.Functions 2} {t₁ t₂ : L.Term α}
  {v : α → M},
  FirstOrder.Language.Term.realize v (f.apply₂ t₁ t₂) =
    FirstOrder.Language.Structure.funMap f
      ![FirstOrder.Language.Term.realize v t₁, FirstOrder.Language.Term.realize v t₂]
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_pow : ∀ {o : Type u_4} {m' : o → Type u_7} {α : Type u_12} [inst : DecidableEq o] [inst_1 : (i : o) → DecidableEq (m' i)]
  [inst_2 : Fintype o] [inst_3 : (i : o) → Fintype (m' i)] [inst_4 : Semiring α] (M : (i : o) → Matrix (m' i) (m' i) α)
  (n : ℕ), Matrix.blockDiagonal' (M ^ n) = Matrix.blockDiagonal' M ^ n
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivInverse_obj_unitIso_hom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : (D ≌ C)ᵒᵖ),
  ((CategoryTheory.Equivalence.symmEquivInverse C D).obj X).unitIso.hom = (Opposite.unop X).counitIso.inv
-- Mathlib.Algebra.Lie.Derivation.Killing
LieDerivation.IsKilling.instIsKilling_range_ad : ∀ (R : Type u_1) (L : Type u_2) [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Module.Finite R L]
  [LieAlgebra.IsKilling R L], LieAlgebra.IsKilling R ↥(LieDerivation.ad R L).range
-- Mathlib.Algebra.Order.Hom.Monoid
antitone_iff_map_nonneg : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [i : FunLike F α β] (f : F)
  [iamhc : AddMonoidHomClass F α β], Antitone ⇑f ↔ ∀ a ≤ 0, 0 ≤ f a
-- Lean.Parser.Types
Lean.Parser.instHashableParserCacheKey : Hashable Lean.Parser.ParserCacheKey
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- The equivalence `(A ⟶ F.functorHom G) ≃ HomObj F G A`.  -/
CategoryTheory.Functor.functorHomEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        (F G : CategoryTheory.Functor C D) →
          (A : CategoryTheory.Functor C (Type (max u v v'))) → (A ⟶ F.functorHom G) ≃ F.HomObj G A
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.hom_ext_iff' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (f g : X ⟶ Y),
  f = g ↔
    ∀ (i : X.I), ∃ (h₁ : f.f i = g.f i), CategoryTheory.CategoryStruct.comp (f.φ i) (CategoryTheory.eqToHom ⋯) = g.φ i
-- Init.GrindInstances.ToInt
Lean.Grind.instLEUInt8UintOfNatNat : Lean.Grind.ToInt.LE UInt8 (Lean.Grind.IntInterval.uint 8)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.mul_def : ∀ {α : Type u} [inst : Mul α] (x y : FreeAbelianGroup α),
  x * y = (FreeAbelianGroup.lift fun x₂ => (FreeAbelianGroup.lift fun x₁ => FreeAbelianGroup.of (x₁ * x₂)) x) y
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F},
  Function.HasTemperateGrowth f →
    ∀ (n : ℕ), ∃ k C, 0 ≤ C ∧ ∀ N ≤ n, ∀ (x : E), ‖iteratedFDeriv ℝ N f x‖ ≤ C * (1 + ‖x‖) ^ k
-- Mathlib.Dynamics.Flow
Flow.instCoeFunForallForall : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] → [inst_2 : AddZero τ] → CoeFun (Flow τ α) fun x => τ → α → α
-- Mathlib.Topology.Convenient.GeneratedBy
/-- The obvious bijection `WithGeneratedByTopology X Y ≃ Y`, where
the source is endowed with the `X`-generated topology. See `continuous_equiv`
for the continuity of `equiv`. The inverse map `equiv.symm` is continuous
iff `Y` is `X`-generated, see `isGeneratedBy_iff`.  -/
Topology.WithGeneratedByTopology.equiv : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} → [tY : TopologicalSpace Y] → Topology.WithGeneratedByTopology X Y ≃ Y
-- Lean.Elab.Match
Lean.Elab.Term.isPatternVar : Lean.Syntax → Lean.Elab.TermElabM Bool
-- Init.Data.List.Lemmas
List.mem_flatten : ∀ {α : Type u_1} {a : α} {L : List (List α)}, a ∈ L.flatten ↔ ∃ l ∈ L, a ∈ l
-- Mathlib.Data.Int.Log
Int.log_of_left_le_one : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, b ≤ 1 → ∀ (r : R), Int.log b r = 0
-- Mathlib.Algebra.Group.Equiv.TypeTags
addMonoidEndToMultiplicative_apply_apply : ∀ (A : Type u_4) [inst : AddZeroClass A] (f : A →+ A) (a : Multiplicative A),
  ((addMonoidEndToMultiplicative A) f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_neg_iff_of_nonpos : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : PartialOrder N] {f : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ x ∈ s, f x ≤ 0) → (∑ x ∈ s, f x < 0 ↔ ∃ x ∈ s, f x < 0)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.insertManyIfNewUnit_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp},
  Std.DTreeMap.Const.insertManyIfNewUnit t [] = t
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr_supports : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  [inst_1 : Inhabited Λ] {S : Finset Λ},
  Turing.TM2.Supports M S → Turing.TM1.Supports (Turing.TM2to1.tr M) (Turing.TM2to1.trSupp M S)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {v : β k}, (t.insert k v).get? k = some v
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
_private.Mathlib.Combinatorics.SetFamily.AhlswedeZhang.0.Finset.inf_aux : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s : Finset α} {a : α} [inst_1 : DecidableLE α],
  a ∈ upperClosure ↑s → {b ∈ s | b ≤ a}.Nonempty
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeEndWhile_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice}, s.copy = t.copy → (s.takeEndWhile pat).copy = (t.takeEndWhile pat).copy
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_map_right_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.toArrowArrowFunctor'.map φ).right.left = φ.τ₃
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- a family of modules over `R.obj X` for all `X`  -/
PresheafOfModules.obj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → PresheafOfModules R → (X : Cᵒᵖ) → ModuleCat ↑(R.obj X)
-- Mathlib.Data.Nat.Log
Nat.pow_le_of_le_log : ∀ {b x y : ℕ}, y ≠ 0 → x ≤ Nat.log b y → b ^ x ≤ y
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
/-- The lift of a group hom to the separation quotient as a group hom.  -/
SeparationQuotient.liftNormedAddGroupHom : {M : Type u_1} →
  {N : Type u_2} →
    [inst : SeminormedAddCommGroup M] →
      [inst_1 : SeminormedAddCommGroup N] →
        (f : NormedAddGroupHom M N) → (∀ (x : M), ‖x‖ = 0 → f x = 0) → NormedAddGroupHom (SeparationQuotient M) N
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.mapNeighborSet_apply_coe : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') (v : V) (w : ↑(G.neighborSet v)),
  ↑((f.mapNeighborSet v) w) = f ↑w
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.ConstPromiseVal.exts : Lean.Environment.ConstPromiseVal✝ → Array Lean.EnvExtensionState
-- Init.Data.SInt.Lemmas
ISize.le_minValue_iff : ∀ {a : ISize}, a ≤ ISize.minValue ↔ a = ISize.minValue
-- Lean.Meta.LetToHave
/-- Heuristic for skipping subexpressions. If true, we definitely can skip.

The default max depth of `5` was not experimentally optimized, except to see that it was faster than `0`.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.canSkip : Lean.Expr → optParam UInt32 5 → Bool
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.volume_def : MeasureTheory.volume =
  (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume).withDensity fun z =>
    ↑((1 / NNReal.mk z.im ⋯) ^ 2)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.not_rev : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {x : α} {b : Bool},
  FreeGroup.Red.Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)
-- Mathlib.Topology.Order.Monotone
/-- A monotone function `f` sending `bot` to `bot` and continuous at the supremum of a set sends
this supremum to the supremum of the image of this set.  -/
Monotone.map_sSup_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : CompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β] {f : α → β} {s : Set α},
  ContinuousAt f (sSup s) → Monotone f → f ⊥ = ⊥ → f (sSup s) = sSup (f '' s)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.image_trans_source : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  ↑e '' (e.trans e').source = e.target ∩ e'.source
-- Mathlib.Order.RelIso.Basic
/-- `fun a ↦ Prod.mk a b` as a relation embedding.  -/
RelEmbedding.prodLexMkRight : {α : Type u_1} → {β : Type u_2} → {s : β → β → Prop} → (r : α → α → Prop) → {b : β} → ¬s b b → r ↪r Prod.Lex r s
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
/-- A category is locally finitely presentable if it is locally `ℵ₀`-presentable.  -/
CategoryTheory.IsLocallyFinitelyPresentable : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.comap_inf : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s t : Subring S) (f : R →+* S),
  Subring.comap f (s ⊓ t) = Subring.comap f s ⊓ Subring.comap f t
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.fold.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((c : RBTree.RBColor) →
            (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)) →
          motive x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
min_add_min_le_min_add_add : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] [AddLeftMono α] [AddRightMono α] {a b c d : α},
  min a c + min b d ≤ min (a + b) (c + d)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.keys_insertIfNew!_perm : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : BEq α] [Std.TransOrd α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).keys.Perm
        (if Std.DTreeMap.Internal.Impl.contains k t = true then t.keys else k :: t.keys)
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.prod_map_comap_prod' : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Type u_5} {N' : Type u_6}
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* N) (g : M' →* N') (S : Submonoid N) (S' : Submonoid N'),
  Submonoid.comap (f.prodMap g) (S.prod S') = (Submonoid.comap f S).prod (Submonoid.comap g S')
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.Equalizer.ι_comp_lift : ∀ {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : SeminormedAddCommGroup V₁] {f g : NormedAddGroupHom V W} (φ : NormedAddGroupHom V₁ V)
  (h : f.comp φ = g.comp φ), (NormedAddGroupHom.Equalizer.ι f g).comp (NormedAddGroupHom.Equalizer.lift φ h) = φ
-- Mathlib.RingTheory.Nilpotent.Defs
isReduced_of_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : MonoidWithZero R] [inst_1 : MonoidWithZero S] {F : Type u_3}
  [inst_2 : FunLike F R S] [MonoidWithZeroHomClass F R S] (f : F), Function.Injective ⇑f → ∀ [IsReduced S], IsReduced R
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] (μ μ_1 : MeasureTheory.Measure E),
  μ = μ_1 → ProbabilityTheory.covarianceBilin μ = ProbabilityTheory.covarianceBilin μ_1
-- Lean.Parser.Term
Lean.Parser.Term.str : Lean.Parser.Parser
-- Lean.Parser.Term
Lean.Parser.Term.matchAlts.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Do.SPred.SPred
/-- Biimplication in `SPred`: states that either satisfy both `P` and `Q` or satisfy neither satisfy
`spred(P ↔ Q)`.
 -/
Std.Do.SPred.iff : {σs : List (Type u)} → Std.Do.SPred σs → Std.Do.SPred σs → Std.Do.SPred σs
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- `RestrictedProduct.evalAddMonoidHom j` is the monoid homomorphism from the
restricted product `Πʳ i, [R i, B i]_[𝓕]` to the component `R j`.  -/
RestrictedProduct.evalAddMonoidHom : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            (j : ι) →
              [inst_1 : (i : ι) → AddMonoid (R i)] →
                [inst_2 : ∀ (i : ι), AddSubmonoidClass (S i) (R i)] →
                  RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕 →+ R j
-- Mathlib.Algebra.Ring.Defs
CommSemiring.toNonUnitalCommSemiring : {α : Type u} → [CommSemiring α] → NonUnitalCommSemiring α
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If for any finitely generated submodules `N'` of `N`, `M` and `N'` are linearly disjoint,
then `M` and `N` themselves are linearly disjoint.  -/
Submodule.LinearDisjoint.of_linearDisjoint_fg_right : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  (∀ N' ≤ N, N'.FG → M.LinearDisjoint N') → M.LinearDisjoint N
-- Mathlib.Algebra.Group.Opposite
MulOpposite.unop_div : ∀ {α : Type u_1} [inst : DivInvMonoid α] (x y : αᵐᵒᵖ),
  MulOpposite.unop (x / y) = (MulOpposite.unop y)⁻¹ * MulOpposite.unop x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
IsUnramifiedAtInfinitePlaces.top : ∀ (k : Type u_1) [inst : Field k] (K : Type u_2) [inst_1 : Field K] (F : Type u_3) [inst_2 : Field F]
  [inst_3 : Algebra k K] [inst_4 : Algebra k F] [inst_5 : Algebra K F] [IsScalarTower k K F]
  [h : IsUnramifiedAtInfinitePlaces k F], IsUnramifiedAtInfinitePlaces K F
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₂₃_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₂₃ h₂₃.p₁ = h.p₂
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- A vector field on a vector space is `C^n` in the manifold sense iff it is `C^n` in the vector
space sense.  -/
contMDiff_vectorSpace_iff_contDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x},
  (ContMDiff (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent n fun x => ⟨x, V x⟩) ↔ ContDiff 𝕜 n V
-- Mathlib.Combinatorics.SimpleGraph.Matching
/-- A graph `G` consists of a set of cycles, if each vertex is either isolated or connected to
exactly two vertices. This is used to create new matchings by taking the `symmDiff` with cycles.
The definition of `symmDiff` that makes sense is the one for `SimpleGraph`. The `symmDiff`
for `SimpleGraph.Subgraph` deriving from the lattice structure also affects the vertices included,
which we do not want in this case. This is why this property is defined for `SimpleGraph`, rather
than `SimpleGraph.Subgraph`.
 -/
SimpleGraph.IsCycles : {V : Type u_1} → SimpleGraph V → Prop
-- Lean.Server.InfoUtils
Lean.Elab.Info.docString? : Lean.Elab.Info → Lean.MetaM (Option String)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_same : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {i : ι} {f : Π₀ (i : ι), β i},
  (DFinsupp.erase i f) i = 0
-- Mathlib.Geometry.Euclidean.Projection
/-- The intersection of the subspace and the orthogonal subspace
through the given point is the `orthogonalProjection` of that point
onto the subspace.  -/
EuclideanGeometry.inter_eq_singleton_orthogonalProjection : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  ↑s ∩ ↑(AffineSubspace.mk' p s.directionᗮ) = {↑((EuclideanGeometry.orthogonalProjection s) p)}
-- Std.Time.Time.HourMarker
Std.Time.HourMarker.noConfusionType : Sort v✝ → Std.Time.HourMarker → Std.Time.HourMarker → Sort v✝
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The set `integerSet K` is stable under the action of the torsion.  -/
NumberField.mixedEmbedding.fundamentalCone.torsion_unitSMul_mem_integerSet : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K}
  {ζ : (NumberField.RingOfIntegers K)ˣ},
  ζ ∈ NumberField.Units.torsion K →
    x ∈ NumberField.mixedEmbedding.fundamentalCone.integerSet K →
      ζ • x ∈ NumberField.mixedEmbedding.fundamentalCone.integerSet K
-- Lean.Meta.WrapInstance
_private.Lean.Meta.WrapInstance.0.Lean.Meta.wrapInstance.go : Bool → Bool → Bool → Lean.Expr → Lean.Expr → Bool → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Combinatorics.Hindman
Ultrafilter.continuous_mul_left : ∀ {M : Type u_1} [inst : Mul M] (V : Ultrafilter M), Continuous fun x => x * V
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.coindResAdjunction_homEquiv_apply : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u v, u, v} k ↥S)
  {B : Rep.{max (max u v) w, u, v} k G} (f : Rep.coind.{u, v, v, max (max u v) w} S.subtype A ⟶ B),
  ((Rep.coindResAdjunction k S).homEquiv A B) f =
    (Rep.indResHomEquiv S.subtype A B) (CategoryTheory.CategoryStruct.comp A.indCoindIso.hom f)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Vector measures over a partially ordered monoid is partially ordered.

This definition is consistent with `Measure.instPartialOrder`.  -/
MeasureTheory.VectorMeasure.instPartialOrder : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : TopologicalSpace M] →
        [inst_1 : AddCommMonoid M] → [PartialOrder M] → PartialOrder (MeasureTheory.VectorMeasure α M)
-- Mathlib.Algebra.Order.Group.Finset
Finset.sup_add_sup : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : LinearOrder M]
  [CanonicallyOrderedAdd M] [inst_3 : Sub M] [AddLeftReflectLE M] [OrderedSub M] {s : Finset ι} {t : Finset κ}
  [inst_6 : OrderBot M],
  s.Nonempty → t.Nonempty → ∀ (f : ι → M) (g : κ → M), s.sup f + t.sup g = (s ×ˢ t).sup fun ij => f ij.1 + g ij.2
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_bot : ∀ {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), CategoryTheory.Sieve.functorPullback F ⊥ = ⊥
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.mconv_add : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M] (μ ν ρ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite ρ], μ.mconv (ν + ρ) = μ.mconv ν + μ.mconv ρ
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
writtenInExtChartAt_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] {I : ModelWithCorners 𝕜 E H}
  [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] [inst_7 : TopologicalSpace H']
  [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} [inst_9 : ChartedSpace H M]
  [inst_10 : ChartedSpace H' M'] {G : Type u_8} {G' : Type u_9} {F : Type u_10} {F' : Type u_11} {N : Type u_12}
  {N' : Type u_13} [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] [inst_13 : NormedAddCommGroup F']
  [inst_14 : NormedSpace 𝕜 F'] [inst_15 : TopologicalSpace G] [inst_16 : TopologicalSpace N]
  [inst_17 : TopologicalSpace G'] [inst_18 : TopologicalSpace N'] {J : ModelWithCorners 𝕜 F G}
  {J' : ModelWithCorners 𝕜 F' G'} [inst_19 : ChartedSpace G N] [inst_20 : ChartedSpace G' N'] {f : M → N} {g : M' → N'}
  {x : M} {x' : M'},
  writtenInExtChartAt (I.prod I') (J.prod J') (x, x') (Prod.map f g) =
    Prod.map (writtenInExtChartAt I J x f) (writtenInExtChartAt I' J' x' g)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_natCast_mul : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} {f : Polynomial R},
  Polynomial.derivative (↑n * f) = ↑n * Polynomial.derivative f
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_neg : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] {f : MeasureTheory.SimpleFunc α E},
  MeasureTheory.Integrable (⇑f) μ → MeasureTheory.SimpleFunc.integral μ (-f) = -MeasureTheory.SimpleFunc.integral μ f
-- Mathlib.Analysis.Complex.Norm
Complex.isAbsoluteValueNorm : IsAbsoluteValue fun x => ‖x‖
-- Mathlib.Topology.Category.Profinite.Basic
instFullFintypeCatProfiniteToProfinite : FintypeCat.toProfinite.Full
-- Mathlib.RingTheory.LocalRing.Module
Module.IsLocalRing.linearIndependent_of_flat : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [Module.Flat R M] {ι : Type u} (v : ι → M),
  LinearIndependent (IsLocalRing.ResidueField R) (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v) →
    LinearIndependent R v
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_map_equiv : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {L : BooleanSubalgebra α}
  {f : α ≃o β} {a : β},
  a ∈
      BooleanSubalgebra.map
        (let __src := { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
        L ↔
    f.symm a ∈ L
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.getVert_cycleCons : ∀ {n : ℕ} (m : Fin (n + 3)), ∀ i ≤ ↑m, ↑((SimpleGraph.cycleGraph.cycleCons✝ n m).getVert i) = (↑m - i) % (n + 3)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_inv : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι} [inst_1 : Inv β],
  MeasureTheory.stoppedValue u⁻¹ τ = (MeasureTheory.stoppedValue u τ)⁻¹