mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.mem_ballSubgroup_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M}
  {c : FiniteMulArchimedeanClass M}, a ∈ c.ballSubgroup ↔ ∀ (h : a ≠ 1), c < FiniteMulArchimedeanClass.mk a h
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from commutative groups to types preserves all limits. (That is, the
underlying types could have been computed instead as limits in the category of types.)
 -/
CommGrpCat.forget_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget CommGrpCat)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.orderMonoidIso.congr_simp : ∀ {R : Type u_2} {Γ : Type u_3} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : LinearOrderedCommGroupWithZero Γ]
  (v : Valuation R Γ) [inst_3 : v.Compatible],
  ValuativeRel.ValueGroupWithZero.orderMonoidIso v = ValuativeRel.ValueGroupWithZero.orderMonoidIso v
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- Build an isomorphism in the category `CommAlgCat R` from an `AlgEquiv` between commutative
`Algebra`s.  -/
CommAlgCat.isoMk : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      {x : CommRing X} →
        {x_1 : CommRing Y} →
          {x_2 : Algebra R X} → {x_3 : Algebra R Y} → (X ≃ₐ[R] Y) → (CommAlgCat.of R X ≅ CommAlgCat.of R Y)
-- Mathlib.RingTheory.Bialgebra.Basic
/-- A bialgebra over a commutative (semi)ring `R` is both an algebra and a coalgebra over `R`, such
that the counit and comultiplication are algebra morphisms.  -/
Bialgebra : (R : Type u) → (A : Type v) → [CommSemiring R] → [Semiring A] → Type (max u v)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.TrailingMonic.trailingCoeff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.TrailingMonic → p.trailingCoeff = 1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instLaxBraidedMonMapAddMon : {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 : CategoryTheory.SymmetricCategory C] →
                [inst_5 : CategoryTheory.SymmetricCategory D] → [inst_6 : F.LaxBraided] → F.mapAddMon.LaxBraided
-- Mathlib.CategoryTheory.Monoidal.Limits.Basic
CategoryTheory.Limits.lim_μ_π_assoc : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_3 : CategoryTheory.MonoidalCategory C]
  (F G : CategoryTheory.Functor J C) (j : J) {Z : C}
  (h : (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Limits.lim F G)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) j) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Limits.limit.π F j)
        (CategoryTheory.Limits.limit.π G j))
      h
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_div : ∀ {α : Type u_2} [inst : Div α] {t : Set α} {a : α}, {a} / t = (fun x1 x2 => x1 / x2) a '' t
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α},
  Std.ExtDHashMap.Const.get? ∅ a = none
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.hom_id : ∀ {X : AddGrpCat}, AddGrpCat.Hom.hom (CategoryTheory.CategoryStruct.id X) = AddMonoidHom.id ↑X
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
AddGroup.existsAddOfLE : ∀ (α : Type u) [inst : AddGroup α] [inst_1 : LE α], ExistsAddOfLE α
-- Lean.DocString.Types
Lean.Doc.instReprInline : {i : Type u_1} → [Repr i] → Repr (Lean.Doc.Inline i)
-- Mathlib.Tactic.Ring.Compare
/-- `PartialOrder` implies `LE`.  -/
Mathlib.Tactic.Ring.leOfPartialOrder : (α : Type u_1) → [PartialOrder α] → LE α
-- Mathlib.Data.Setoid.Basic
/-- The equivalence closure of a binary relation r is contained in any equivalence
relation containing r.  -/
Setoid.eqvGen_le : ∀ {α : Type u_1} {r : α → α → Prop} {s : Setoid α}, (∀ (x y : α), r x y → s x y) → Relation.EqvGen.setoid r ≤ s
-- Init.Data.List.Control
/-- Folds a monadic function over a list from the left, accumulating a value starting with `init`. The
accumulated value is combined with the each element of the list in order, using `f`.

