mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- Given `h : ConnectData K L` and `n : ℕ` non-zero, the homology
of `h.cochainComplex` in degree `-(n + 1)` identifies to the homology of `K` in degree `n`.  -/
CochainComplex.ConnectData.homologyIsoNeg : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : ChainComplex C ℕ} →
        {L : CochainComplex C ℕ} →
          (h : CochainComplex.ConnectData K L) →
            (n : ℕ) →
              [NeZero n] →
                (m : ℤ) →
                  m = -↑(n + 1) →
                    [inst_3 : HomologicalComplex.HasHomology h.cochainComplex m] →
                      [inst_4 : HomologicalComplex.HasHomology K n] →
                        HomologicalComplex.homology h.cochainComplex m ≅ HomologicalComplex.homology K n
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
/-- Least fixed point of functor F. The result is a functor with one fewer parameters
than the input. For `F a b c` a ternary functor, `Fix F` is a binary functor such that

```lean
Fix F a b = F a b (Fix F a b)
```
 -/
MvQPF.Fix : {n : ℕ} → (F : TypeVec.{u_1} (n + 1) → Type u_1) → [q : MvQPF F] → TypeVec.{u_1} n → Type u_1
-- Mathlib.Algebra.Group.Action.Defs
/-- A typeclass indicating that the right (aka `AddOpposite`) and left actions by `M` on `α` are
equal, that is that `M` acts centrally on `α`. This can be thought of as a version of commutativity
for `+ᵥ`.  -/
IsCentralVAdd : (M : Type u_9) → (α : Type u_10) → [VAdd M α] → [VAdd Mᵃᵒᵖ α] → Prop
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.utf8Size_assemble₁ : ∀ {w : UInt8} {c : Char} {h : ByteArray.utf8DecodeChar?.parseFirstByte w = ByteArray.utf8DecodeChar?.FirstByte.done},
  ByteArray.utf8DecodeChar?.assemble₁ w h = some c → c.utf8Size = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_erase!_eq_iff_not_compare_maxKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ((Std.DTreeMap.Internal.Impl.erase! k t).maxKey! = t.maxKey! ↔ ¬compare k t.maxKey! = Ordering.eq)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.opcyclesIsoSc' i j k hi hk).inv (K.fromOpcycles j k) =
    (K.sc' i j k).fromOpcycles
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Forgetting the differentials than picking out the `i`-th object is the same as
just picking out the `i`-th object.  -/
HomologicalComplex.forgetEval : {ι : Type u_1} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        (c : ComplexShape ι) →
          (i : ι) →
            (HomologicalComplex.forget V c).comp (CategoryTheory.GradedObject.eval i) ≅ HomologicalComplex.eval V c i
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.TreeSet.Raw.ofList l cmp).getD k fallback = fallback
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.opFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : (CategoryTheory.Square C)ᵒᵖ),
  CategoryTheory.Square.opFunctor.obj sq = (Opposite.unop sq).op
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.succ_mem_succ_succ_iff : ∀ {α : Type u} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {lo a : α}, Std.PRange.succ a ∈ (Std.PRange.succ lo)<...* ↔ a ∈ lo<...*
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instInvolutiveNegOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : InvolutiveNeg Mᵃᵒᵖ], DomAddAct.instInvolutiveNegOfAddOpposite = inst
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_sup_distrib_left : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderTop α] (s : Finset ι) (f : ι → α) (a : α),
  a ⊔ s.inf f = s.inf fun i => a ⊔ f i
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.essSurj_map₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {L : D} {R : CategoryTheory.Functor C D} {L' : B}
  {R' : CategoryTheory.Functor A B} {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : L' ⟶ G.obj L)
  (β : R.comp G ⟶ F.comp R') [F.EssSurj] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β],
  (CategoryTheory.StructuredArrow.map₂ α β).EssSurj
-- Mathlib.Analysis.RCLike.Extend
/-- The extension `Module.Dual.extendRCLike` as a linear equivalence between the algebraic duals.  -/
Module.Dual.extendRCLikeₗ : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {F : Type u_2} →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module ℝ F] → [inst_3 : Module 𝕜 F] → [IsScalarTower ℝ 𝕜 F] → Module.Dual ℝ F ≃ₗ[ℝ] Module.Dual 𝕜 F
-- Init.Data.List.Basic
List.leftpad_eq_leftpadTR : @List.leftpad = @List.leftpadTR
-- Init.Core
Std.Identity.toLeftIdentity : ∀ {α : Sort u} {op : α → α → α} {o : outParam α} [self : Std.Identity op o], Std.LeftIdentity op o
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instNontrivial : ∀ {α : Type u} [Nonempty α], Nontrivial (WithOne α)
-- Lean.Attributes
Lean.AttributeApplicationTime.afterTypeChecking : Lean.AttributeApplicationTime
-- Mathlib.RingTheory.Ideal.Operations
Submodule.top_smul : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Submodule R M),
  ⊤ • N = N
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.of_ρ : ∀ {k : Type u} {G : Type v} (X : Type w) [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G]
  [inst_3 : AddCommGroup X] [inst_4 : Module k X] [inst_5 : TopologicalSpace X] [inst_6 : IsTopologicalAddGroup X]
  [inst_7 : ContinuousSMul k X] (ρ : ContRepresentation k G X), (TopRep.of ρ).ρ = ρ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  {h : (m.get? a).isSome = true}, (m.get? a).get h = m.get a ⋯
