mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
/-- Let `c₁` (resp. `c₂`) be a colimit cokernel cofork for a morphism `f₁ : X₁ ⟶ Y₁`
in a category `C₁` (resp. `f₂ : X₂ ⟶ Y₂` in `C₂`). If `F : C₁ ⥤ C₂ ⥤ C` is a bifunctor,
then `(F.obj c₁.pt).obj c₂.pt` identifies to the cokernel of the morphism
`(F.obj X₁).obj Y₂ ⨿ (F.obj Y₁).obj X₂ ⟶ (F.obj Y₁).obj Y₂`
when the cokernel of `f₁` is preserved by `F.obj c₁.pt` and the cokernel of `f₂`
is preserved by `F.flip.obj X₁` and `F.flip.obj Y₁`.  -/
CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  {X₁ Y₁ : C₁} →
                    {f₁ : X₁ ⟶ Y₁} →
                      {c₁ : CategoryTheory.Limits.CokernelCofork f₁} →
                        CategoryTheory.Limits.IsColimit c₁ →
                          {X₂ Y₂ : C₂} →
                            {f₂ : X₂ ⟶ Y₂} →
                              {c₂ : CategoryTheory.Limits.CokernelCofork f₂} →
                                CategoryTheory.Limits.IsColimit c₂ →
                                  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) →
                                    [inst_6 : (F.obj c₁.pt).PreservesZeroMorphisms] →
                                      [inst_7 : F.PreservesZeroMorphisms] →
                                        [CategoryTheory.Limits.PreservesColimit
                                              (CategoryTheory.Limits.parallelPair f₂ 0) (F.obj c₁.pt)] →
                                          [CategoryTheory.Limits.PreservesColimit
                                                (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj Y₂)] →
                                            [inst_10 :
                                                CategoryTheory.Limits.HasBinaryCoproduct ((F.obj X₁).obj Y₂)
                                                  ((F.obj Y₁).obj X₂)] →
                                              [CategoryTheory.Limits.PreservesColimit
                                                    (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj X₂)] →
                                                CategoryTheory.Limits.IsColimit (c₁.mapBifunctor c₂ F)
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.isIso_g_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact → ∀ [CategoryTheory.Balanced C], CategoryTheory.IsIso S.g ↔ CategoryTheory.Limits.IsZero S.X₁
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.le_maxKeyD_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.finrank_lt_finrank_of_lt : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s t : Submodule K V} [FiniteDimensional K ↥t], s < t → Module.finrank K ↥s < Module.finrank K ↥t
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α} [inst_2 : Inhabited β],
  (List.map Prod.fst l).contains k = false → (Std.ExtHashMap.ofList l)[k]! = default
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_rio_eq_self : ∀ {n i fallback : ℕ}, i < n → (*...n).toArray.getD i fallback = i
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.inclusion.injective : ∀ {V : Type u} {G : SimpleGraph V} {x y : G.Subgraph} (h : x ≤ y),
  Function.Injective ⇑(SimpleGraph.Subgraph.inclusion h)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instLattice : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : NormedAddCommGroup β] →
        [inst_2 : Lattice β] → [HasSolidNorm β] → [IsOrderedAddMonoid β] → Lattice (BoundedContinuousFunction α β)
