mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind.eq.sizeOf_spec : sizeOf Mathlib.Tactic.Translate.CastKind.eq✝ = 1
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_hom_leftUnitor : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {X : Rep.{u, u, v} k G},
  Rep.Hom.hom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom = ↑(Representation.TensorProduct.lid k X.ρ)
-- Mathlib.Data.UInt
UInt64.toFin_injective : Function.Injective UInt64.toFin
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the left whiskering `f ◁ η` with `η : g ⟶ h`.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.whiskerLeft : Lean.Expr →
  Option Mathlib.Tactic.BicategoryLike.IsoLift →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₂
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.isDefEqAssigning : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.Connected.Clopen
instCompactSpaceConnectedComponents : ∀ {α : Type u} [inst : TopologicalSpace α] [CompactSpace α], CompactSpace (ConnectedComponents α)
-- Mathlib.Analysis.Real.Pi.Bounds
/-- Create a proof of `a < π` for a fixed rational number `a`, given a witness, which is a
sequence of rational numbers `√2 < r 1 < r 2 < ... < r n < 2` satisfying the property that
`√(2 + r i) ≤ r(i+1)`, where `r 0 = 0` and `√(2 - r n) ≥ a/2^(n+1)`.  -/
Real.«tacticPi_lower_bound[_,,]» : Lean.ParserDescr
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.minpoly_inj : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {c d : ConjRootClass K L},
  c.minpoly = d.minpoly ↔ c = d
-- Mathlib.LinearAlgebra.Eigenspace.Triangularizable
/-- In finite dimensions, over an algebraically closed field, every linear endomorphism has an
eigenvalue.  -/
Module.End.exists_eigenvalue : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [IsAlgClosed K]
  [FiniteDimensional K V] [Nontrivial V] (f : Module.End K V), ∃ c, f.HasEigenvalue c
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentColorOptions : Lean.ToJson Lean.Lsp.DocumentColorOptions
-- Mathlib.Data.Set.Lattice
Set.iUnion_nonempty_self : ∀ {α : Type u_1} (s : Set α), ⋃ (_ : s.Nonempty), s = s
-- Mathlib.Order.Hom.Basic
/-- Notation for an `OrderIso`.  -/
«term_≃o_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- Given a functor `p : 𝒳 ⥤ 𝒮`, an arrow `φ : a ⟶ b` in `𝒳` and an arrow `f : R ⟶ S` in `𝒮`,
`p.IsHomLift f φ` expresses the fact that `φ` lifts `f` through `p`.
This is often drawn as:
```
  a --φ--> b
  -        -
  |        |
  v        v
  R --f--> S
```  -/
CategoryTheory.Functor.IsHomLift : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] →
      [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮] →
        CategoryTheory.Functor 𝒳 𝒮 → {R S : 𝒮} → {a b : 𝒳} → (R ⟶ S) → (a ⟶ b) → Prop
-- Mathlib.Data.Countable.Defs
exists_surjective_nat : ∀ (α : Sort u) [Nonempty α] [Countable α], ∃ f, Function.Surjective f
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A]
  (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) (X : CategoryTheory.Functor Cᵒᵖ A)
  (X_1 : SimplexCategory),
  ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).obj X).obj X_1 =
    ∏ᶜ fun i => X.obj (Opposite.op ((E.obj (Opposite.op X_1)).obj i))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?.match_1.congr_eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1))
  (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β),
  x = Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1 →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
      | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2 =>
        h_3 size k v l size_2 k_2 v_2 l_1 r h r_2) ≍
      h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.of.inj : ∀ {J : Type v} {inst : CategoryTheory.SmallCategory J} {F : CategoryTheory.Functor J CommRingCat} {j : J}
  {x : ↑(F.obj j)} {j_1 : J} {x_1 : ↑(F.obj j_1)},
  CommRingCat.Colimits.Prequotient.of j x = CommRingCat.Colimits.Prequotient.of j_1 x_1 → j = j_1 ∧ x ≍ x_1
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.log_div_log_pos : ∀ {F : Type u_1} [inst : Field F] {v w : AbsoluteValue F ℝ},
  v.IsEquiv w → ∀ {a : F}, a ≠ 0 → w a ≠ 1 → 0 < Real.log (w a) / Real.log (v a)