-- Mathlib.Dynamics.TopologicalEntropy.Subset
Dynamics.coverEntropyInfEntourage_monotone : ∀ {X : Type u_1} (T : X → X) (U : SetRel X X), Monotone fun F => Dynamics.coverEntropyInfEntourage T F U
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- An arbitrary choice of limit object of a functor.  -/
CategoryTheory.Limits.limit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) → [CategoryTheory.Limits.HasLimit F] → C
-- Mathlib.Data.NNReal.Basic
Real.toNNReal_sum_of_nonneg : ∀ {ι : Type u_2} {s : Finset ι} {f : ι → ℝ}, (∀ i ∈ s, 0 ≤ f i) → (∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) [Nonempty ι], f 0 = 0
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.pairing_one_four_iff' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι) [Finite ι]
  [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [Module.IsTorsionFree R N],
  IsSMulRegular R 2 → (P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i)
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_rightUnitor_hom_fst : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] {a b : B × C}
  (f : a ⟶ b), (CategoryTheory.Bicategory.rightUnitor f).hom.1 = (CategoryTheory.Bicategory.rightUnitor f.1).hom
-- Mathlib.Topology.Order.LeftRightNhds
Set.Ioo.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Ioo a b = {x | a < x ∧ x < b}
-- Mathlib.Tactic.Linter.TextBased
/-- Produce an entry in the style-exceptions file: mention the error code, slightly uglier
than human-readable output  -/
Mathlib.Linter.TextBased.ErrorFormat.exceptionsFile : Mathlib.Linter.TextBased.ErrorFormat
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.coconeAt_ι_app : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.LeftExtension F) (Y : D)
  (g : CategoryTheory.CostructuredArrow L Y),
  (E.coconeAt Y).ι.app g =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.hom E).app g.left)
      ((CategoryTheory.StructuredArrow.right E).map g.hom)
-- Mathlib.Topology.EMetricSpace.Defs
uniformity_basis_edist_nnreal_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 ≤ ↑ε}
-- Mathlib.Algebra.Quaternion
Quaternion.coe_inj : ∀ {R : Type u_3} [inst : CommRing R] {x y : R}, ↑x = ↑y ↔ x = y
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.ofComplex_apply_eq_ite : ∀ (w : ℂ), ↑UpperHalfPlane.ofComplex w = if hw : 0 < w.im then { coe := w, coe_im_pos := hw } else Classical.choice ⋯
-- Mathlib.Topology.EMetricSpace.Weak
Option.edist_some_none : ∀ {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {a : α}, edist (some a) none = ⊤
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.opcyclesMap_smul : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  (φ : S₁ ⟶ S₂) (a : R) [inst_4 : S₁.HasRightHomology] [inst_5 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.opcyclesMap (a • φ) = a • CategoryTheory.ShortComplex.opcyclesMap φ
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Two additive Haar measures coincide up to a multiplicative constant in a second countable group.  -/
MeasureTheory.Measure.isAddLeftInvariant_eq_smul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] [SecondCountableTopology G]
  (μ' μ : MeasureTheory.Measure G) [inst_7 : μ.IsAddHaarMeasure] [inst_8 : MeasureTheory.IsFiniteMeasureOnCompacts μ']
  [inst_9 : μ'.IsAddLeftInvariant], μ' = μ'.addHaarScalarFactor μ • μ
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.mul_rpow_of_ne_zero : ∀ {x y : ENNReal}, x ≠ 0 → y ≠ 0 → ∀ (z : ℝ), (x * y) ^ z = x ^ z * y ^ z
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement'.sup_eq_top : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K → H ⊔ K = ⊤
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.inter_ae_eq_empty_of_ae_eq_empty_right : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, t =ᵐ[μ] ∅ → s ∩ t =ᵐ[μ] ∅
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.neg_part : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => max (-f x) 0) p μ
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda₀_mapComp_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (x : B) {a b c : Bᵒᵖ} (f : a ⟶ b) (g : b ⟶ c)
  (X : Opposite.unop a ⟶ x),
  ((CategoryTheory.Bicategory.yoneda₀ x).mapComp f g).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop f.unop X).inv
