mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
/-- A functor from a pretriangulated category to an abelian category is a homological functor
if it sends distinguished triangles to exact sequences.  -/
CategoryTheory.Functor.IsHomological : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.HasShift C ℤ] →
        [inst_2 : CategoryTheory.Category.{v_3, u_3} A] →
          CategoryTheory.Functor C A →
            [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_4 : CategoryTheory.Preadditive C] →
                [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                  [CategoryTheory.Pretriangulated C] → [CategoryTheory.Abelian A] → Prop
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.essSup_piecewise : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α}
  [inst : DecidablePred fun x => x ∈ s] {g : α → ENNReal},
  MeasurableSet s → essSup (s.piecewise f g) μ = max (essSup f (μ.restrict s)) (essSup g (μ.restrict sᶜ))
-- Mathlib.Algebra.Ring.BooleanRing
toBoolAlg_zero : ∀ {α : Type u_1} [inst : BooleanRing α], toBoolAlg 0 = ⊥
-- Mathlib.Tactic.Positivity.Finset
/-- The `positivity` extension which proves that `∑ i ∈ s, f i` is nonnegative if `f` is, and
positive if each `f i` is and `s` is nonempty.

TODO: The following example does not work
```
example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.sum f := by positivity
```
because `compareHyp` can't look for assumptions behind binders.
 -/
