mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_some_getD : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {a : α} {fallback : β},
      a ∈ t → Std.DTreeMap.Internal.Impl.Const.get? t a = some (Std.DTreeMap.Internal.Impl.Const.getD t a fallback)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_eq_of_degreeOf_add_lt : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {i : σ},
  MvPolynomial.degreeOf i (p + q) < MvPolynomial.degreeOf i p → MvPolynomial.degreeOf i p = MvPolynomial.degreeOf i q
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeffs_empty_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.coeffs = ∅ ↔ p = 0
-- Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Nat.factors_multiset_prod_of_irreducible : ∀ {s : Multiset ℕ}, (∀ x ∈ s, Irreducible x) → UniqueFactorizationMonoid.normalizedFactors s.prod = s
-- Lean.Hygiene
Lean.Unhygienic.Context.mk.injEq : ∀ (ref : Lean.Syntax) (scope : Lean.MacroScope) (ref_1 : Lean.Syntax) (scope_1 : Lean.MacroScope),
  ({ ref := ref, scope := scope } = { ref := ref_1, scope := scope_1 }) = (ref = ref_1 ∧ scope = scope_1)
-- Mathlib.Logic.Relation
/-- If `f : α → β` is a fibration between relations `rα` and `rβ`, and `a : α` is
accessible under `rα`, then `f a` is accessible under `rβ`.  -/
Acc.of_fibration : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} (f : α → β),
  Relation.Fibration rα rβ f → ∀ {a : α}, Acc rα a → Acc rβ (f a)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkHaveS : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Name → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Topology.Category.TopCat.Limits.Konig
TopCat.partialSections.closed : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat)
  [∀ (j : J), T2Space ↑(F.obj j)] {G : Finset J} (H : Finset (TopCat.FiniteDiagramArrow✝ G)),
  IsClosed (TopCat.partialSections F H)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- In the power series expansion of `℘(z) = ∑ aᵢzⁱ` at some `x ∉ L`,
each `aᵢ` can be written as an infinite sum over `l ∈ L`.
This is the summand of this infinite sum. See `PeriodPair.coeff_weierstrassPSeries`.  -/
PeriodPair.weierstrassPSummand : (L : PeriodPair) → ℂ → ℕ → ↥L.lattice → ℂ
-- Mathlib.Order.Filter.Map
Filter.seq_pure : ∀ {α : Type u_1} {β : Type u_2} (f : Filter (α → β)) (a : α), f.seq (pure a) = Filter.map (fun g => g a) f
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.getSimpPriority : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Aesop.Frontend.RuleConfig → m ℕ
-- Lean.Environment
Lean.PersistentEnvExtensionState.mk.sizeOf_spec : ∀ {α σ : Type} [inst : SizeOf α] [inst_1 : SizeOf σ] (importedEntries : Array (Array α)) (state : σ),
  sizeOf { importedEntries := importedEntries, state := state } = 1 + sizeOf importedEntries + sizeOf state
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofTop_symm_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) {h : p = ⊤} (x : M), (LinearEquiv.ofTop p h).symm x = ⟨x, ⋯⟩
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.toSeq? : List Lean.Grind.AC.Var → Option Lean.Grind.AC.Seq
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  {f g : α → ENNReal},
  Measurable f →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ) → f ≤ᵐ[μ] g
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.δ_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (F.obj X) (F.obj Y)) =
    F.map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- The following diagram is a pullback
```
X --f--> Z
|        |
id       id
v        v
X --f--> Z
```
 -/
CategoryTheory.IsPullback.id_vert : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Z : C} (f : X ⟶ Z),
  CategoryTheory.IsPullback f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Z) f