Example:
```lean example
example [Monad m] (f : α → β → m α) :
    List.foldlM (m := m) f x₀ [a, b, c] = (do
      let x₁ ← f x₀ a
      let x₂ ← f x₁ b
      let x₃ ← f x₂ c
      pure x₃)
  := by rfl
```
 -/
List.foldlM : {m : Type u → Type v} → [Monad m] → {s : Type u} → {α : Type w} → (s → α → m s) → s → List α → m s
-- Init.Data.Int.Lemmas
Int.neg_ne_zero : ∀ {a : ℤ}, -a ≠ 0 ↔ a ≠ 0
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrangeRestrict_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N),
  MonoidHom.mker f.mrangeRestrict = MonoidHom.mker f
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V],
  (CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk V).multiplicativeClosure = ⊤
-- Mathlib.Order.Sublocale
Nucleus.toSublocale_le_toSublocale : ∀ {X : Type u_1} [inst : Order.Frame X] {m n : Nucleus X}, m.toSublocale ≤ n.toSublocale ↔ n ≤ m
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.multiequalizer_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type s}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J C}
  [inst_3 : CategoryTheory.Limits.HasMultiequalizer I]
  [CategoryTheory.Limits.PreservesLimit I.multicospan (CategoryTheory.forget C)]
  (x y : CategoryTheory.ToType (CategoryTheory.Limits.multiequalizer I)),
  (∀ (t : J.L),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι I t)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Multiequalizer.ι I t)) y) →
    x = y
-- Init.Data.BitVec.Lemmas
BitVec.toNat_shiftLeft : ∀ {v n : ℕ} {x : BitVec v}, (x <<< n).toNat = x.toNat <<< n % 2 ^ v
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- In an inner product space with dimension 1, a set `{v}` is an orthonormal basis for
`‖v‖ = 1`.  -/
FiniteDimensional.orthonormalBasisSingleton : (ι : Type u_1) →
  (𝕜 : Type u_3) →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : Fintype ι] → [Unique ι] → Module.finrank 𝕜 E = 1 → (v : E) → ‖v‖ = 1 → OrthonormalBasis ι 𝕜 E
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.lift_symm_apply : ∀ {α : Type u} {β : Type v} [inst : AddGroup β] (g : FreeAddGroup α →+ β) (a : α),
  FreeAddGroup.lift.symm g a = (⇑g ∘ FreeAddGroup.of) a
-- Init.System.IO
_private.Init.System.IO.0.IO.FS.Stream.lines.read : IO.FS.Stream → Array String → IO (Array String)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- The left Kan extension functor `L.Lan` is left adjoint to the precomposition by `L`.  -/
CategoryTheory.Functor.lanAdjunction : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (L : CategoryTheory.Functor C D) →
          (H : Type u_3) →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F] →
                L.lan ⊣ (CategoryTheory.Functor.whiskeringLeft C D H).obj L
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- `invertibleOfFromBlocksZero₁₂Invertible` and `Matrix.fromBlocksZero₁₂Invertible` form
an equivalence.  -/
Matrix.fromBlocksZero₁₂InvertibleEquiv : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (C : Matrix n m α) →
                    (D : Matrix n n α) → Invertible (Matrix.fromBlocks A 0 C D) ≃ Invertible A × Invertible D
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- Let `u : E →L[𝕜] F` be a continuous linear map. A **Fredholm package** for `u` is the data of
Fredholm decompositions `decDom` and `decCodom` of `E` and `F` respectively, together with
a continuous linear equivalence `equiv : decDom.X₁ ≃L[𝕜] decCodom.X₁` between the "essential"
(i.e. finite codimension) parts of these decompositions, such that `u` equals the composition
`decCodom.X₁.subtypeL ∘L equiv ∘L decDom.proj`. In other words, in these
"essential ⊕ inessential" decompositions, the matrix of `u` is
$\begin{pmatrix} \texttt{equiv} & 0 \cr 0 & 0 \end{pmatrix}$.

