mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- Given a t-structure `t` on a pretriangulated category `C` and `n : ℤ`, this
is the `< n`-truncation functor. See also the natural transformation `truncLTι`.  -/
CategoryTheory.Triangulated.TStructure.truncLT : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → ℤ → CategoryTheory.Functor C C
-- Mathlib.Algebra.Group.Basic
mul_div_left_comm : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a * (b / c) = b * (a / c)
-- Mathlib.Order.Interval.Set.Basic
/-- An interval `Ici a` is nonempty.  -/
Set.nonempty_Ici_subtype : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Nonempty ↑(Set.Ici a)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertIfNew.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β),
  m = m_1 → ∀ (a a_1 : α), a = a_1 → ∀ (b b_1 : β), b = b_1 → m.insertIfNew a b = m_1.insertIfNew a_1 b_1
-- Mathlib.Analysis.Normed.Field.Basic
Real.normedField : NormedField ℝ
-- Init.Data.SInt.Bitwise
instCommutativeInt64HXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.toIsAdjoinRoot : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → {f : Polynomial R} → IsAdjoinRootMonic S f → IsAdjoinRoot S f
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.lintegral_mono_fun : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : MeasureTheory.SimpleFunc α ENNReal},
  f ≤ g → f.lintegral μ ≤ g.lintegral μ
-- Mathlib.Order.Interval.Finset.Defs
/-- Transfer `LocallyFiniteOrderBot` across an `OrderIso`.  -/
OrderIso.locallyFiniteOrderBot : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [LocallyFiniteOrderBot β] → α ≃o β → LocallyFiniteOrderBot α
-- Mathlib.Analysis.Convex.Gauge
gauge_sum_le : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {ι : Type u_3},
  Convex ℝ s → Absorbent ℝ s → ∀ (t : Finset ι) (f : ι → E), gauge s (∑ i ∈ t, f i) ≤ ∑ i ∈ t, gauge s (f i)
-- Lean.Linter.UnusedVariables
/-- The set of all (ranges corresponding to) global definitions that are made in the syntax.
For example in `mutual def foo := ...  def bar := ... where baz := ... end` this would be
the spans for `foo`, `bar`, and `baz`. Global definitions are always treated as used.
(It would be nice to be able to detect unused global definitions but this requires more
information than the linter framework can provide.)  -/
Lean.Linter.UnusedVariables.References.constDecls : Lean.Linter.UnusedVariables.References → Std.HashSet Lean.Syntax.Range
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.of.sizeOf_spec : ∀ (carrier : Type u) [str : OmegaCompletePartialOrder carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.composePath_comp' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : CategoryTheory.Paths C} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.composePath (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.composePath f) (CategoryTheory.composePath g)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.quasiCoherentData_presentation_relations_I : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.LocalGeneratorsData) [inst_3 : q.IsLocallyFreeData] (i : q.I),
  (q.quasiCoherentData.presentation i).relations.I = ULift.{u, 0} Empty
-- Lean.PrettyPrinter
_private.Lean.PrettyPrinter.0.Lean.PrettyPrinter.withoutContext : {α : Type u_1} → {m : Type u_1 → Type u_2} → [MonadExcept Lean.Exception m] → m α → m α
-- Mathlib.Algebra.Lie.BaseChange
LieSubmodule.baseChange.eq_1 : ∀ {R : Type u_1} (A : Type u_2) {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A] (N : LieSubmodule R L M),
  LieSubmodule.baseChange A N = { toSubmodule := Submodule.baseChange A ↑N, lie_mem := ⋯ }
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
MeasureTheory.Measure.condKernel.congr_simp : ∀ {α : Type u_5} {Ω : Type u_6} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  [inst_1 : Nonempty Ω] (ρ ρ_1 : MeasureTheory.Measure (α × Ω)) (e_ρ : ρ = ρ_1)
  [inst_2 : MeasureTheory.IsFiniteMeasure ρ], ρ.condKernel = ρ_1.condKernel
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toArray_succ_eq_map : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.InfinitelyUpwardEnumerable α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α] [inst_8 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_9 : Std.PRange.LawfulUpwardEnumerableLeast? α] {hi : α},
  (*...=Std.PRange.succ hi).toArray =
    #[Std.PRange.UpwardEnumerable.least] ++ Array.map Std.PRange.succ (*...=hi).toArray
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.instLinearIntShiftFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ) {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C],
  CategoryTheory.Functor.Linear R (CochainComplex.shiftFunctor C n)