Mathlib.Meta.Positivity.evalFinsetSum : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.RingTheory.Localization.Module
/-- A linear map `M →ₗ[R] N` gives a map between localized modules `Mₛ →ₗ[Rₛ] Nₛ`.  -/
IsLocalizedModule.mapExtendScalars : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        {M' : Type u_3} →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M'] →
              [inst_3 : Module R M] →
                [inst_4 : Module R M'] →
                  (f : M →ₗ[R] M') →
                    [IsLocalizedModule S f] →
                      {N : Type u_4} →
                        {N' : Type u_5} →
                          [inst_6 : AddCommMonoid N] →
                            [inst_7 : AddCommMonoid N'] →
                              [inst_8 : Module R N] →
                                [inst_9 : Module R N'] →
                                  (g : N →ₗ[R] N') →
                                    [IsLocalizedModule S g] →
                                      (Rₛ : Type u_6) →
                                        [inst_11 : CommSemiring Rₛ] →
                                          [inst_12 : Algebra R Rₛ] →
                                            [inst_13 : Module Rₛ M'] →
                                              [inst_14 : Module Rₛ N'] →
                                                [IsScalarTower R Rₛ M'] →
                                                  [inst_16 : IsScalarTower R Rₛ N'] →
                                                    [IsLocalization S Rₛ] → (M →ₗ[R] N) →ₗ[R] M' →ₗ[Rₛ] N'
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget₂Grp_obj_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommGrp C),
  CategoryTheory.MonObj.one = CategoryTheory.MonObj.one
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.tot : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P), affineSpan k (Set.range ⇑b) = ⊤
-- Mathlib.Topology.Defs.Basic
/-- Notation for `IsClosed` with respect to a non-standard topology.  -/
Topology.IsClosed_of : Lean.ParserDescr
-- Mathlib.Algebra.Category.Grp.EpiMono
AddCommGrpCat.forget_commGrp_preserves_epi : (CategoryTheory.forget AddCommGrpCat).PreservesEpimorphisms
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.toIsPrecomplete : ∀ {R : Type u_1} {inst : CommRing R} {I : Ideal R} {M : Type u_4} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  [self : IsAdicComplete I M], IsPrecomplete I M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.WithCache.cache : {α : Type u} →
  {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
    Std.Tactic.BVDecide.BVExpr.WithCache α aig → Std.Tactic.BVDecide.BVExpr.Cache aig
-- Mathlib.GroupTheory.FixedPointFree
/-- If a finite group admits a fixed-point-free involution, then it is commutative.  -/
MonoidHom.FixedPointFree.commGroupOfInvolutive : {F : Type u_1} →
  {G : Type u_2} →
    [inst : Group G] →
      [inst_1 : FunLike F G G] →
        [MonoidHomClass F G G] →
          {φ : F} → [Finite G] → MonoidHom.FixedPointFree ⇑φ → Function.Involutive ⇑φ → CommGroup G
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
mem_selfAdjointMatricesSubmodule' : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {n : Type u_5} [inst_1 : Fintype n] (J A : Matrix n n R₂)
  [inst_2 : DecidableEq n], A ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.mk.inj : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} {inst : L.Structure M} {inst_1 : L.Structure N}
  {dom : L.Substructure M} {cod : L.Substructure N} {toEquiv : L.Equiv ↥dom ↥cod} {dom_1 : L.Substructure M}
  {cod_1 : L.Substructure N} {toEquiv_1 : L.Equiv ↥dom_1 ↥cod_1},
  { dom := dom, cod := cod, toEquiv := toEquiv } = { dom := dom_1, cod := cod_1, toEquiv := toEquiv_1 } →
    dom = dom_1 ∧ cod = cod_1 ∧ toEquiv ≍ toEquiv_1
-- Mathlib.Condensed.Discrete.Colimit
/-- `locallyConstantPresheaf` restricted to finite sets is isomorphic to `finYoneda F`.  -/
Condensed.locallyConstantIsoFinYoneda : (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) →
  FintypeCat.toProfinite.op.comp
      (Condensed.locallyConstantPresheaf
        (F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))) ≅
    Condensed.finYoneda F
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- If `forget C` reflects initials and `ToType X` is empty, then `X` is initial.  -/
CategoryTheory.Limits.Concrete.initial_of_empty_of_reflects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] (X : C),
  IsEmpty (CategoryTheory.ToType X) → Nonempty (CategoryTheory.Limits.IsInitial X)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_eq : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K],
  RatFunc.ofFractionRing =
    ⇑(IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (FractionRing (Polynomial K)) (RatFunc K))
-- Mathlib.Algebra.Order.Group.Lattice
AddCommGroup.toDistribLattice.eq_1 : ∀ (α : Type u_2) [inst : Lattice α] [inst_1 : AddCommGroup α] [inst_2 : AddLeftMono α],
  AddCommGroup.toDistribLattice α = { toLattice := inst, le_sup_inf := ⋯ }
-- Aesop.Tree.Data
Aesop.instInhabitedMVarClusterData.default : {Goal Rapp : Type} → Aesop.MVarClusterData Goal Rapp
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.decompEquiv_symm_apply : ∀ (R : Type u_1) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace Q]
  [inst_10 : IsTopologicalAddTorsor Q] (p : Q × (V →L[R] W)) (x : V),
  ((ContinuousAffineMap.decompEquiv R V Q).symm p) x = p.2 x +ᵥ p.1
-- Mathlib.Tactic.ClickSuggestions.FindPremises
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.mk.inj : ∀
  {rw :
    Array
      (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.RwLemma)}
  {grw :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.GrwLemma)}
  {app :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyLemma)}
  {appAt :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyAtLemma)}
  {rw_1 :
    Array
      (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.RwLemma)}
  {grw_1 :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.GrwLemma)}
  {app_1 :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyLemma)}
  {appAt_1 :
    Array
      (Lean.Meta.RefinedDiscrTree.Key ×
        Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyAtLemma)},
  { rw := rw, grw := grw, app := app, appAt := appAt } = { rw := rw_1, grw := grw_1, app := app_1, appAt := appAt_1 } →
    rw = rw_1 ∧ grw = grw_1 ∧ app = app_1 ∧ appAt = appAt_1