-- Init.Data.UInt.Bitwise
UInt8.xor_left_inj : ∀ {a b : UInt8} (c : UInt8), a ^^^ c = b ^^^ c ↔ a = b
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.id_hcomp_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H : CategoryTheory.Functor E C} (α : F ⟶ G) (X : E), (CategoryTheory.CategoryStruct.id H ◫ α).app X = α.app (H.obj X)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instMulAction : {G : Type u_1} → {α : Type u_2} → [inst : Group G] → [MulAction G α] → (H : Subgroup G) → MulAction (↥H) α
-- Mathlib.CategoryTheory.Category.Quiv
/-- The identity in the category of quivers equals the identity prefunctor.  -/
CategoryTheory.Quiv.id_eq_id : ∀ (X : CategoryTheory.Quiv), CategoryTheory.CategoryStruct.id X = 𝟭q ↑X
-- Mathlib.Data.W.Basic
/-- The canonical map from `WType β` into any type `γ` given a map `(Σ a : α, β a → γ) → γ`.  -/
WType.elim : {α : Type u_1} → {β : α → Type u_2} → (γ : Type u_3) → ((a : α) × (β a → γ) → γ) → WType β → γ
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- An additive functor is in particular a functor.  -/
CategoryTheory.AdditiveFunctor.forget : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] → CategoryTheory.Functor (C ⥤+ D) (CategoryTheory.Functor C D)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- Version of `Bicategory.precomposing` viewed in the bicategory `Cat`.  -/
CategoryTheory.Bicategory.precomposingCat : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b c : B) → CategoryTheory.Functor (a ⟶ b) (CategoryTheory.Cat.of (b ⟶ c) ⟶ CategoryTheory.Cat.of (a ⟶ c))
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.instIsEquivalenceIncl : FintypeCat.Skeleton.incl.IsEquivalence
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.ofFractionRing : {K : Type u} → [inst : CommRing K] → FractionRing (Polynomial K) → RatFunc K
-- Mathlib.GroupTheory.Divisible
rootableByOfPowLeftSurj.eq_1 : ∀ (A : Type u_1) (α : Type u_2) [inst : Monoid A] [inst_1 : Pow A α] [inst_2 : Zero α]
  (H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n),
  rootableByOfPowLeftSurj A α H =
    { root := fun a n => if x : n = 0 then 1 else ⋯.choose, root_zero := ⋯, root_cancel := ⋯ }