-- Mathlib.Analysis.Calculus.Rademacher
LipschitzWith.integral_inv_smul_sub_mul_tendsto_integral_lineDeriv_mul' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f g : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzWith C f →
    HasCompactSupport f →
      Continuous g →
        ∀ (v : E),
          Filter.Tendsto (fun t => ∫ (x : E), t⁻¹ • (f (x + t • v) - f x) * g x ∂μ) (nhdsWithin 0 (Set.Ioi 0))
            (nhds (∫ (x : E), lineDeriv ℝ f x v * g x ∂μ))
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.nonempty_leftResolution_iff_op : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂),
  Nonempty (Φ.LeftResolution X₂) ↔ Nonempty (Φ.op.RightResolution (Opposite.op X₂))
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- The condition that a property of morphisms is stable by coproducts.  -/
CategoryTheory.MorphismProperty.IsStableUnderCoproducts : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- A braided monoidal category is a monoidal category equipped with a braiding isomorphism
`β_ X Y : X ⊗ Y ≅ Y ⊗ X`
which is natural in both arguments,
and also satisfies the two hexagon identities.
 -/
CategoryTheory.BraidedCategory : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)
-- Mathlib.Data.List.Basic
List.append_subset_of_subset_of_subset : ∀ {α : Type u} {l₁ l₂ l : List α}, l₁ ⊆ l → l₂ ⊆ l → l₁ ++ l₂ ⊆ l
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_eq_one : ∀ {α : Type u} [inst : Preorder α] [OrderTop α], Order.cof α = 1
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.induction_on : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {motive : Monoid.CoprodI M → Prop}
  (m : Monoid.CoprodI M),
  motive 1 →
    (∀ (i : ι) (m : M i), motive (Monoid.CoprodI.of m)) →
      (∀ (x y : Monoid.CoprodI M), motive x → motive y → motive (x * y)) → motive m
-- Mathlib.Data.Rat.Cast.Order
/-- Extension for NNRat.cast.  -/
Mathlib.Meta.Positivity.evalNNRatCast : Mathlib.Meta.Positivity.PositivityExt
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.RingTheory.Finiteness.Basic
AlgHom.Finite.of_comp_finite : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  {f : A →ₐ[R] B} {g : B →ₐ[R] C}, (g.comp f).Finite → g.Finite
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : F ≅ G),
  (CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso α).functor =
    CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans α.hom
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_shiftLeft : ∀ (a b : ISize) (h : System.Platform.numBits = 64), (a <<< b).toBitVec64 h = a.toBitVec64 h <<< (b.toBitVec64 h).smod 64
-- Init.Data.Nat.Lcm
Nat.lcm_assoc : ∀ (m n k : ℕ), (m.lcm n).lcm k = m.lcm (n.lcm k)
-- Init.Data.SInt.Lemmas
Int64.toNat_toUInt64_of_le : ∀ {x : Int64}, 0 ≤ x → x.toUInt64.toNat = x.toNatClampNeg
-- Init.Data.Nat.Basic
Nat.mul_two : ∀ (n : ℕ), n * 2 = n + n
-- Mathlib.NumberTheory.Padics.MahlerBasis
PadicInt.mahlerTerm.eq_1 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] (a : E) (n : ℕ), PadicInt.mahlerTerm a n = mahler n • ContinuousMap.const ℤ_[p] a
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.sub_one_ne_zero : ∀ {p q : NNReal}, p.HolderConjugate q → p - 1 ≠ 0
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- The homeomorphism obtained by restricting an `OpenPartialHomeomorph` to a subset of the source.
 -/
OpenPartialHomeomorph.homeomorphOfImageSubsetSource : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : OpenPartialHomeomorph X Y) → {s : Set X} → {t : Set Y} → s ⊆ e.source → ↑e '' s = t → ↑s ≃ₜ ↑t
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- `PreservesFilteredColimitsOfSize.{w', w} F` means that `F` sends all colimit cocones over any
filtered diagram `J ⥤ C` to colimit cocones, where `J : Type w` with `[Category.{w'} J]`.  -/
CategoryTheory.Limits.PreservesFilteredColimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalComp_nil_cons : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g h i j : C} (α : f ≅ g) (β : g ≅ h) (η : h ⟶ i)
  (ηs : i ⟶ j),
  CategoryTheory.CategoryStruct.comp α.hom
      (CategoryTheory.CategoryStruct.comp β.hom (CategoryTheory.CategoryStruct.comp η ηs)) =
    CategoryTheory.CategoryStruct.comp (α ≪≫ β).hom (CategoryTheory.CategoryStruct.comp η ηs)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_pos' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [ν.HaveLebesgueDecomposition μ]
  [MeasureTheory.SigmaFinite μ], μ.AbsolutelyContinuous ν → ∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x