-- Mathlib.RingTheory.SimpleModule.Isotypic
sSup_isotypicComponents : ∀ (R : Type u_2) (M : Type u) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M],
  sSup (isotypicComponents R M) = ⊤
-- Init.Meta.Defs
Lean.Meta.Occurrences.isAll : Lean.Meta.Occurrences → Bool
-- Mathlib.Data.NNRat.Defs
instLinearOrderNNRat : LinearOrder ℚ≥0
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofErase_parts : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] {a : α} (parts : Finset α)
  (sup_indep : parts.SupIndep id) (sup_parts : parts.sup id = a),
  (Finpartition.ofErase parts sup_indep sup_parts).parts = parts.erase ⊥
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sInf_le_iff : ∀ {s : Set ℝ} {a : ℝ}, BddBelow s → s.Nonempty → (sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.map_preimage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (self : F.FullyFaithful) {X Y : C} (f : F.obj X ⟶ F.obj Y),
  F.map (self.preimage f) = f
-- Init.Data.SInt.Lemmas
BitVec.ofInt_int64ToInt : ∀ (x : Int64), BitVec.ofInt 64 x.toInt = x.toBitVec
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
_private.Mathlib.MeasureTheory.Integral.Lebesgue.Sub.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.ofLeftExact_map_hom : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : CategoryTheory.Limits.HasZeroObject D]
  [inst_6 : CategoryTheory.Limits.HasBinaryBiproducts C] {F G : C ⥤ₗ D} (α : F ⟶ G),
  ((CategoryTheory.AdditiveFunctor.ofLeftExact C D).map α).hom = α.hom
-- Lean.MetavarContext
/-- Add `mvarId := u` to the universe metavariable assignment.
This method does not check whether `mvarId` is already assigned, nor does it check whether
a cycle is being introduced.
This is a low-level API, and it is safer to use `isLevelDefEq (mkLevelMVar mvarId) u`.
 -/
Lean.assignLevelMVar : {m : Type → Type} → [Lean.MonadMCtx m] → Lean.LMVarId → Lean.Level → m Unit
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.le_comap_map : ∀ {α : Type u_1} {β : Type u_3} (f : α → β) (m : MeasureTheory.OuterMeasure α),
  m ≤ (MeasureTheory.OuterMeasure.comap f) ((MeasureTheory.OuterMeasure.map f) m)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.isOpen_iff : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (U : Set (ProjectiveSpectrum 𝒜)), IsOpen U ↔ ∃ s, Uᶜ = ProjectiveSpectrum.zeroLocus 𝒜 s
-- Aesop.Script.OptimizeSyntax
Aesop.optimizeInitialRenameI : {m : Type → Type} → [Monad m] → [Lean.MonadQuotation m] → Lean.Syntax → m Lean.Syntax
-- Mathlib.CategoryTheory.Products.Basic
/-- `prod C D` gives the Cartesian product of two categories.  -/
CategoryTheory.prod' : (C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} (C × D)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
AbsConvex.closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E},
  AbsConvex 𝕜 s → AbsConvex 𝕜 (closure s)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_mono_real : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F} {g : α → ℝ},
  (∀ (x : α), ‖f x‖ ≤ g x) → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
-- Mathlib.Algebra.Group.Ext
AddCancelMonoid.ext_iff : ∀ {M : Type u_1} {m₁ m₂ : AddCancelMonoid M}, m₁ = m₂ ↔ HAdd.hAdd = HAdd.hAdd
-- Mathlib.RingTheory.Morita.Matrix
ModuleCat.matrixEquivalence_inverse : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι),
  (ModuleCat.matrixEquivalence R i).inverse = MatrixModCat.toModuleCat R i
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- Determinant of a transvection, over a domain.

See `LinearMap.transvection.det` for the general case.  -/
_private.Mathlib.LinearAlgebra.Transvection.Basic.0.LinearMap.transvection.det_ofDomain : ∀ {R : Type u_3} {V : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] [Module.Free R V]
  [Module.Finite R V] [IsDomain R] (f : Module.Dual R V) (v : V), LinearMap.det (LinearMap.transvection f v) = 1 + f v