-- Mathlib.Algebra.Order.IsBotOne
zero_notMem_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α] {s : Set α}, 0 ∉ s ↔ ∀ x ∈ s, 0 < x
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.TendstoInDistribution.congr : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {μ : (i : ι) → MeasureTheory.Measure (Ω i)} [inst : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)]
  {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} [inst_1 : MeasureTheory.IsProbabilityMeasure μ']
  {mE : MeasurableSpace E} {X Y : (i : ι) → Ω i → E} {Z : Ω' → E} {l : Filter ι} [inst_2 : TopologicalSpace E]
  [inst_3 : OpensMeasurableSpace E] {T : Ω' → E},
  (∀ (i : ι), X i =ᵐ[μ i] Y i) →
    Z =ᵐ[μ'] T → MeasureTheory.TendstoInDistribution X l Z μ μ' → MeasureTheory.TendstoInDistribution Y l T μ μ'
-- Mathlib.FieldTheory.Normal.Defs
/-- Restrict algebra homomorphism to normal subfield.  -/
AlgHom.restrictNormal : {F : Type u_1} →
  [inst : Field F] →
    {K₁ : Type u_3} →
      {K₂ : Type u_4} →
        [inst_1 : Field K₁] →
          [inst_2 : Field K₂] →
            [inst_3 : Algebra F K₁] →
              [inst_4 : Algebra F K₂] →
                (K₁ →ₐ[F] K₂) →
                  (E : Type u_6) →
                    [inst_5 : Field E] →
                      [inst_6 : Algebra F E] →
                        [inst_7 : Algebra E K₁] →
                          [inst_8 : Algebra E K₂] →
                            [IsScalarTower F E K₁] → [IsScalarTower F E K₂] → [Normal F E] → E →ₐ[F] E
-- Mathlib.CategoryTheory.Shift.Basic
/-- A helper structure to construct the shift functor `(Discrete A) ⥤ (C ⥤ C)`.  -/
CategoryTheory.ShiftMkCore : (C : Type u) → (A : Type u_1) → [CategoryTheory.Category.{v, u} C] → [AddMonoid A] → Type (max (max u u_1) v)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_add_sum_eq_sum_zipWith_of_length_eq : ∀ {M : Type u_4} [inst : AddCommMonoid M] (l l' : List M),
  l.length = l'.length → l.sum + l'.sum = (List.zipWith (fun x1 x2 => x1 + x2) l l').sum
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If three points are not collinear, the first and second are different.  -/
ne₁₂_of_not_collinear : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, ¬Collinear k {p₁, p₂, p₃} → p₁ ≠ p₂
-- Lean.Parser.Tactic
Lean.Parser.Tactic.nestedTactic.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.Transfer
/-- Given `ϕ : H →* A` from `H : Subgroup G` to a commutative group `A`,
the transfer homomorphism is `transfer ϕ : G →* A`.  -/
MonoidHom.transfer : {G : Type u_1} →
  [inst : Group G] → {H : Subgroup G} → {A : Type u_2} → [inst_1 : CommGroup A] → (↥H →* A) → [H.FiniteIndex] → G →* A
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.coeff_iterate_fslope : ∀ {𝕜 : Type u} {E : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} (k n : ℕ),
  (FormalMultilinearSeries.fslope^[k] p).coeff n = p.coeff (n + k)
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.edist_indicatorConstLp_eq_enorm : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E} {t : Set α}
  {ht : MeasurableSet t} {hμt : μ t ≠ ⊤},
  edist (MeasureTheory.indicatorConstLp p hs hμs c) (MeasureTheory.indicatorConstLp p ht hμt c) =
    ‖MeasureTheory.indicatorConstLp p ⋯ ⋯ c‖ₑ
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseRat : ℕ → Std.Internal.Parsec.ByteArray.Parser Std.Tactic.BVDecide.LRAT.IntAction
-- Mathlib.RepresentationTheory.FiniteIndex
/-- Let `S ≤ G` be a subgroup and `(A, ρ)` a `k`-linear `S`-representation. Then given `g : G` and
`a : A`, this is the function `G → A` sending `sg` to `ρ(s)(a)` for all `s : S` and everything else
to 0.  -/
Rep.indToCoindAux : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Group G] →
        {S : Subgroup G} → [DecidableRel ⇑(QuotientGroup.rightRel S)] → (A : Rep.{w, u, v} k ↥S) → G → ↑A →ₗ[k] G → ↑A
-- Mathlib.Order.RelIso.Basic
RelIso.coe_toRelEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s), ⇑f.toRelEmbedding = ⇑f
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_natCast_eq_lift : ∀ {o : Ordinal.{u}} {n : ℕ}, Ordinal.omega ↑n = Ordinal.lift.{v, u} o ↔ Ordinal.omega ↑n = o
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.instAlgebraCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensFunctionFieldOfNonemptyToScheme : (X : AlgebraicGeometry.Scheme) →
  [inst : IrreducibleSpace ↥X] →
    (U : X.Opens) → [Nonempty ↥↑U] → Algebra ↑(X.presheaf.obj (Opposite.op U)) ↑X.functionField
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- A strict vector subspace has measure zero.  -/
MeasureTheory.Measure.addHaar_submodule : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Submodule ℝ E), s ≠ ⊤ → μ ↑s = 0
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- The precylinder object obtained by switching the two inclusions.  -/
HomotopicalAlgebra.Precylinder.symm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : C} → HomotopicalAlgebra.Precylinder A → HomotopicalAlgebra.Precylinder A
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.IsLimit.lift'_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (h : CategoryTheory.Limits.IsLimit s) (f : W ⟶ X) (g : W ⟶ Y),
  ↑(CategoryTheory.Limits.BinaryFan.IsLimit.lift' h f g) = h.lift (CategoryTheory.Limits.BinaryFan.mk f g)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalOpOp_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.opOp C) X Y =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.opOp C).obj X) ((CategoryTheory.opOp C).obj Y))
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.as : Lean.FVarId → Lean.Meta.Match.Pattern → Lean.FVarId → Lean.Meta.Match.Pattern
-- Mathlib.Algebra.Notation.Defs
SDiv.mk : {G : outParam (Type u_1)} → {P : Type u_2} → (P → P → G) → SDiv G P
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.addConst : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Poly
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α}, k ∈ t → t.getKey? k = some k
-- Init.Data.Bool
Bool.not_bne_not : ∀ (x y : Bool), ((!x) != !y) = (x != y)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.prod_single : ∀ {R : Type u_1} {M : Type u_4} {ι : Type u_7} [inst : CommSemiring R] [inst_1 : CommMonoid M] (s : Finset ι)
  (m : ι → M) (r : ι → R),
  ∏ i ∈ s, MonoidAlgebra.single (m i) (r i) = MonoidAlgebra.single (∏ i ∈ s, m i) (∏ i ∈ s, r i)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.le_ndinsert_self : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), s ≤ Multiset.ndinsert a s
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
/-- A variant of `IsSemilinearSet.proj` for backward reasoning.  -/
IsSemilinearSet.proj' : ∀ {M : Type u_1} {ι : Type u_3} {κ : Type u_4} [inst : AddCommMonoid M] {p : (ι → M) → (κ → M) → Prop},
  IsSemilinearSet {x | p (x ∘ Sum.inl) (x ∘ Sum.inr)} → IsSemilinearSet {x | ∃ y, p x y}
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.ofSupport_singleton : ∀ {V : Type u} (G : SimpleGraph V) (v : V), SimpleGraph.Walk.ofSupport [v] ⋯ ⋯ = SimpleGraph.Walk.nil
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.natTransOfLe_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S T : CategoryTheory.Sieve X} (h : S ≤ T),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.natTransOfLe h) T.functorInclusion = S.functorInclusion
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.α_hom_inv : ∀ {C : Type u} {X Y Z : CategoryTheory.FreeMonoidalCategory C},
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((CategoryTheory.FreeMonoidalCategory.Hom.α_hom X Y Z).comp (CategoryTheory.FreeMonoidalCategory.Hom.α_inv X Y Z))
    (CategoryTheory.FreeMonoidalCategory.Hom.id ((X.tensor Y).tensor Z))
