mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.shiftFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (t : CategoryTheory.TwistShiftData C A) {X Y : t.Category} (f : X ⟶ Y) (m : A),
  (CategoryTheory.shiftFunctor t.Category m).map f =
    CategoryTheory.CategoryStruct.comp ((t.shiftIso m).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m).map f) ((t.shiftIso m).inv.app Y))
-- Mathlib.RingTheory.Unramified.LocalRing
Localization.exists_awayMap_injective_of_localRingHom_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [inst_3 : p.IsPrime] {q : Ideal S} [inst_4 : q.IsPrime],
  (RingHom.ker (algebraMap R S)).FG →
    ∀ [inst_5 : q.LiesOver p],
      Function.Injective ⇑(Localization.localRingHom p q (algebraMap R S) ⋯) →
        ∃ r ∉ p, ∀ (r' : R), r ∣ r' → Function.Injective ⇑(Localization.awayMap (algebraMap R S) r')
-- Lean.SubExpr
Lean.SubExpr.bindingBody! : Lean.SubExpr → Lean.SubExpr
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_eq_of_subset_of_ae_sdiff_eq_zero_aux : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  s ⊆ t →
    (∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0) →
      MeasureTheory.StronglyMeasurable f →
        MeasureTheory.IntegrableOn f t μ → ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.associator_inv_apply_2 : ∀ {X Y Z : Type u}
  {x :
    (fun X => X)
      (CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) x).2 = x.2.2
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.instInhabitedPostponeBehavior.default : Lean.Elab.Term.PostponeBehavior
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], (↑m).WF → ∀ {a : α}, m.getKey! a = (m.getKey? a).get!
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvectorUnitary_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian) (i j : n), ↑hA.eigenvectorUnitary i j = (hA.eigenvectorBasis j).ofLp i
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.instMonadCacheExprStructEqExprM : Lean.MonadCache Lean.ExprStructEq Lean.Expr Lean.MetavarContext.LevelMVarToParam.M
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.notMem_one : ∀ {α : Type u_1} {m : α}, m ∉ 1
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.IsValuedIn.exists_value : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} {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} {S : Type u_6}
  {inst_5 : CommRing S} {inst_6 : Algebra S R} [self : P.IsValuedIn S] (i j : ι),
  ∃ s, (algebraMap S R) s = P.pairing i j
-- Mathlib.Algebra.BigOperators.Group.Finset.Indicator
Finset.sum_indicator_eq_sum_filter : ∀ {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [inst : AddCommMonoid β] (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ)
  (g : ι → κ) [inst_1 : DecidablePred fun i => g i ∈ t i],
  ∑ i ∈ s, (t i).indicator (f i) (g i) = ∑ i ∈ s with g i ∈ t i, f i (g i)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_insertEntryIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = true →
      ∀ {fallback : α}, Std.Internal.List.minKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback = k
-- Mathlib.Algebra.CharP.Algebra
/-- If a ring homomorphism `R →+* A` is injective and `R` has characteristic zero
then so does `A`.  -/
charZero_of_injective_ringHom : ∀ {R : Type u_1} {A : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring A] {f : R →+* A},
  Function.Injective ⇑f → ∀ [CharZero R], CharZero A
-- Mathlib.Analysis.InnerProductSpace.Subspace
/-- The inner product on submodules is the same as on the ambient space.  -/
Submodule.coe_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (W : Submodule 𝕜 E) (x y : ↥W), inner 𝕜 x y = inner 𝕜 ↑x ↑y
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When `S₁.f` and `S₂.f` are zero and we have chosen limit kernel forks `c₁` and `c₂`
for `S₁.g` and `S₂.g` respectively, the action on homology of a morphism `φ : S₁ ⟶ S₂` of
short complexes is given by the unique morphism `f : c₁.pt ⟶ c₂.pt` such that
`c₁.ι ≫ φ.τ₂ = f ≫ c₂.ι`.  -/
CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hf₁ : S₁.f = 0) →
            (c₁ : CategoryTheory.Limits.KernelFork S₁.g) →
              (hc₁ : CategoryTheory.Limits.IsLimit c₁) →
                (hf₂ : S₂.f = 0) →
                  (c₂ : CategoryTheory.Limits.KernelFork S₂.g) →
                    (hc₂ : CategoryTheory.Limits.IsLimit c₂) →
                      (f : c₁.pt ⟶ c₂.pt) →
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
                            CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂) →
                          CategoryTheory.ShortComplex.HomologyMapData φ
                            (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁)
                            (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂)