We will show in `isFredholm_tfae` that an operator is Fredholm if and only if it admits
a Fredholm package. In practice, the condition that `u` is Fredholm (`IsFredholm`) is always easier
to prove, so if you need a Fredholm package you should probably get it from
`IsFredholm.nonempty_fredholmPackage` or `IsFredholm.fredholmPackage`.  -/
ContinuousLinearMap.FredholmPackage : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : AddCommGroup F] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : Module 𝕜 F] →
                [inst_5 : TopologicalSpace E] → [inst_6 : TopologicalSpace F] → (E →L[𝕜] F) → Type (max u_2 u_3)
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.hyp.injEq : ∀ (ldecl ldecl_1 : Lean.LocalDecl),
  (Aesop.IndexMatchLocation.hyp ldecl = Aesop.IndexMatchLocation.hyp ldecl_1) = (ldecl = ldecl_1)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.id_toPrelaxFunctor : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B],
  (CategoryTheory.Pseudofunctor.id B).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.id B
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv_toMatrixAlgEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁),
  (Matrix.toLinAlgEquiv v₁) ((LinearMap.toMatrixAlgEquiv v₁) f) = f
-- Init.Core
PUnit.subsingleton : ∀ (a b : PUnit.{u_1}), a = b
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- `nsmul` of `AddOreLocalization`  -/
AddOreLocalization.nsmul : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] → ℕ → AddOreLocalization S R → AddOreLocalization S R
-- Mathlib.AlgebraicGeometry.Gluing
CategoryTheory.GlueData.ι.eq_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] (i : D.J),
  D.ι i = CategoryTheory.Limits.Multicoequalizer.π D.diagram i
-- Mathlib.Topology.Homotopy.Equiv
ContinuousMap.HomotopyEquiv.ext_iff : ∀ {X : Type u} {Y : Type v} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y}
  {x y : ContinuousMap.HomotopyEquiv X Y}, x = y ↔ x.toFun = y.toFun ∧ x.invFun = y.invFun
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- If a category has wide pushouts on a higher universe level it also has wide pushouts
on a lower universe level.  -/
CategoryTheory.Limits.hasWidePushouts_shrink : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasWidePushouts C],
  CategoryTheory.Limits.HasWidePushouts C
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isEquiv_iff_val_le_one : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀},
  v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.instFintype : (α : Type u_1) → [inst : Fintype α] → [inst_1 : DecidableEq α] → Fintype ↥(alternatingGroup α)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Topology.Algebra.Monoid
SeparatelyContinuousAdd.to_continuousVAdd_op : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M], ContinuousConstVAdd Mᵃᵒᵖ M
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂),
  LinearMap.toMatrix v₁ v₂ = (v₁.equivFun.arrowCongr v₂.equivFun).trans LinearMap.toMatrix'
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The `Aut F` action on the fiber of a connected object is transitive. For a version
with less restrictive universe assumptions, see `FiberFunctor.isPretransitive_of_isConnected`.  -/
_private.Mathlib.CategoryTheory.Galois.Prorepresentability.0.CategoryTheory.PreGaloisCategory.FiberFunctor.isPretransitive_of_isConnected' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C)
  [CategoryTheory.PreGaloisCategory.IsConnected X], MulAction.IsPretransitive (CategoryTheory.Aut F) (F.obj X).obj
-- Mathlib.Topology.Irreducible
IsPreirreducible.image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X},
  IsPreirreducible s → ∀ (f : X → Y), ContinuousOn f s → IsPreirreducible (f '' s)