-- Init.Data.OfScientific
/-- Converts an integer into the closest-possible 32-bit floating-point number, or positive or negative
infinite floating-point value if the range of `Float32` is exceeded.
 -/
Float32.ofInt : ℤ → Float32
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- If `n < 0` and `|w - c| = |R|`, then `(z - w) ^ n` is not circle integrable on the circle with
center `c` and radius `|R|`, so the integral `∮ z in C(c, R), (z - w) ^ n` is equal to zero.  -/
circleIntegral.integral_sub_zpow_of_undef : ∀ {n : ℤ} {c w : ℂ} {R : ℝ}, n < 0 → w ∈ Metric.sphere c |R| → ∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero (Opposite.op X)
-- Init.Data.Array.Lemmas
Array.foldr_map : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} {f : α₁ → α₂} {g : α₂ → β → β} {xs : Array α₁} {init : β},
  Array.foldr g init (Array.map f xs) = Array.foldr (fun x y => g (f x) y) init xs
-- Mathlib.Data.Fin.Tuple.Basic
/-- `Fin.cons` is the same as appending a one-tuple to the left.  -/
Fin.cons_eq_append : ∀ {n : ℕ} {α : Sort u_1} (x : α) (xs : Fin n → α), Fin.cons x xs = Fin.append (Fin.cons x Fin.elim0) xs ∘ Fin.cast ⋯
-- Mathlib.LinearAlgebra.Alternating.Curry
AlternatingMap.curryLeft_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {n : ℕ}, AlternatingMap.curryLeft 0 = 0
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_eq_mod_256_iff : ∀ (a : UInt8) (b : UInt32), a.toUInt32 = b % 256 ↔ a = b.toUInt8
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborates applications. Removes up to `maxArgs` arguments to form the "head" of the application.
* `delabHead` is a delaborator to use for the head of the expression.
  It is passed whether the result needs to have `@` inserted.