-- Mathlib.Control.ULiftable
/-- Not an instance as it is incompatible with `outParam`. In practice it seems not to be needed
anyway.  -/
ULiftable.symm : (f : Type u₀ → Type u₁) → (g : Type v₀ → Type v₁) → [ULiftable f g] → ULiftable g f
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.right_unitor_inv_apply : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X : (i : I) → C i} {i : I},
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv i =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X i)).inv
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Given a subgraph of `G`, restrict it to being a subgraph of another subgraph `G'` by
taking the portion of `G` that intersects `G'`.  -/
SimpleGraph.Subgraph.restrict : {V : Type u} → {G : SimpleGraph V} → {G' : G.Subgraph} → G.Subgraph → G'.coe.Subgraph
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.instSMulOfAlgebra : {R : Type u_3} →
  {A : Type u_4} →
    {M : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : CommSemiring A] → [Algebra R A] → [inst : Module A M] → SMul R (TensorAlgebra A M)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sigma_sum : ∀ {ι : Type u_4} {M : Type u_5} {N : Type u_6} {αs : ι → Type u_12} [inst : Zero M] (l : (i : ι) × αs i →₀ M)
  [inst_1 : AddCommMonoid N] (f : (i : ι) × αs i → M → N),
  l.sum f = ∑ i ∈ l.splitSupport, (l.split i).sum fun a b => f ⟨i, a⟩ b
-- Mathlib.FieldTheory.LinearDisjoint
/-- If for any field extension `K` of `F` that `A` and `B` embed into, their images are
linearly disjoint, then `A ⊗[F] B` is a field. (In the proof we choose `K` to be the quotient
of `A ⊗[F] B` by a maximal ideal.)  -/
IntermediateField.LinearDisjoint.isField_of_forall : ∀ (F : Type u) [inst : Field F] (A : Type v) [inst_1 : Field A] (B : Type w) [inst_2 : Field B] [inst_3 : Algebra F A]
  [inst_4 : Algebra F B],
  (∀ (K : Type (max v w)) [inst_5 : Field K] [inst_6 : Algebra F K] (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
      fa.fieldRange.LinearDisjoint ↥fb.fieldRange) →
    IsField (TensorProduct F A B)
-- Mathlib.Data.ENNReal.Inv
ENNReal.le_of_forall_pos_nnreal_lt : ∀ {x y : ENNReal}, (∀ (r : NNReal), 0 < r → ↑r < x → ↑r ≤ y) → x ≤ y
-- Batteries.Lean.EStateM
EStateM.run'_set : ∀ {σ ε : Type u_1} (v s : σ), (set v).run' s = some PUnit.unit
-- Mathlib.Order.DirSupClosed
PartialOrder.dirSupClosedOn_singleton : ∀ {α : Type u_1} {D : Set (Set α)} [inst : PartialOrder α] (a : α), DirSupClosedOn D {a}
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.neg_snd : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} (x : WithCStarModule A (E × F)) [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F], (-x).2 = -x.2
-- Mathlib.Topology.Homeomorph.Defs
Equiv.coe_toHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s), ⇑(e.toHomeomorph he) = ⇑e
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- `G.CliqueFree n` means that `G` has no `n`-cliques.  -/
SimpleGraph.CliqueFree : {α : Type u_1} → SimpleGraph α → ℕ → Prop
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.inner_def : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (x y : A),
  inner A x y = y * star x
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_five_gt_d9 : 1.6094379123 < Real.log 5
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsStronglyProgressive.finsetProd : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : CommMonoid β]
  [ContinuousMul β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) →
    MeasureTheory.IsStronglyProgressive f fun i a => ∏ c ∈ s, U c i a
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ'_four : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ' 4 = W.preΨ₄
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.not_tendsto_const_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [NoTopOrder α] (x : α) (l : Filter β) [l.NeBot],
  ¬Filter.Tendsto (fun x_1 => x) l Filter.atTop
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  Option.all (fun x_2 => x_2 == k) (m.get? k) = true
-- Mathlib.RingTheory.AdicCompletion.Basic
Submodule.factorPow.congr_simp : ∀ {R : Type u_1} [inst : Ring R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m n : ℕ}
  (le : m ≤ n), Submodule.factorPow I M le = Submodule.factorPow I M le