-- Lean.Data.Lsp.Internal
/-- References from a single module/file  -/
Lean.Lsp.ModuleRefs : Type
-- Mathlib.Data.Int.Log
/-- Over suitable subtypes, `Int.clog` and `zpow` form a Galois insertion  -/
Int.clogZPowGi : (R : Type u_1) →
  [inst : Semifield R] →
    [inst_1 : LinearOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        [inst_3 : FloorSemiring R] →
          {b : ℕ} → (hb : 1 < b) → GaloisInsertion (fun r => Int.clog b ↑r) fun z => ⟨↑b ^ z, ⋯⟩
-- Init.Data.List.ControlImpl
List.flatMapM_eq_flatMapMTR : @List.flatMapM = @List.flatMapMTR
-- Mathlib.Probability.Kernel.Condexp
MeasureTheory.Integrable.integral_condExpKernel : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F],
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable (fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω) μ
-- Init.Data.String.Lemmas.Basic
String.sliceTo_slice : ∀ {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂} {p : (s.slice p₁ p₂ h).Pos},
  (s.slice p₁ p₂ h).sliceTo p = s.slice p₁ (String.Pos.ofSlice p) ⋯
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNormEssSup_const_smul : ∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {𝕜 : Type u_3} [inst_1 : NormedDivisionRing 𝕜] [inst_2 : Module 𝕜 F] [NormSMulClass 𝕜 F] (c : 𝕜) (f : α → F),
  MeasureTheory.eLpNormEssSup (c • f) μ = ‖c‖ₑ * MeasureTheory.eLpNormEssSup f μ
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instPartialOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] {x : CompleteLattice β},
  sInfHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.isEmpty = false
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_succ' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] (n : ℕ),
  P.extensionProductIter (n + 1) = (P.extensionProductIter n).extensionProduct P
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, k ∉ t₁ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.linearEquiv_of_isLocalizedModule_comp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f] (g : M' →ₗ[R] M'')
  [inst_8 : IsLocalizedModule S (g ∘ₗ f)], ↑(IsLocalizedModule.linearEquiv S f (g ∘ₗ f)) = g
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.mk.injEq : ∀ (declName? : Option Lean.Name) (options : Lean.Options) (openDecls : List Lean.OpenDecl)
  (macroStack : Lean.Elab.MacroStack) (errToSorry : Bool) (levelNames : List Lean.Name)
  (fixedTermElabs : Array Lean.Elab.Term.FixedTermElabRef) (declName?_1 : Option Lean.Name) (options_1 : Lean.Options)
  (openDecls_1 : List Lean.OpenDecl) (macroStack_1 : Lean.Elab.MacroStack) (errToSorry_1 : Bool)
  (levelNames_1 : List Lean.Name) (fixedTermElabs_1 : Array Lean.Elab.Term.FixedTermElabRef),
  ({ declName? := declName?, options := options, openDecls := openDecls, macroStack := macroStack,
        errToSorry := errToSorry, levelNames := levelNames, fixedTermElabs := fixedTermElabs } =
      { declName? := declName?_1, options := options_1, openDecls := openDecls_1, macroStack := macroStack_1,
        errToSorry := errToSorry_1, levelNames := levelNames_1, fixedTermElabs := fixedTermElabs_1 }) =
    (declName? = declName?_1 ∧
      options = options_1 ∧
        openDecls = openDecls_1 ∧
          macroStack = macroStack_1 ∧
            errToSorry = errToSorry_1 ∧ levelNames = levelNames_1 ∧ fixedTermElabs = fixedTermElabs_1)
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.coe_real_preimage_closedBall_eq_iUnion : ∀ (p x ε : ℝ), QuotientAddGroup.mk ⁻¹' Metric.closedBall (↑x) ε = ⋃ z, Metric.closedBall (x + z • p) ε
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ext_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {t₁ t₂ : Std.ExtTreeSet α cmp},
  (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁ = t₂
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instBEqConfig : BEq Mathlib.Tactic.RingNF.Config
-- Mathlib.Data.Set.Finite.Basic
Set.finite_range_ite : ∀ {α : Type u} {β : Type v} {p : α → Prop} [inst : DecidablePred p] {f g : α → β},
  (Set.range f).Finite → (Set.range g).Finite → (Set.range fun x => if p x then f x else g x).Finite
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedOneHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N], instInhabitedOneHom = { default := 1 }
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s : Set M} {x : M}
  {n : WithTop ℕ∞},
  ContMDiffWithinAt I I' n f s x → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → ContMDiffWithinAt I I' n f₁ s x
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_35 : HAdd Std.Time.Day.Offset Std.Time.Week.Offset Std.Time.Day.Offset
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.X_pow_mul_assoc : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {n : ℕ}, p * Polynomial.X ^ n * q = p * q * Polynomial.X ^ n
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.extendScalarsHomOfSurjective_apply : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A ≃ₐ[R] A),
  (AlgEquiv.extendScalarsHomOfSurjective h) f = { toEquiv := ↑f, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_inverse_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (c : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C))
  {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y),
  (CategoryTheory.WithTerminal.equivComma.inverse.obj c).map f =
    match X, Y, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
      c.left.map (CategoryTheory.WithTerminal.down f)
    | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => c.hom.app x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id c.right
-- Mathlib.Data.Finsupp.Defs
/-- The witness that the support of a `Finsupp` is indeed the exact locus where its
underlying function is nonzero.  -/
Finsupp.mem_support_toFun : ∀ {α : Type u_9} {M : Type u_10} [inst : Zero M] (self : α →₀ M) (a : α), a ∈ self.support ↔ self.toFun a ≠ 0
-- Mathlib.Tactic.Positivity.Core
/-- Attempts to prove an expression `e : α` is `>0`, `≥0`, or `≠0`.  -/
Mathlib.Meta.Positivity.PositivityExt.eval : Mathlib.Meta.Positivity.PositivityExt →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      (zα : Q(Zero «$α»)) →
        (pα? : Option Q(PartialOrder «$α»)) → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.induction : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f : M →ₗ[R] A},
  IsSymmetricAlgebra f →
    ∀ {motive : A → Prop},
      (∀ (r : R), motive ((algebraMap R A) r)) →
        (∀ (x : M), motive (f x)) →
          (∀ (a b : A), motive a → motive b → motive (a * b)) →
            (∀ (a b : A), motive a → motive b → motive (a + b)) → ∀ (a : A), motive a