-- Mathlib.Order.Filter.Subsingleton
Filter.Subsingleton.of_subsingleton : ∀ {α : Type u_1} {l : Filter α} [Subsingleton α], l.Subsingleton
-- Mathlib.Algebra.Group.Prod
Prod.instDivInvMonoid : {G : Type u_1} → {H : Type u_2} → [DivInvMonoid G] → [DivInvMonoid H] → DivInvMonoid (G × H)
-- Std.Http.Data.Status
Std.Http.Status.created.sizeOf_spec : sizeOf Std.Http.Status.created = 1
-- Mathlib.Computability.Primrec.List
/-- Bounded universal quantifiers are primitive recursive.  -/
PrimrecPred.forall_lt : ∀ {p : ℕ → Prop}, PrimrecPred p → PrimrecPred fun n => ∀ x < n, p x
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ κ_1 : ProbabilityTheory.Kernel α β),
  κ = κ_1 → ∀ (g g_1 : γ → α) (e_g : g = g_1) (hg : Measurable g), κ.comap g hg = κ_1.comap g_1 ⋯
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.eq_zero_of_isEmpty : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [IsEmpty α] (μ : MeasureTheory.VectorMeasure α M), μ = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → (Std.DTreeMap.Raw.Const.insertMany t l).getKey! k' = k
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce.Step.eq : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.Red.Step L₁ L₂ → FreeAddGroup.reduce L₁ = FreeAddGroup.reduce L₂
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.coeff_zero_multiset_prod : ∀ {R : Type u} [inst : CommSemiring R] (t : Multiset (Polynomial R)),
  t.prod.coeff 0 = (Multiset.map (fun f => f.coeff 0) t).prod
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleMatch.type : LeanSearchClient.LoogleMatch → String
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edgeSet_sdiff : ∀ {V : Type u} (G₁ G₂ : SimpleGraph V), (G₁ \ G₂).edgeSet = G₁.edgeSet \ G₂.edgeSet
-- Lean.Meta.ArgsPacker
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Mutual.pack.go : ℕ → ℕ → Lean.Expr → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Fin.Lemmas
Fin.mul_ofNat : ∀ {n : ℕ} [inst : NeZero n] (x : Fin n) (y : ℕ), x * Fin.ofNat n y = Fin.ofNat n (↑x * y)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.map'_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n)
  (i j k : ℕ) (hij : autoParam (i ≤ j) CategoryTheory.ComposableArrows.map'_comp._auto_1)
  (hjk : autoParam (j ≤ k) CategoryTheory.ComposableArrows.map'_comp._auto_3)
  (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.map'_comp._auto_5),
  F.map' i k ⋯ hk = CategoryTheory.CategoryStruct.comp (F.map' i j hij ⋯) (F.map' j k hjk hk)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- Auxiliary lemma used as an argument to `CliffordAlgebra.changeForm`  -/
CliffordAlgebra.changeForm.neg_proof : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M},
  LinearMap.BilinMap.toQuadraticMap B = Q' - Q → LinearMap.BilinMap.toQuadraticMap (-B) = Q - Q'
-- Lean.Meta.Tactic.Grind.EqResolution
Lean.Meta.Grind.TopSort.State.tempMark : Lean.Meta.Grind.TopSort.State → Std.HashSet Lean.Expr
-- Mathlib.Algebra.Polynomial.RingDivision
Polynomial.mem_nonZeroDivisors_of_leadingCoeff : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R},
  p.leadingCoeff ∈ nonZeroDivisors R → p ∈ nonZeroDivisors (Polynomial R)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_associator_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y Z : C) {Z_1 : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) h))))