-- Mathlib.Data.List.Chain
/-- The type of `r`-decreasing chains  -/
List.chains : {α : Type u_1} → (α → α → Prop) → Type (max 0 u_1)
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- If, for some `x : F`, `‖φ x ·‖` is bounded below by `M`, then the value at `x` of any monic
polynomial over `ℝ` of degree `2 * n` has norm bounded below by `M ^ n`. This follows by
induction from the fact that a real monic polynomial of even degree is a product of monic
polynomials of degree `2`.  -/
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.Real.le_aeval_of_isMonicOfDegree : ∀ {F : Type u_1} [inst : NormedRing F] [inst_1 : NormedAlgebra ℝ F] [NormOneClass F] [NormMulClass F] {x : F} {M : ℝ},
  0 ≤ M →
    (∀ (z : ℝ × ℝ), M ≤ ‖NormedAlgebra.Real.φ✝ x z‖) →
      ∀ {p : Polynomial ℝ} {n : ℕ}, p.IsMonicOfDegree (2 * n) → M ^ n ≤ ‖(Polynomial.aeval x) p‖
-- Lean.Elab.Syntax
Lean.Elab.Term.elabParserName : Lean.Ident → Lean.Elab.TermElabM Lean.Parser.ParserResolution
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] {Z : HomotopyCategory D (ComplexShape.up ℕ)}
      (h :
        (HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) ⟶
          Z),
      CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f)
          (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).hom h) =
        CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).hom
          (CategoryTheory.CategoryStruct.comp
            ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
              ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ))
            h)
-- Mathlib.Data.WSeq.Defs
/-- Get the first `n` elements of a weak sequence  -/
Stream'.WSeq.take : {α : Type u} → Stream'.WSeq α → ℕ → Stream'.WSeq α
-- Mathlib.GroupTheory.ArchimedeanDensely
Units.mulArchimedean_iff : ∀ {G₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero G₀], MulArchimedean G₀ˣ ↔ MulArchimedean G₀
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.mulConst_inv_right : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G), A.mulConst B⁻¹ = A.divConst B
-- Mathlib.RingTheory.Length
Module.length_of_free : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M],
  Module.length R M = Cardinal.toENat (Module.rank R M) * Module.length R R
-- Mathlib.Combinatorics.Quiver.Subquiver
/-- an arrow  -/
Quiver.Total.hom : {V : Type u} → [inst : Quiver V] → (self : Quiver.Total V) → self.left ⟶ self.right
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.symm_homotopyHomInvId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂), e.symm.homotopyHomInvId = e.homotopyInvHomId
-- Mathlib.Data.Rat.Defs
Rat.den_neg_eq_den : ∀ (q : ℚ), (-q).den = q.den
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
one_lt_div' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b : α}, 1 < a / b ↔ b < a
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonMeasure.eq_1 : ∀ (r : NNReal),
  ProbabilityTheory.poissonMeasure r =
    MeasureTheory.Measure.sum fun n =>
      ENNReal.ofReal (Real.exp (-↑r) * ↑r ^ n / ↑n.factorial) • MeasureTheory.Measure.dirac n