-- Init.Data.Option.Basic
/-- Lifts an optional value to any `Alternative`, sending `none` to `failure`.  -/
Option.getM : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Alternative m] → Option α → m α
-- Lean.DocString.Types
Lean.Doc.instBEqMathMode : BEq Lean.Doc.MathMode
-- Mathlib.Topology.UrysohnsLemma
/-- The proof that `C` and `U` satisfy the property `P C U`  -/
Urysohns.CU.P_C_U : ∀ {X : Type u_2} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (self : Urysohns.CU P), P self.C self.U
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
/-- Modular forms of odd weight for `𝒮ℒ` are zero-dimensional.  -/
ModularForm.levelOne_odd_weight_rank_zero : ∀ {k : ℤ}, Odd k → Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) = 0
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.ofRingCon.inj : ∀ {R : Type u_1} {inst : NonUnitalNonAssocRing R} {ringCon ringCon_1 : RingCon R},
  { ringCon := ringCon } = { ringCon := ringCon_1 } → ringCon = ringCon_1
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.instHasInjectiveResolution : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.EnoughInjectives C] (Z : C), CategoryTheory.HasInjectiveResolution Z
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement'.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [inst_2 : Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements),
  CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement' F =
    CategoryTheory.Limits.Types.Limit.mk ((F.comp (CategoryTheory.CategoryOfElements.π A)).comp A)
      (fun i => (F.obj i).snd) ⋯
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H1Iso_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.shortComplexH1 A).moduleCatLeftHomologyData.π
      (groupHomology.H1Iso A).inv =
    groupHomology.H1π A
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- Notation for the pullback-hom of morphisms.  -/
CategoryTheory.MonoidalCategory.Arrow.«term_⋔_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.irrelevant_eq_closure : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜],
  (HomogeneousIdeal.irrelevant 𝒜).toAddSubmonoid = AddSubmonoid.closure (⋃ i, ⋃ (_ : i > 0), ↑(𝒜 i))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.isZero_trivial : ∀ (D : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D],
  CategoryTheory.Limits.IsZero (CategoryTheory.AddMon.trivial D)
-- Mathlib.GroupTheory.Coset.Basic
AddMonoidHom.fiberEquiv_apply : ∀ {α : Type u_1} [inst : AddGroup α] {H : Type u_2} [inst_1 : AddGroup H] (f : α →+ H) (a b : α) (g : ↑(⇑f ⁻¹' {f a})),
  ↑((f.fiberEquiv a b) g) = b + (-a + ↑g)
-- Mathlib.Geometry.Euclidean.Triangle
/-- A variant of the law of sines, angle-at-point form.  -/
EuclideanGeometry.sin_angle_div_dist_eq_sin_angle_div_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  p₂ ≠ p₃ →
    p₃ ≠ p₁ →
      Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) / dist p₃ p₁ =
        Real.sin (EuclideanGeometry.angle p₃ p₁ p₂) / dist p₂ p₃
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.invLimEquiv_symm_apply_coe : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι]
  {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} {equiv : (j : ↑(Set.Iio i)) → F ↑j ≃ InverseSystem.piLT X ↑j}
  (nat : InverseSystem.IsNatEquiv f equiv) (t : ↑(InverseSystem.limit InverseSystem.piLTProj i)) (l : ↑(Set.Iio i)),
  ↑((InverseSystem.invLimEquiv nat).symm t) l = (equiv l).symm (↑t l)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