* If `unexpand` is true, then allow unexpanders and field notation.
  This should likely be set to `false` except in the main `delabApp` delaborator.

Propagates `pp.tagAppFns` into the head for `delabHead`.
 -/
Lean.PrettyPrinter.Delaborator.delabAppCore : ℕ → (Bool → Lean.PrettyPrinter.Delaborator.Delab) → Bool → Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C)
  [inst_3 : CategoryTheory.PreGaloisCategory.IsGalois A] (a a_1 : (F.obj A).obj),
  a = a_1 →
    CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a =
      CategoryTheory.PreGaloisCategory.evaluationEquivOfIsGalois F A a_1
-- Mathlib.Algebra.Order.Group.Abs
abs_sub_abs_le_abs_add : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] (a b : G), |a| - |b| ≤ |a + b|
-- Init.Omega.IntList
Lean.Omega.IntList.dot_eq_zero_of_left_eq_zero : ∀ {xs ys : Lean.Omega.IntList}, (∀ x ∈ xs, x = 0) → xs.dot ys = 0
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.equivSubgroupOrbitsSetoidComap.eq_1 : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (H : Subgroup G)
  (ω : Quotient (MulAction.orbitRel G X)),
  MulAction.equivSubgroupOrbitsSetoidComap H ω =
    { toFun := fun q => Quotient.liftOn' q (fun x => ⟦⟨↑x, ⋯⟩⟧) ⋯, invFun := fun q => q.liftOn' (fun x => ⟦⟨↑x, ⋯⟩⟧) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.isLeftCancelMulZero_iff : ∀ {R : Type u_1} [inst : Semiring R], IsLeftCancelMulZero (Polynomial R) ↔ IsLeftCancelMulZero R ∧ IsCancelAdd R
-- Init.Control.ExceptCps
/-- Run an action from the transformed monad in the exception monad.
 -/
ExceptCpsT.lift : {m : Type u_1 → Type u_2} → {α ε : Type u_1} → [Monad m] → m α → ExceptCpsT ε m α
-- Aesop.Search.SearchM
Aesop.SearchM.State.queue : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.SearchM.State Q → Q
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flip_d_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (i i' : I₂) (j : I₁), (K.flip.d i i').f j = (K.X j).d i i'
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_add_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      MeasureTheory.MemLp Z 2 μ →
        ProbabilityTheory.covariance (X + Y) Z μ =
          ProbabilityTheory.covariance X Z μ + ProbabilityTheory.covariance Y Z μ
-- Mathlib.Data.Set.Sups
/-- The point-wise infimum `a ⊓ b` of `a, b : α`.  -/
HasInfs.infs : {α : Type u_4} → [self : HasInfs α] → α → α → α
-- Mathlib.Order.Interval.Set.Infinite
Set.Icc_infinite : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {a b : α}, a < b → (Set.Icc a b).Infinite
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- We can express `qrSign m n` as a power of `-1` when `m` and `n` are odd.  -/
qrSign.neg_one_pow : ∀ {m n : ℕ}, Odd m → Odd n → qrSign m n = (-1) ^ (m / 2 * (n / 2))
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
/-- If scalar multiplication yields zero, either the scalar or the vector was zero.  -/
NoZeroSMulDivisors.eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {R : Type u_4} {M : Type u_5} {inst : Zero R} {inst_1 : Zero M} {inst_2 : SMul R M} [self : NoZeroSMulDivisors R M]
  {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0