-- Mathlib.Topology.Order.LeftRightLim
tendsto_rightLim_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → β} {a : α},
  (∃ y, Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds y)) →
    Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds (Function.rightLim f a))
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanrM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m β) (init : β) (xs : List α),
  List.scanrM f init xs = List.scanAuxM✝ (flip f) init xs.reverse
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_smul_measure : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (c : ENNReal) {s : Set α},
  MeasureTheory.weightedSMul (c • μ) s = c.toReal • MeasureTheory.weightedSMul μ s
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierTransform_toLp : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  {f : V → E} (hf : MeasureTheory.MemLp f 1 MeasureTheory.volume),
  ⇑(Real.Lp.fourierTransform (MeasureTheory.MemLp.toLp f hf)) = FourierTransform.fourier f
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.eraseOptVar : Lean.Elab.Term.Do.VarSet → Option Lean.Elab.Term.Do.Var → Lean.Elab.Term.Do.VarSet
-- Aesop.Index.Forward
/-- Insert a forward rule into the `ForwardIndex`.  -/
Aesop.ForwardIndex.insert : Aesop.ForwardRule → Aesop.ForwardIndex → Aesop.ForwardIndex
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.mk : {X : SSet.Truncated 2} →
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    (edge : X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 })) →
      autoParam
          ((CategoryTheory.ConcreteCategory.hom
                (X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
              edge =
            x₀)
          SSet.Truncated.Edge.src_eq._autoParam →
        autoParam
            ((CategoryTheory.ConcreteCategory.hom
                  (X.map (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
                edge =
              x₁)
            SSet.Truncated.Edge.tgt_eq._autoParam →
          SSet.Truncated.Edge x₀ x₁
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the reverse direction of `Asymptotics.isLittleO_norm_right`. -/
Asymptotics.IsLittleO.norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =o[l] g' → f =o[l] fun x => ‖g' x‖
-- Mathlib.Order.Bounds.Basic
BddAbove.dual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove s → BddBelow (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.Hom.hom_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : CategoryTheory.Mon C} [inst_3 : CategoryTheory.IsCommMonObj N.X],
  CategoryTheory.Mon.Hom.hom 1 = 1
-- Mathlib.Tactic.NormNum.Prime
/-- The `norm_num` extension which identifies expressions of the form `minFac n`.  -/
Mathlib.Meta.NormNum.evalMinFac : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.Star.Basic
star_sub : ∀ {R : Type u} [inst : AddGroup R] [inst_1 : StarAddMonoid R] (r s : R), star (r - s) = star r - star s
-- Mathlib.Algebra.Order.Group.DenselyOrdered
le_iff_forall_neg_add_le : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] [DenselyOrdered α] {a b : α},
  a ≤ b ↔ ∀ ε < 0, a + ε ≤ b
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- The weighted sum of squares with respect to some weight as a quadratic form.

The weights are applied using `•`; typically this definition is used either with `S = R` or
`[Algebra S R]`, although this is stated more generally.  -/
QuadraticMap.weightedSumSquares : {S : Type u_1} →
  (R : Type u_3) →
    [inst : CommSemiring R] →
      {ι : Type u_8} →
        [Fintype ι] →
          [inst_2 : Monoid S] →
            [inst_3 : DistribMulAction S R] → [SMulCommClass S R R] → (ι → S) → QuadraticMap R (ι → R) R
-- Mathlib.RingTheory.Flat.Rank
/-- If `S` is a finite, flat `R`-algebra, `S` is of constant rank `1` if and only if
`S` is isomorphic to `R`.  -/
Module.algebraMap_bijective_iff_rankAtStalk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S], Module.rankAtStalk S = 1 ↔ Function.Bijective ⇑(algebraMap R S)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.instCoeTypeForall_1 : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
LocallyFiniteOrder.orderMonoidWithZeroHom.eq_1 : ∀ (G : Type u_3) [inst : LinearOrderedCommGroupWithZero G] [inst_1 : LocallyFiniteOrder Gˣ],
  LocallyFiniteOrder.orderMonoidWithZeroHom G =
    {
      toMonoidWithZeroHom :=
        (WithZero.map' ↑(LocallyFiniteOrder.orderMonoidHom Gˣ)).comp
          OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom,
      monotone' := ⋯ }
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- The empty set has Dirichlet density `0`.  -/
NumberField.Set.hasDirichletDensity_empty : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], NumberField.Set.HasDirichletDensity ∅ 0
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.enorm_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E), ‖f x‖ₑ = ‖x‖ₑ
-- Lean.Parser.Types
Lean.Parser.InputContext.endPos : Lean.Parser.InputContext → String.Pos.Raw
-- Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
/-- If the quadratic form of a vector is invertible, then so is that vector.  -/
CliffordAlgebra.invertibleιOfInvertible : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (Q : QuadraticForm R M) → (m : M) → [Invertible (Q m)] → Invertible ((CliffordAlgebra.ι Q) m)