left_vsub_midpoint : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ : P), p₁ -ᵥ midpoint R p₁ p₂ = ⅟2 • (p₁ -ᵥ p₂)
-- Mathlib.Order.Interval.Finset.Nat
Nat.instUniqueSubtypeMemFinsetIicOfNat : Unique ↥(Finset.Iic 0)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.piEquivL_apply : ∀ (𝕜 : Type u_1) [inst : NormedField 𝕜] (E : Type u_2) {ι : Type u_3} (F : ι → Type u_4) [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : (i : ι) → AddCommGroup (F i)]
  [inst_5 : (i : ι) → Module 𝕜 (F i)] [inst_6 : (i : ι) → TopologicalSpace (F i)]
  [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)]
  (F_1 : (i : ι) → E →L[𝕜] F i), (ContinuousLinearMap.piEquivL 𝕜 E F) F_1 = ContinuousLinearMap.pi F_1
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.hom_inv_id_right_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) {Z : T}
  (h : f.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e.inv) h) =
    h
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.le_tsum_of_forall_lt_exists_sum : ∀ {α : Type u_1} {a : ENNReal} {f : α → ENNReal}, (∀ b < a, ∃ I, b < ∑ i ∈ I, f i) → a ≤ ∑' (i : α), f i
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.power_nat_le_max : ∀ {c : Cardinal.{u}} {n : ℕ}, c ^ ↑n ≤ max c Cardinal.aleph0
-- Mathlib.CategoryTheory.Limits.Fubini
/-- `coconeOfCoconeUncurry Q c` is a colimit cocone when `c` is a colimit cocone.
 -/
CategoryTheory.Limits.coconeOfCoconeUncurryIsColimit : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              {D : CategoryTheory.Limits.DiagramOfCocones F} →
                (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) →
                  {c : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.uncurry.obj F)} →
                    CategoryTheory.Limits.IsColimit c →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfCoconeUncurry Q c)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.subNegMonoid.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : SubNegMonoid G],
  Filter.Germ.subNegMonoid =
    { toAddMonoid := Filter.Germ.instAddMonoid, toNeg := Filter.Germ.instNeg, toSub := Filter.Germ.instSub,
      zsmul := fun z f => z • f, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_rco : ∀ {m n k : ℕ}, Array.map (fun x => x + k) (m...n).toArray = ((m + k)...n + k).toArray
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.multicospanIndex_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) (F : CategoryTheory.Functor Cᵒᵖ A) (j : E.multicospanShape.R),
  (E.multicospanIndex F).fst j = F.map (E.p₁ j.snd).op
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_cons : ∀ {V : Type u} [inst : Quiver V] {a b c d : V} (p : Quiver.Path a b) (q : Quiver.Path b c) (e : c ⟶ d),
  p.comp (q.cons e) = (p.comp q).cons e
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
/-- Assume that `R` has finite quotients and that `S` is a domain and a finite `R`-module. Then
`S` has finite quotients.
 -/
Ring.HasFiniteQuotients.of_module_finite : ∀ (R : Type u_1) [inst : CommRing R] [Ring.HasFiniteQuotients R] (S : Type u_2) [inst_2 : CommRing S] [IsDomain S]
  [inst_4 : Algebra R S] [Module.Finite R S], Ring.HasFiniteQuotients S
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- Given `φ : F ⟶ G`, this is the morphism `mappingCone φ ⟶ K` that is constructed
from a cochain `α : Cochain F K (-1)` and a morphism `β : G ⟶ K` such that
`δ (-1) 0 α = Cochain.ofHom (φ ≫ β)`.  -/
CochainComplex.mappingCone.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {K : CochainComplex C ℤ} →
              (α : CochainComplex.HomComplex.Cochain F K (-1)) →
                (β : G ⟶ K) →
                  CochainComplex.HomComplex.δ (-1) 0 α =
                      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β) →
                    (CochainComplex.mappingCone φ ⟶ K)
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_nat_floor_mul_div_atTop : ∀ {R : Type u_4} [inst : TopologicalSpace R] [inst_1 : Field R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R]
  [OrderTopology R] [inst_5 : FloorRing R] {a : R},
  0 ≤ a → Filter.Tendsto (fun x => ↑⌊a * x⌋₊ / x) Filter.atTop (nhds a)
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.instT3Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T3Space M], T3Space Mᵈᵐᵃ
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.add.inj : ∀ {k : ℤ} {v : Int.Internal.Linear.Var} {p : Int.Internal.Linear.Poly} {k_1 : ℤ} {v_1 : Int.Internal.Linear.Var}
  {p_1 : Int.Internal.Linear.Poly},
  Int.Internal.Linear.Poly.add k v p = Int.Internal.Linear.Poly.add k_1 v_1 p_1 → k = k_1 ∧ v = v_1 ∧ p = p_1
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
OrderAddMonoidHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (toAddMonoidHom toAddMonoidHom_1 : α →+ β)
  (e_toAddMonoidHom : toAddMonoidHom = toAddMonoidHom_1) (monotone' : Monotone (↑toAddMonoidHom).toFun),
  { toAddMonoidHom := toAddMonoidHom, monotone' := monotone' } = { toAddMonoidHom := toAddMonoidHom_1, monotone' := ⋯ }