-- Lean.Meta.CollectFVars
Lean.LocalDecl.collectFVars : Lean.LocalDecl → StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
-- Lean.Server.References
Lean.Server.TransientWorkerILean.mk.injEq : ∀ (moduleUri : Lean.Lsp.DocumentUri) (version : ℕ) (directImports : Lean.Server.DirectImports)
  (isSetupFailure? : Option Bool) (refs : Lean.Lsp.ModuleRefs) (decls : Lean.Lsp.Decls)
  (moduleUri_1 : Lean.Lsp.DocumentUri) (version_1 : ℕ) (directImports_1 : Lean.Server.DirectImports)
  (isSetupFailure?_1 : Option Bool) (refs_1 : Lean.Lsp.ModuleRefs) (decls_1 : Lean.Lsp.Decls),
  ({ moduleUri := moduleUri, version := version, directImports := directImports, isSetupFailure? := isSetupFailure?,
        refs := refs, decls := decls } =
      { moduleUri := moduleUri_1, version := version_1, directImports := directImports_1,
        isSetupFailure? := isSetupFailure?_1, refs := refs_1, decls := decls_1 }) =
    (moduleUri = moduleUri_1 ∧
      version = version_1 ∧
        directImports = directImports_1 ∧ isSetupFailure? = isSetupFailure?_1 ∧ refs = refs_1 ∧ decls = decls_1)
-- Mathlib.CategoryTheory.Yoneda
/-- `yoneda.obj X` is represented by `X`.  -/
CategoryTheory.Functor.RepresentableBy.yoneda : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → (X : C) → (CategoryTheory.yoneda.obj X).RepresentableBy X
-- Lean.Parser.Term
Lean.Parser.Term.matchAltsWhereDecls.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Batteries.Data.Float.Basic
/-- The floating point value closest to the mathematical constant `π`.
 -/
Float32.pi : Float32
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.mk₀_comp_mk₀Inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y X] [inst_6 : W.IsCompatibleWithShift M]
  [inst_7 : W.RespectsIso] (m₀ : M) (hm₀ : m₀ = 0) (f : Y ⟶ X) (hf : W f),
  (CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ f).comp
      (CategoryTheory.Localization.SmallShiftedHom.mk₀Inv m₀ hm₀ f hf) ⋯ =
    CategoryTheory.Localization.SmallShiftedHom.mk₀ W m₀ hm₀ (CategoryTheory.CategoryStruct.id Y)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.typeClass.inj : ∀ {extraErrorMsg? extraErrorMsg?_1 : Option Lean.MessageData},
  Lean.Elab.Term.SyntheticMVarKind.typeClass extraErrorMsg? =
      Lean.Elab.Term.SyntheticMVarKind.typeClass extraErrorMsg?_1 →
    extraErrorMsg? = extraErrorMsg?_1
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.Indep.isNonloop_of_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → e ∈ I → M.IsNonloop e
-- Mathlib.Algebra.MonoidAlgebra.Lift
MonoidAlgebra.liftNCRingHom_single : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : Semiring R] (f : k →+* R)
  (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (f x) (g y)) (a : G) (b : k),
  (MonoidAlgebra.liftNCRingHom f g h_comm) (MonoidAlgebra.single a b) = f b * g a
-- Mathlib.CategoryTheory.RepresentedBy
/-- The canonical representation induced by the universal element `x : F.obj X`.  -/
CategoryTheory.Functor.IsRepresentedBy.representableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} → {x : F.obj (Opposite.op X)} → F.IsRepresentedBy x → F.RepresentableBy X
-- Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform
integrable_cexp_quadratic' : ∀ {b : ℂ},
  b.re < 0 → ∀ (c d : ℂ), MeasureTheory.Integrable (fun x => Complex.exp (b * ↑x ^ 2 + c * ↑x + d)) MeasureTheory.volume
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
/-- A regular ordinal `o` has a fundamental sequence given by all smaller ordinals.  -/
Ordinal.IsFundamentalSeq.id : ∀ {o : Ordinal.{u_1}}, o ≤ o.cof.ord → Ordinal.IsFundamentalSeq id
-- Lean.DocString.Types
Lean.Doc.Inline.emph.injEq : ∀ {i : Type u} (content content_1 : Array (Lean.Doc.Inline i)),
  (Lean.Doc.Inline.emph content = Lean.Doc.Inline.emph content_1) = (content = content_1)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
SimpleGraph.isEdgeReachable_two : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V},
  G.IsEdgeReachable 2 u v ↔ ∀ (e : Sym2 V), (G.deleteEdges {e}).Reachable u v