-- Init.Data.Int.Lemmas
Int.neg_add_cancel_left : ∀ (a b : ℤ), -a + (a + b) = b
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Functor.mapComon_obj_comon_counit : ∀ {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.OplaxMonoidal] (A : CategoryTheory.Comon C),
  CategoryTheory.ComonObj.counit =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.ComonObj.counit) (CategoryTheory.Functor.OplaxMonoidal.η F)
-- Batteries.Data.String.Lemmas
String.utf8SetAux_of_valid : ∀ (c' : Char) (cs cs' : List Char) {i p : ℕ},
  i + String.utf8Len cs = p →
    String.Pos.Raw.utf8SetAux c' (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs ++ List.modifyHead (fun x => c') cs'
-- Mathlib.RingTheory.LocalProperties.Basic
/-- A property of ring homs is local if it is preserved by localizations and compositions, and for
each `{ r }` that spans `S`, we have `P (R →+* S) ↔ ∀ r, P (R →+* Sᵣ)`.  -/
RingHom.PropertyIsLocal : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.isGE_iff_orthogonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ → ∀ (X : C), t.IsGE X n₁ ↔ ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
-- Mathlib.Data.Nat.Cast.Basic
/-- This lemma is not marked `@[simp]` lemma because its `#discr_tree_key` (for the LHS) would just
be `DFunLike.coe _ _`, due to the `ofNat` that https://github.com/leanprover/lean4/issues/2867
forces us to include, and therefore it would negatively impact performance.

If that issue is resolved, this can be marked `@[simp]`.  -/
map_ofNat : ∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : FunLike F R S] [RingHomClass F R S] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo],
  f (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.«termλ⁻¹_» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.exp_sub_sum_range_succ_isLittleO_pow : ∀ (n : ℕ), (fun x => Real.exp x - ∑ i ∈ Finset.range (n + 1), x ^ i / ↑i.factorial) =o[nhds 0] fun x => x ^ n
-- Init.Data.Range.Polymorphic.UInt
UInt32.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize UInt32
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).size = t.size
-- Init.Data.Order.Ord
compareOn.eq_1 : ∀ {β : Type u_1} {α : Sort u_2} [ord : Ord β] (f : α → β) (x y : α), compareOn f x y = compare (f x) (f y)
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.isClosedUnderIsomorphisms_iff_isoClosure_eq_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.IsClosedUnderIsomorphisms ↔ P.isoClosure = P
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → Std.ExtDTreeMap.Const.get? (t₁.union t₂) k = Std.ExtDTreeMap.Const.get? t₁ k
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_app : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens),
  AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.CategoryStruct.comp f g) U =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app g U)
      (AlgebraicGeometry.Scheme.Hom.app f ((TopologicalSpace.Opens.map g.base).obj U))
-- Lean.Server.Rpc.Basic
Lean.Server.rpcGetRef : (α : Type) →
  [TypeName α] → Lean.Lsp.RpcRef → ReaderT Lean.Server.RpcObjectStore (ExceptT String Id) (Lean.Server.WithRpcRef α)