-- Mathlib.Topology.Separation.SeparatedNhds
Set.hasSeparatingCover_empty_left : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), HasSeparatingCover ∅ s
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.get!_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, m₁.Equiv m₂ → m₁.get! k = m₂.get! k
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- Any graph containing an `IsFiveWheelLike r k` structure is not `(r + 1)`-colorable.
 -/
SimpleGraph.IsFiveWheelLike.not_colorable_succ : ∀ {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [inst : DecidableEq α] {v w₁ w₂ : α} {t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → ¬G.Colorable (r + 1)
-- Mathlib.Topology.Closure
subset_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s ⊆ closure s
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
/-- Definition of the derivative of a bilinear map `f`, given at a point `p` by
`q ↦ f(p.1, q.2) + f(q.1, p.2)` as in the standard formula for the derivative of a product.
We define this function here as a linear map `E × F →ₗ[𝕜] G`, then `IsBoundedBilinearMap.deriv`
strengthens it to a continuous linear map `E × F →L[𝕜] G`.
 -/
IsBoundedBilinearMap.linearDeriv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : SeminormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {G : Type u_4} →
                  [inst_5 : SeminormedAddCommGroup G] →
                    [inst_6 : NormedSpace 𝕜 G] → {f : E × F → G} → IsBoundedBilinearMap 𝕜 f → E × F → E × F →ₗ[𝕜] G
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES_distinguished : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  DerivedCategory.triangleOfSES hS ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F : C ⥤ D` is final, and `t : Cocone G` for some `G : D ⥤ E`,
`t.whisker F` is a colimit cocone exactly when `t` is.
 -/
CategoryTheory.Functor.Final.isColimitWhiskerEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  (t : CategoryTheory.Limits.Cocone G) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cocone.whisker F t) ≃
                      CategoryTheory.Limits.IsColimit t
-- Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.TerminationMeasure.mk.inj : ∀ {ref : Lean.Syntax} {structural : Bool} {fn : Lean.Expr} {ref_1 : Lean.Syntax} {structural_1 : Bool}
  {fn_1 : Lean.Expr},
  { ref := ref, structural := structural, fn := fn } = { ref := ref_1, structural := structural_1, fn := fn_1 } →
    ref = ref_1 ∧ structural = structural_1 ∧ fn = fn_1
-- Mathlib.Algebra.Group.Defs
IsLeftRegular.mul_eq_one_symm : ∀ {M : Type u_2} [inst : Monoid M] {a b : M}, IsLeftRegular a → a * b = 1 → b * a = 1
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.norm_rTensor_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] F),
  ‖ContinuousLinearMap.rTensor G f‖ ≤ ‖f‖
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball_inter : ∀ {β : Type ub} (x : β) (V W : Set (β × β)), UniformSpace.ball x (V ∩ W) = UniformSpace.ball x V ∩ UniformSpace.ball x W
-- Mathlib.Algebra.QuadraticDiscriminant
discrim_eq_zero_of_existsUnique : ∀ {K : Type u_1} [inst : Field K] [NeZero 2] {a b c : K},
  a ≠ 0 → (∃! x, a * (x * x) + b * x + c = 0) → discrim a b c = 0
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.bicomp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : TopologicalSpace α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : α → β} {a : α} [inst_3 : Preorder δ] {op : β → γ → δ},
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) op op →
    IsLocalMax f a → ∀ {g : α → γ}, IsLocalMax g a → IsLocalMax (fun x => op (f x) (g x)) a
-- Mathlib.Tactic.FunProp.Theorems
/-- Environment extension storing all lambda theorems.  -/
Mathlib.Meta.FunProp.lambdaTheoremsExt : Mathlib.Meta.FunProp.LambdaTheoremsExt
-- Std.Data.HashMap.Basic
/-- The number of mappings present in the hash map  -/
Std.HashMap.size : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → ℕ
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- For any `S`-module Y, there is a natural `R`-linear map from `S ⨂ Y` to `Y` by
`s ⊗ y ↦ s • y`  -/
ModuleCat.ExtendRestrictScalarsAdj.Counit.map : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) → {Y : ModuleCat S} → ((ModuleCat.restrictScalars f).comp (ModuleCat.extendScalars f)).obj Y ⟶ Y
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.card_eq_sum_card_image : ∀ {ι : Type u_1} {M : Type u_4} [inst : DecidableEq M] (f : ι → M) (s : Finset ι),
  s.card = ∑ b ∈ Finset.image f s, {a ∈ s | f a = b}.card
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
SimpleGraph.ComponentCompl.hom_refl : ∀ {V : Type u} {G : SimpleGraph V} {L : Set V} (C : G.ComponentCompl L), SimpleGraph.ComponentCompl.hom ⋯ C = C
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.preimage_image : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β) (s : Set α),
  ⇑h ⁻¹' ⇑h '' s = s
-- Mathlib.RingTheory.DedekindDomain.Factorization
IsDedekindDomain.HeightOneSpectrum.multiplicity_le_of_ideal_ge : ∀ {R : Type u_3} [inst : CommRing R] [IsDedekindDomain R] (p : IsDedekindDomain.HeightOneSpectrum R) {I J : Ideal R},
  J ≤ I → J ≠ ⊥ → multiplicity p.asIdeal I ≤ multiplicity p.asIdeal J
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_hom_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ≅ Y) (Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.inv Z)
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)
-- Lean.Elab.Term.TermElabM
/-- Use typeclass resolution to synthesize value for metavariable.
If `extraErrorMsg?` is `some msg`, `msg` contains additional information to include in error messages
regarding type class synthesis failure.
 -/
Lean.Elab.Term.SyntheticMVarKind.typeClass : Option Lean.MessageData → Lean.Elab.Term.SyntheticMVarKind
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.DeclMod.none.sizeOf_spec : sizeOf Lean.Meta.LibrarySearch.DeclMod.none = 1
-- Std.Async.Timer
/-- Set up a `Sleep` that waits for `duration` milliseconds.
This function only initializes but does not yet start the timer.
 -/
Std.Async.Sleep.mk : Std.Time.Millisecond.Offset → Std.Async.Async Std.Async.Sleep
-- Aesop.Tree.TreeM
Aesop.Tree : Type
-- Init.Data.String.Substring
Substring.beq : Substring.Raw → Substring.Raw → Bool
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.supported_eq_map : ∀ (R : Type u_1) (S : Type u_2) {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M),
  MonoidAlgebra.supported R S s = Submodule.map (↑(MonoidAlgebra.coeffLinearEquiv R).symm) (Finsupp.supported S R s)
-- Init.Data.SInt.Lemmas
Int64.zero_div : ∀ {a : Int64}, 0 / a = 0
-- Std.Http.Data.URI.Encoding
_private.Std.Http.Data.URI.Encoding.0.Std.Http.URI.isValidPercentEncoding.loop : ByteArray → ℕ → Bool
-- Mathlib.Algebra.Order.Ring.GeomSum
Nat.pred_mul_geom_sum_le : ∀ (a b n : ℕ), (b - 1) * ∑ i ∈ Finset.range n.succ, a / b ^ i ≤ a * b - a / b ^ n
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic'.congr_simp : ∀ (n n_1 : ℕ),
  n = n_1 →
    ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R],
      Polynomial.cyclotomic' n R = Polynomial.cyclotomic' n_1 R
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.of.inj : ∀ {B : Type u} {inst : Quiver B} {a b : B} {f f_1 : a ⟶ b},
  CategoryTheory.FreeBicategory.Hom.of f = CategoryTheory.FreeBicategory.Hom.of f_1 → f = f_1