-- Mathlib.Order.Hom.Basic
/-- The identity function as bundled monotone function.  -/
OrderHom.id : {α : Type u_2} → [inst : Preorder α] → α →o α
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.inv : {α : Type u_1} → [inst : Semifield α] → [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → Inv { x // 0 ≤ x }
-- Mathlib.Algebra.Module.Equiv.Defs
/-- The backward map of an equivalence.

Do NOT use `e.invFun` directly. Use the coercion of `e.symm` instead.  -/
LinearEquiv.invFun : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                {M : Type u_16} →
                  {M₂ : Type u_17} →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] → [inst_7 : Module S M₂] → (M ≃ₛₗ[σ] M₂) → M₂ → M
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.pred_eq_iff_isSuccPrelimit : ∀ {o : Ordinal.{u_4}}, o.pred = o ↔ Order.IsSuccPrelimit o
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKeyD_modifyKey_beq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {fallback : α},
      (Std.Internal.List.minKeyD (Std.Internal.List.Const.modifyKey k f l) fallback ==
          Std.Internal.List.minKeyD l fallback) =
        true
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.forget₂_map : ∀ {R S : AddCommGrpCat} (f : R ⟶ S) (x : ↑((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).obj R)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ AddCommGrpCat AddGrpCat).map f)) x =
    (CategoryTheory.ConcreteCategory.hom f) x
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u_1} {X Y : CategoryTheory.GradedObject β C}
  {f g : X ⟶ Y}, f = g ↔ ∀ (x : β), f x = g x
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.u_injective : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : Preorder α] [inst_1 : PartialOrder β]
  (gi : GaloisInsertion l u), Function.Injective u
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMax'.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α × α → Sort u_2) → (x : Ordnode α × α) → ((r' : Ordnode α) → (xm : α) → motive (r', xm)) → motive x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_mem_div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α} {a b : α}, a ∈ s → b ∈ t → a / b ∈ s / t
-- Mathlib.Condensed.Basic
CondensedSet.hom_naturality_apply : ∀ {X Y : CondensedSet} (f : X ⟶ Y) {S T : CompHausᵒᵖ} (g : S ⟶ T) (x : X.obj.obj S),
  (CategoryTheory.ConcreteCategory.hom (f.hom.app T)) ((CategoryTheory.ConcreteCategory.hom (X.obj.map g)) x) =
    (CategoryTheory.ConcreteCategory.hom (Y.obj.map g)) ((CategoryTheory.ConcreteCategory.hom (f.hom.app S)) x)
-- Mathlib.Condensed.Light.Epi
LightCondensed.epi_π_app_zero_of_epi : ∀ (R : Type u_1) [inst : Ring R] {F : CategoryTheory.Functor ℕᵒᵖ (LightCondMod R)} {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsLimit c),
  (∀ (n : ℕ), CategoryTheory.Epi (F.map (CategoryTheory.homOfLE ⋯).op)) → CategoryTheory.Epi (c.π.app (Opposite.op 0))
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.inf_addSubgroupOf_inf_normal_of_right : ∀ {G : Type u_1} [inst : AddGroup G] (A B' B : AddSubgroup G) [hN : (B'.addSubgroupOf B).Normal],
  ((A ⊓ B').addSubgroupOf (A ⊓ B)).Normal
-- Mathlib.Tactic.Translate.Core
/-- View the trace of the translation procedure.
Equivalent to `set_option trace.translate true`.  -/
Mathlib.Tactic.Translate.Config.trace : Mathlib.Tactic.Translate.Config → Bool
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries_mono`. -/
upperCentralSeries_mono : ∀ (G : Type u_1) [inst : Group G], Monotone (Subgroup.upperCentralSeries G)
-- Mathlib.Data.Nat.Dist
Nat.dist.triangle_inequality : ∀ (n m k : ℕ), n.dist k ≤ n.dist m + m.dist k
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lmap_lof : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i) [inst_5 : DecidableEq ι] (i : ι) (x : M i),
  (DirectSum.lmap f) ((DirectSum.lof R ι M i) x) = (DirectSum.lof R ι N i) ((f i) x)
-- Mathlib.Data.Fintype.Defs
Fintype.decidableRightInverseFintype : {α : Type u_1} →
  {β : Type u_2} → [DecidableEq α] → [Fintype α] → (f : α → β) → (g : β → α) → Decidable (Function.RightInverse f g)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.whiskerRight_comp_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {A''' : Type u₁₀} {B''' : Type u₁₁} {C''' : Type u₁₂}
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} A'''] [inst_10 : CategoryTheory.Category.{v₁₁, u₁₁} B''']
  [inst_11 : CategoryTheory.Category.{v₁₂, u₁₂} C'''] {F''' : CategoryTheory.Functor A''' B'''}
  {G''' : CategoryTheory.Functor C''' B'''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''}
  {τ : CategoryTheory.Limits.CatCospanTransform F'' G'' F''' G'''}
  {Z : CategoryTheory.Limits.CatCospanTransform F G F''' G'''} (h : ψ'.comp (φ.comp τ) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η (φ.comp τ)) h =
    CategoryTheory.CategoryStruct.comp (ψ.associator φ τ).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight
          (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ) τ)
        (CategoryTheory.CategoryStruct.comp (ψ'.associator φ τ).hom h))
-- Mathlib.Topology.Algebra.Group.Pointwise
IsCompact.add_closure_zero_eq_closure : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {K : Set G},
  IsCompact K → K + closure {0} = closure K
-- Init.Data.AC
Lean.Data.AC.Expr.var : ℕ → Lean.Data.AC.Expr
-- Std.Http.Data.URI.Basic
Std.Http.URI.Host.name.sizeOf_spec : ∀ (name : Std.Http.URI.DomainName), sizeOf (Std.Http.URI.Host.name name) = 1 + sizeOf name
-- Aesop.Tracing
Aesop.ruleSuccessEmoji : String
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instAdd : {α : Type u_1} → Add (MeasureTheory.OuterMeasure α)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.module : {R : Type u_1} →
  {R₃ : Type u_3} →
    {S₃ : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : Semiring R₃] →
          [inst_2 : Semiring S₃] →
            {M : Type u_6} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : Module R M] →
                    {M₃ : Type u_8} →
                      [inst_6 : TopologicalSpace M₃] →
                        [inst_7 : AddCommMonoid M₃] →
                          [inst_8 : Module R₃ M₃] →
                            [inst_9 : Module S₃ M₃] →
                              [SMulCommClass R₃ S₃ M₃] →
                                [ContinuousConstSMul S₃ M₃] →
                                  {σ₁₃ : R →+* R₃} → [inst_12 : ContinuousAdd M₃] → Module S₃ (M →SL[σ₁₃] M₃)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.one_le_mul`.  -/
Right.one_le_mul : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b : α}, 1 ≤ a → 1 ≤ b → 1 ≤ a * b
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
ContMDiff.coordChangeL : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {M : Type u_5} {E : B → Type u_6}
  [inst : NontriviallyNormedField 𝕜] {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB]
  {HB : Type u_8} [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] {EM : Type u_9} [inst_6 : NormedAddCommGroup EM] [inst_7 : NormedSpace 𝕜 EM]
  {HM : Type u_10} [inst_8 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace HM M] [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)]
  [inst_13 : NormedAddCommGroup F] [inst_14 : NormedSpace 𝕜 F] [inst_15 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_16 : (x : B) → TopologicalSpace (E x)] [inst_17 : FiberBundle F E] [inst_18 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] {e e' : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_20 : MemTrivializationAtlas e] [inst_21 : MemTrivializationAtlas e'] {f : M → B},
  ContMDiff IM IB n f →
    (∀ (x : M), f x ∈ e.baseSet) →
      (∀ (x : M), f x ∈ e'.baseSet) →
        ContMDiff IM (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n fun y => ↑(Bundle.Trivialization.coordChangeL 𝕜 e e' (f y))
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- The measurability assumption is necessary, otherwise there are counterexamples: for instance,
the conclusion fails if `f` is the characteristic function of a Vitali set.  -/
MeasureTheory.lintegral_eq_zero_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → (∫⁻ (a : α), f a ∂μ = 0 ↔ f =ᵐ[μ] 0)
-- Mathlib.Order.Filter.Pointwise
Filter.instOne.eq_1 : ∀ {α : Type u_2} [inst : One α], Filter.instOne = { one := pure 1 }
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
/-- **Alias** of `SimpleGraph.cycleGraph.length_cycle`. -/
SimpleGraph.cycleGraph_EulerianCircuit_length : ∀ {n : ℕ}, (SimpleGraph.cycleGraph.cycle n).length = n + 3
-- Mathlib.Order.Heyting.Hom
BiheytingHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β]
  [inst_2 : BiheytingAlgebra γ] {f : BiheytingHom α β} {g₁ g₂ : BiheytingHom β γ},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.norm_ofSubsingleton_id : ∀ (𝕜 : Type u) (F : Type wF) {ι : Type v} [inst : Fintype ι] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] [inst_4 : Subsingleton ι] [Nontrivial F] (i : ι),
  ‖(ContinuousAlternatingMap.ofSubsingleton 𝕜 F F i) (ContinuousLinearMap.id 𝕜 F)‖ = 1
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsIInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C)
  [∀ (a : α), (P a).IsClosedUnderIsomorphisms], (⨅ a, P a).IsClosedUnderIsomorphisms
-- Mathlib.Order.WithBot
/-- **Alias** of the reverse direction of `WithTop.strictMono_map_iff`. -/
StrictMono.withTop_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → StrictMono (WithTop.map f)