-- Mathlib.Order.RelIso.Basic
RelIso.IsWellOrder.preimage : ∀ {β : Type u_2} {α : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β ≃ α), IsWellOrder β (⇑f ⁻¹'o r)
-- Mathlib.Algebra.Group.Finsupp
AddEquiv.finsuppUnique_symm_apply_support_val : ∀ {M : Type u_3} [inst : AddZeroClass M] {ι : Type u_8} [inst_1 : Unique ι] (a : M),
  (AddEquiv.finsuppUnique.symm a).support.val =
    Multiset.map (⇑(Function.Embedding.subtype fun x => x ∈ Function.support (uniqueElim a))) Finset.univ.val
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toLinearEquiv_injective : ∀ {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₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
  [inst_7 : Module R₂ E₂], Function.Injective LinearIsometryEquiv.toLinearEquiv
-- Mathlib.Topology.LocallyFinsupp
/-- Every positive function with locally finite supports dominates a singleton indicator.
 -/
Function.locallyFinsuppWithin.exists_single_le_pos : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : DecidableEq X] {D : Function.locallyFinsupp X ℤ},
  0 < D → ∃ e, Function.locallyFinsuppWithin.single e 1 ≤ D
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.instAddCommGroupQuotient : {A : Type u_1} → [inst : Ring A] → (relations : Module.Relations A) → AddCommGroup relations.Quotient
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.erase.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → t.erase a = t_1.erase a_1
-- Std.Http.Protocol.H1
/-- Runs a parser against reader input and translates parser outcomes into machine
state transitions.

- On success, advances reader input.
- On EOF with open input, emits `needMoreData`.
- On EOF after `noMoreInput`, fails with `connectionClosed`.
- On hard parse errors or size-limit breaches, fails with `onHardError`.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.parseWith : {dir : Std.Http.Protocol.H1.Direction} →
  {α : Type} →
    Std.Http.Protocol.H1.Machine dir →
      Std.Internal.Parsec.ByteArray.Parser α →
        Option ℕ →
          optParam (Option ℕ) none →
            (optParam (Std.Internal.Parsec.Error → Std.Http.Protocol.H1.Error) fun x =>
                Std.Http.Protocol.H1.Error.badMessage) →
              Std.Http.Protocol.H1.Machine dir × Option α
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.e0.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), CliffordAlgebra.EquivEven.e0 Q = (CliffordAlgebra.ι (CliffordAlgebra.EquivEven.Q' Q)) (0, 1)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.val_expOrderIso_apply : ∀ {G : Type u_3} [inst : Preorder G] [inst_1 : AddGroup G] (a : G),
  ↑(WithZero.expOrderIso a) = ↑(Multiplicative.ofAdd a)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.elimOffset : {α : Sort u} → (a b k : ℕ) → a + k = b + k → (a = b → α) → α
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
UpperSemicontinuous.measurable : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  [inst : TopologicalSpace δ] [OpensMeasurableSpace δ] {f : δ → α}, UpperSemicontinuous f → Measurable f
-- Mathlib.Algebra.FreeMonoid.Count
FreeMonoid.countP'_mul : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l₁ l₂ : FreeMonoid α),
  FreeMonoid.countP' p (l₁ * l₂) = FreeMonoid.countP' p l₁ + FreeMonoid.countP' p l₂
-- Mathlib.Algebra.Algebra.Epi
Algebra.isEpi_iff_surjective_algebraMap_of_finite : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Module.Finite R A],
  Algebra.IsEpi R A ↔ Function.Surjective ⇑(algebraMap R A)
-- Mathlib.Order.Filter.Subsingleton
Filter.subsingleton_pure : ∀ {α : Type u_1} {a : α}, (pure a).Subsingleton
-- Init.Omega.IntList
/-- Implementation of subtraction on `IntList`.  -/
Lean.Omega.IntList.sub : Lean.Omega.IntList → Lean.Omega.IntList → Lean.Omega.IntList
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C) (p : X ⟶ X)
  (idem : autoParam (CategoryTheory.CategoryStruct.comp p p = p) CategoryTheory.Idempotents.Karoubi.idem._autoParam)
  (X_1 : C) (p_1 : X_1 ⟶ X_1)
  (idem_1 :
    autoParam (CategoryTheory.CategoryStruct.comp p_1 p_1 = p_1) CategoryTheory.Idempotents.Karoubi.idem._autoParam),
  ({ X := X, p := p, idem := idem } = { X := X_1, p := p_1, idem := idem_1 }) = (X = X_1 ∧ p ≍ p_1)
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.lift_algebraMap : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {B : Type w'} [inst_4 : Semiring B]
  [inst_5 : Algebra R B] (maps : {i : I} → A i →ₐ[R] B) (r : R),
  ((LinearAlgebra.FreeProduct.lift R A) fun {i} => maps) ((algebraMap R (LinearAlgebra.FreeProduct R A)) r) =
    (algebraMap R B) r
-- Mathlib.AlgebraicGeometry.EffectiveEpi
/-- If `π : X ⟶ Y` is a surjective and flat morphism between affine schemes, then any morphism
`f : X ⟶ S` to an affine scheme `S` whose two pullbacks to `X ×[Y] X` agree descends to a morphism
`u : Y ⟶ S` with `π ≫ u = f`.  -/
_private.Mathlib.AlgebraicGeometry.EffectiveEpi.0.AlgebraicGeometry.EffectiveEpiConstruction.of_isAffine_target : ∀ {X Y S : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y] (π : X ⟶ Y)
  [AlgebraicGeometry.Surjective π] [AlgebraicGeometry.Flat π] (f : X ⟶ S),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst π π) f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd π π) f →
    ∀ [AlgebraicGeometry.IsAffine S], ∃ u, CategoryTheory.CategoryStruct.comp π u = f
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₁)}
  (h : (F.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).inv.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId b₀).hom.toNatTrans.app X)) h
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_unique : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) {j : N →* P},
  (∀ (x : M), j (f x) = g x) → f.lift hg = j
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.IsHomotopyInvariant.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP : TopPair.HomologyPretheory C c},
  autoParam (∀ {X Y : TopPair} {f g : X ⟶ Y} (F : TopPair.Homotopy f g) (i : ι), (HP.Hₚ i).map f = (HP.Hₚ i).map g)
      TopPair.HomologyPretheory.IsHomotopyInvariant.map_eq_of_homotopy._autoParam →
    HP.IsHomotopyInvariant
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of February.
 -/
Std.Time.Month.Ordinal.february : Std.Time.Month.Ordinal