-- Lean.Level
Lean.Level.max : Lean.Level → Lean.Level → Lean.Level
-- Batteries.Data.MLList.Basic
/-- Filter a `MLList`.  -/
MLList.filter : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → (α → Bool) → MLList m α → MLList m α
-- Init.Data.UInt.Lemmas
UInt64.toUSize_ofBitVec : ∀ (b : BitVec 64), { toBitVec := b }.toUSize = { toBitVec := BitVec.setWidth System.Platform.numBits b }
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
map_eq_zero : ∀ {G₀ : Type u_3} {M₀' : Type u_4} {F : Type u_6} [inst : GroupWithZero G₀] [inst_1 : MulZeroOneClass M₀']
  [Nontrivial M₀'] [inst_3 : FunLike F G₀ M₀'] [MonoidWithZeroHomClass F G₀ M₀'] (f : F) {a : G₀}, f a = 0 ↔ a = 0
-- Mathlib.LinearAlgebra.Pi
/-- The constant linear map, taking `x` to `Function.const ι x`.  -/
LinearMap.const : {R : Type u} →
  {M₂ : Type w} →
    {ι : Type x} → [inst : Semiring R] → [inst_1 : AddCommMonoid M₂] → [inst_2 : Module R M₂] → M₂ →ₗ[R] ι → M₂
-- Mathlib.Data.Nat.Prime.Defs
Nat.irreducible_iff_nat_prime : ∀ (a : ℕ), Irreducible a ↔ Nat.Prime a
-- Mathlib.CategoryTheory.Action.Limits
Action.instPreservesColimitsOfShapeForgetOfHasColimitsOfShape : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J] [CategoryTheory.Limits.HasColimitsOfShape J V],
  CategoryTheory.Limits.PreservesColimitsOfShape J (Action.forget V G)
-- Mathlib.Topology.LocallyConstant.Basic
/-- We can turn a locally-constant function into a bundled `ContinuousMap`.  -/
LocallyConstant.toContinuousMap : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → LocallyConstant X Y → C(X, Y)
-- Mathlib.Data.Set.Lattice
Set.sUnion_eq_empty : ∀ {α : Type u_1} {S : Set (Set α)}, ⋃₀ S = ∅ ↔ ∀ s ∈ S, s = ∅
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleSets.mk : Array Aesop.RuleSetName → Aesop.Frontend.RuleSets
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_apply_apply_zpow_self : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (x : α) (k : ℤ),
  (f.cycleOf x) ((f ^ k) x) = (f ^ (k + 1)) x
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.coeff_natTrailingDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.coeff p.natTrailingDegree = 0 ↔ p = 0
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Measurable.nullMeasurable : ∀ {α : Type u_2} {β : Type u_3} [m : MeasurableSpace α] [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α}, Measurable f → MeasureTheory.NullMeasurable f μ
-- Mathlib.Data.Matrix.Basic
RingHom.mapMatrix_id : ∀ {m : Type u_2} {α : Type u_11} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NonAssocSemiring α],
  (RingHom.id α).mapMatrix = RingHom.id (Matrix m m α)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.coe_units_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} {n : ℤ}
  (z : CochainComplex.HomComplex.Cocycle F G n) (x : Rˣ), ↑(x • z) = x • ↑z
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_set_sInter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (a : α) (S : Set (Set β)), a +ᵥ ⋂₀ S ⊆ ⋂ s ∈ S, a +ᵥ s
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.isAddHaarMeasure_inducedMeasure : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C}
  (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A] [inst_7 : IsTopologicalAddGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure]
  [inst_10 : IsTopologicalAddGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B], (H.inducedMeasure μA μC).IsAddHaarMeasure
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isBigO_atTop_of_degree_le : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜], P.degree ≤ Q.degree → (fun x => Polynomial.eval x P) =O[Filter.atTop] fun x => Polynomial.eval x Q
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.liftOn_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Sort u} (f : M → ↥S → p)
  (H : ∀ {a c : M} {b d : ↥S}, (Localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S),
  ((Localization.monoidOf S).mk' a b).liftOn f H = f a b
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
/-- Given `T : MorphismProperty C`, this is the class of morphisms that have the
right lifting property (rlp) with respect to `T`.  -/
CategoryTheory.MorphismProperty.rlp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] [inst_1 : Inhabited α] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap! f t).getKey! k =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Internal.Impl.Const.get t x ⋯)).isSome).get!
-- Mathlib.SetTheory.Cardinal.Basic
/-- A variant of `ciSup_of_empty` but with `0` on the RHS for convenience  -/
Cardinal.iSup_of_empty : ∀ {ι : Sort u_1} (f : ι → Cardinal.{u_2}) [IsEmpty ι], iSup f = 0
-- Mathlib.Data.List.Induction
/-- A recursion principle for lists which separates the singleton case.
 -/