-- Mathlib.CategoryTheory.Functor.Basic
/-- The prefunctor between the underlying quivers.  -/
CategoryTheory.Functor.toPrefunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → C ⥤q D
-- Lean.Meta.Basic
Lean.Meta.saveState : Lean.MetaM Lean.Meta.SavedState
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_bot : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂), AffineSubspace.map f ⊥ = ⊥
-- Lean.Declaration
Lean.Constructor.mk.injEq : ∀ (name : Lean.Name) (type : Lean.Expr) (name_1 : Lean.Name) (type_1 : Lean.Expr),
  ({ name := name, type := type } = { name := name_1, type := type_1 }) = (name = name_1 ∧ type = type_1)
-- Std.Data.DTreeMap.Lemmas
_private.Std.Data.DTreeMap.Lemmas.0.Break.runK.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match none with
    | some a => h_1 a
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_1.eq_1 : ∀ {α α₂ β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m (Std.IterM m β)]
  {it₁ : Std.IterM m (Std.IterM m β)} (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m (Std.IterM m β))
  (it₂' : Std.IterM m β) (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' it₂'))
  (h_1 :
    (it₁' : Std.IterM m (Std.IterM m β)) →
      (it₂' : Std.IterM m β) →
        (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' it₂')) → motive ⟨Std.IterStep.yield it₁' it₂', h⟩)
  (h_2 :
    (it₁' : Std.IterM m (Std.IterM m β)) →
      (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₁' it₂', h⟩ with
    | ⟨Std.IterStep.yield it₁' it₂', h⟩ => h_1 it₁' it₂' h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₁' it₂' h
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_hom_fromSpec : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  CategoryTheory.CategoryStruct.comp hU.isoSpec.hom hU.fromSpec = U.ι
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.isLocal_antitone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W W' : CategoryTheory.MorphismProperty C},
  W ≤ W' → W'.isLocal ≤ W.isLocal
-- Mathlib.NumberTheory.Real.Irrational
Irrational.of_mul_ratCast : ∀ (q : ℚ) {x : ℝ}, Irrational (x * ↑q) → Irrational x
-- Mathlib.Data.Set.Card
Set.Finite.cast_ncard_eq : ∀ {α : Type u_1} {s : Set α}, s.Finite → ↑s.ncard = s.encard
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.comp_of_left_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V]
  {f : Module.Dual R V} {v w : V},
  f w = 0 → LinearMap.transvection f v ∘ₗ LinearMap.transvection f w = LinearMap.transvection f (v + w)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instIsLocallyArtinianFiberOfLocallyQuasiFinite : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f] (y : ↥Y),
  AlgebraicGeometry.IsLocallyArtinian (AlgebraicGeometry.Scheme.Hom.fiber f y)
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_eq_left : ∀ {a b : ENNReal}, a ≠ 0 → a ≠ ⊤ → (a * b = a ↔ b = 1)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixedPoints_bot : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [inst_5 : SMulCommClass G K L],
  FixedPoints.intermediateField ↥⊥ = ⊤
-- Mathlib.Logic.Equiv.Basic
Equiv.piOptionEquivProd_apply : ∀ {α : Type u_10} {β : Option α → Type u_9} (f : (a : Option α) → β a),
  Equiv.piOptionEquivProd f = (f none, fun a => f (some a))
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_eq_comp : ∀ {α : Type u_2} {β : Type u_3} {δ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {f : α → β} {g g' : β → δ},
  AEMeasurable f μ → g =ᵐ[MeasureTheory.Measure.map f μ] g' → g ∘ f =ᵐ[μ] g' ∘ f
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.vcgenDischarge.quot : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Basic
exists_enorm_lt : ∀ (E : Type u_8) [inst : TopologicalSpace E] [inst_1 : ESeminormedAddMonoid E] [hbot : (nhdsWithin 0 {0}ᶜ).NeBot]
  {c : ENNReal}, c ≠ 0 → ∃ x, x ≠ 0 ∧ ‖x‖ₑ < c
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The braiding isomorphism can be passed through a map by swapping the order.  -/
CategoryTheory.Limits.biprod.braid_natural : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g)
      (CategoryTheory.Limits.biprod.braiding Y W).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X Z).hom
      (CategoryTheory.Limits.biprod.map g f)
-- Batteries.Data.ByteArray
/-- - `ofFn f` with `f : Fin n → UInt8` returns the byte array whose `i`th element is `f i`. - -/
ByteArray.ofFn : {n : ℕ} → (Fin n → UInt8) → ByteArray
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- If `λ` divides `x + 1`, then `λ ^ 4` divides `x ^ 3 + 1`.  -/
IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_add_one_of_dvd_add_one : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) [inst_1 : NumberField K]
  [IsCyclotomicExtension {3} ℚ K] {x : NumberField.RingOfIntegers K},
  hζ.toInteger - 1 ∣ x + 1 → (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 + 1
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_bracket_of_module : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {M : Type w} [inst_3 : AddCommGroup M] [inst_4 : LieRingModule L M] (x : ↥L') (m : M), ⁅x, m⁆ = ⁅↑x, m⁆
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_subset_verts : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V), G'.neighborSet v ⊆ G'.verts
-- Mathlib.Topology.Maps.Strict.Basic
/-- A quotient map is strict. See also `isQuotientMap_iff_isStrictMap_surjective`.  -/
Topology.IsQuotientMap.isStrictMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsQuotientMap f → Topology.IsStrictMap f
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_biUnion_finset : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {ι : Type u_4} {s : Finset ι} {f : ι → Set α},
  (↑s).PairwiseDisjoint f → (∀ b ∈ s, MeasurableSet (f b)) → v (⋃ b ∈ s, f b) = ∑ p ∈ s, v (f p)
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.ofFinEmb.eq_1 : ∀ (n : ℕ) (β : Type u_2) (f : Fin n ↪ β), Set.powersetCard.ofFinEmb n β f = Set.powersetCard.map n f ⟨Finset.univ, ⋯⟩
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.coe_skeletonLT`. -/
Topology.CWComplex.coe_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (n : ℕ∞),
  ↑(Topology.RelCWComplex.skeletonLT C n) = D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.closedCell m j
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.indFVars : Lean.Elab.Command.AddAndFinalizeContext✝ → Array Lean.Expr
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instAddCommGroupHom : (R : Type u) → [inst : Ring R] → [inst_1 : TopologicalSpace R] → {X Y : TopModuleCat R} → AddCommGroup (X ⟶ Y)
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_le_iff_le_mul : ∀ {a b c : ENNReal}, b ≠ 0 ∨ c ≠ ⊤ → b ≠ ⊤ ∨ c ≠ 0 → (a / b ≤ c ↔ a ≤ c * b)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_le_minKey?_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k km kme : α} (hkme : (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey? = some kme),
  t.minKey?.get ⋯ = km → (compare km kme).isLE = true
-- Mathlib.Order.Filter.Pointwise
Filter.covariant_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β],
  CovariantClass (Filter α) (Filter β) (fun x1 x2 => x1 +ᵥ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Order.Grade
grade_strictMono : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeOrder 𝕆 α],
  StrictMono (grade 𝕆)
-- Init.Data.Vector.Erase
Vector.eraseIdx_set_lt : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {w : i < n} {j : ℕ} {a : α} (h : j < i),
  (xs.set i a w).eraseIdx j ⋯ = (xs.eraseIdx j ⋯).set (i - 1) a ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂)[k]? = none
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.functor_map_app : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {X Y : Action V G}
  (f : X ⟶ Y) (x : CategoryTheory.SingleObj G), (Action.FunctorCategoryEquivalence.functor.map f).app x = f.hom
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.instPartialOrder : {K : Type u} → [inst : DivisionRing K] → PartialOrder (Subfield K)
-- Mathlib.ModelTheory.Fraisse
/-- The age of a structure `M` is the class of finitely-generated structures that embed into it.  -/
FirstOrder.Language.age : (L : FirstOrder.Language) → (M : Type w) → [L.Structure M] → Set (CategoryTheory.Bundled L.Structure)