List.twoStepInduction : {α : Type u_1} →
  {motive : List α → Sort u_2} →
    motive [] →
      ((x : α) → motive [x]) →
        ((x y : α) → (xs : List α) → motive xs → ((y : α) → motive (y :: xs)) → motive (x :: y :: xs)) →
          (l : List α) → motive l
-- Aesop.Index.Basic
Aesop.IndexingMode.hypsMatchingConst : Lean.Name → Lean.MetaM Aesop.IndexingMode
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
NNReal.HolderTriple.inv_ne_zero' : ∀ {p q r : NNReal}, p.HolderTriple q r → r⁻¹ ≠ 0
-- Mathlib.Order.RelClasses
Subsingleton.isWellOrder : ∀ {α : Type u} [Subsingleton α] (r : α → α → Prop) [Std.Irrefl r], IsWellOrder α r
-- Init.Grind.Norm
Lean.Grind.natCast_mod : ∀ (a b : ℕ), ↑(a % b) = ↑a % ↑b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ofList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {k : α} {v : β} {tl : List (α × β)},
  Std.ExtDTreeMap.Const.ofList ((k, v) :: tl) cmp = Std.ExtDTreeMap.Const.insertMany (∅.insert k v) tl
-- Init.Data.Int.DivMod.Lemmas
Int.add_bmod_left : ∀ (a : ℕ) (b : ℤ), (↑a + b).bmod a = b.bmod a
-- Mathlib.CategoryTheory.Limits.Preorder
/-- If `C` is a preorder with top, then `⊤` is a terminal object.  -/
Preorder.isTerminalTop : (C : Type u) → [inst : Preorder C] → [inst_1 : OrderTop C] → CategoryTheory.Limits.IsTerminal ⊤
-- Init.Core
/-- Rewriting inside `φ` using `Eq.recOn` yields a term that's heterogeneously equal to the original
term.
 -/
eqRec_heq : ∀ {α : Sort u} {φ : α → Sort v} {a a' : α} (h : a = a') (p : φ a), Eq.recOn h p ≍ p
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.equivExterior.eq_1 : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) [inst_3 : Invertible 2], CliffordAlgebra.equivExterior Q = CliffordAlgebra.changeFormEquiv ⋯
-- Mathlib.Algebra.Order.Group.Lattice
mul_inf : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] (a b c : α), c * (a ⊓ b) = c * a ⊓ c * b
-- Mathlib.Order.InitialSeg
/-- Given a well order `s`, there is a most one principal segment embedding of `r` into `s`.  -/
PrincipalSeg.instSubsingletonOfIsWellOrder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s], Subsingleton (PrincipalSeg r s)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The negation of a nonsingular projective point on a Weierstrass curve `W`.

Given a nonsingular projective point `P` on `W`, use `-P` instead of `neg P`.  -/
WeierstrassCurve.Projective.Point.neg : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Projective F} → W.Point → W.Point
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The function `Real.cos` is real analytic.  -/
Real.analyticOnNhd_cos : ∀ {s : Set ℝ}, AnalyticOnNhd ℝ Real.cos s
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableAt.continuousMultilinear_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_5} {M : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H]
  {c : E → ContinuousMultilinearMap 𝕜 M H} [Finite ι],
  DifferentiableAt 𝕜 c x → ∀ (u : (i : ι) → M i), DifferentiableAt 𝕜 (fun y => (c y) u) x
-- Batteries.Data.Fin.Coding
Fin.encodeSigma.eq_1 : ∀ (a : ℕ) (f_2 : Fin (a + 1) → ℕ) (j : Fin (f_2 0)), Fin.encodeSigma f_2 ⟨⟨0, ⋯⟩, j⟩ = ⟨↑j, ⋯⟩