mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  {homEquiv : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X)}
  {homEquiv_comp :
    autoParam
      (∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
        homEquiv (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (homEquiv g))
      CategoryTheory.Functor.RepresentableBy.homEquiv_comp._autoParam}
  {homEquiv_1 : {X : C} → (X ⟶ Y) ≃ F.obj (Opposite.op X)}
  {homEquiv_comp_1 :
    autoParam
      (∀ {X X' : C} (f : X ⟶ X') (g : X' ⟶ Y),
        homEquiv_1 (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map f.op)) (homEquiv_1 g))
      CategoryTheory.Functor.RepresentableBy.homEquiv_comp._autoParam},
  { homEquiv := homEquiv, homEquiv_comp := homEquiv_comp } =
      { homEquiv := homEquiv_1, homEquiv_comp := homEquiv_comp_1 } →
    homEquiv = homEquiv_1
-- Mathlib.Data.Fintype.Parity
Fintype.IsSquare.decidablePred : {α : Type u_1} → [inst : Mul α] → [Fintype α] → [DecidableEq α] → DecidablePred IsSquare
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
/-- A morphism property of schemes is said to preserve joint surjectivity, if
for any pair of morphisms `f : X ⟶ S` and `g : Y ⟶ S` where `g` satisfies `P`,
any pair of points `x : X` and `y : Y` with `f x = g y` can be lifted to a point
of `X ×[S] Y`.

In later files, this will be automatic, since this holds for any morphism `g`
(see `AlgebraicGeometry.Scheme.isJointlySurjectivePreserving`). But at
this early stage in the import tree, we only know it for open immersions.  -/
AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → Prop
-- Mathlib.Algebra.Group.Submonoid.Pointwise
coe_add_coe : ∀ {M : Type u_3} {S : Type u_6} [inst : AddMonoid M] [inst_1 : SetLike S M] [AddSubmonoidClass S M] (H : S),
  ↑H + ↑H = ↑H
-- Mathlib.Algebra.Ring.Int.Parity
Odd.neg_one_zpow : ∀ {α : Type u_1} [inst : DivisionMonoid α] [inst_1 : HasDistribNeg α] {n : ℤ}, Odd n → (-1) ^ n = -1
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instFibrationOfIsWeakFactorizationSystemCofibrationsTrivialFibrationsOfIsIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : C} (f : X ⟶ Y)
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)]
  [CategoryTheory.IsIso f], HomotopicalAlgebra.Fibration f
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk.injEq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (toAddHom : M →ₙ+ N) (isLocalizationMap : S.IsLocalizationMap toAddHom.toFun) (toAddHom_1 : M →ₙ+ N)
  (isLocalizationMap_1 : S.IsLocalizationMap toAddHom_1.toFun),
  ({ toAddHom := toAddHom, isLocalizationMap := isLocalizationMap } =
      { toAddHom := toAddHom_1, isLocalizationMap := isLocalizationMap_1 }) =
    (toAddHom = toAddHom_1)
-- Mathlib.Order.Hom.Lattice
InfHom.instInhabited : (α : Type u_2) → [inst : Min α] → Inhabited (InfHom α α)
-- Init.Data.Nat.Lemmas
Nat.le_mul_of_pos_right : ∀ {m : ℕ} (n : ℕ), 0 < m → n ≤ n * m
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  m.WF → ((Std.HashMap.Raw.filter f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), f (m.getKey k h) m[k] = true)
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_eq_empty_iff_of_pos : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ε : ℝ} {s : Set α}, 0 < ε → (Metric.thickening ε s = ∅ ↔ s = ∅)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.funMap_eq_coe_constants : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {c : L.Constants} {x : Fin 0 → M},
  FirstOrder.Language.Structure.funMap c x = ↑c
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.weightMap_one : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  RootPairing.Hom.weightMap 1 = LinearMap.id
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Topology of uniform convergence, declared as an instance on `α →ᵤ β`.  -/
UniformFun.topologicalSpace : (α : Type u_1) → (β : Type u_2) → [UniformSpace β] → TopologicalSpace (UniformFun α β)
-- Init.Data.Bool
Bool.and' : Bool → Bool → Bool
-- Mathlib.Algebra.BigOperators.Group.Finset.Powerset
/-- A sum over `Finset.powersetCard` which only depends on the size of the sets is constant.  -/
Finset.sum_powersetCard : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β),
  ∑ t ∈ Finset.powersetCard n s, f t.card = s.card.choose n • f n
-- Mathlib.LinearAlgebra.Prod
/-- **Vertical line test** for linear maps.

Let `G ≤ H × I` be a submodule of a product of modules. Assume that `G` maps bijectively to the
first factor. Then `G` is the graph of some linear map `f : H →ₗ[R] I`.  -/
Submodule.exists_eq_graph : ∀ {S : Type u_4} {H : Type u_6} {I : Type u_7} [inst : Semiring S] [inst_1 : AddCommMonoid H] [inst_2 : Module S H]
  [inst_3 : AddCommMonoid I] [inst_4 : Module S I] {G : Submodule S (H × I)},
  Function.Bijective (Prod.fst ∘ ⇑G.subtype) → ∃ f, G = f.graph
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.Eqv.add_comm : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (x y : FreeAddMonoid (R × ((i : ι) → s i))),
  PiTensorProduct.Eqv R s (x + y) (y + x)
-- Mathlib.ModelTheory.Syntax
/-- A term on `α` is either a variable indexed by an element of `α` or a function symbol applied to
simpler terms.  -/
FirstOrder.Language.Term : FirstOrder.Language → Type u' → Type (max u u')
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.map.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (f : (a : α) → β a → γ a) (m : Std.DHashMap.Raw α β),
  Std.DHashMap.Raw.map f m = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.map f ⟨m, h⟩) else ∅
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.exists_range_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {f : MeasureTheory.SimpleFunc α β} {p : β → Prop},
  (∃ y ∈ f.range, p y) ↔ ∃ x, p (f x)
-- Mathlib.Order.Interval.Set.UnorderedInterval
/-- `[[a, b]]` denotes the set of elements lying between `a` and `b`, inclusive.  -/
Interval.«term[[_,_]]» : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.Λ'.ret.inj : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {a a_1 : Turing.TM2.Stmt Γ Λ σ},
  Turing.TM2to1.Λ'.ret a = Turing.TM2to1.Λ'.ret a_1 → a = a_1
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instZero : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Zero (AdicCompletion I M)
-- Mathlib.Algebra.Order.Interval.Basic
instAddNonemptyInterval : {α : Type u_2} → [inst : Preorder α] → [inst_1 : Add α] → [AddLeftMono α] → [AddRightMono α] → Add (NonemptyInterval α)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.pow.sizeOf_spec : ∀ (a : Lean.Grind.CommRing.Expr) (k : ℕ), sizeOf (a.pow k) = 1 + sizeOf a + sizeOf k
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
/-- The composition of two isometric equivalences between bilinear forms.  -/
LinearMap.BilinForm.IsometryEquiv.trans : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {M₃ : Type u_5} →
        [inst : CommSemiring R] →
          [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₃] →
                      {B₁ : LinearMap.BilinForm R M₁} →
                        {B₂ : LinearMap.BilinForm R M₂} →
                          {B₃ : LinearMap.BilinForm R M₃} →
                            B₁.IsometryEquiv B₂ → B₂.IsometryEquiv B₃ → B₁.IsometryEquiv B₃
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- A matrix is doubly stochastic if and only if it is both row and
column stochastic.  -/
doublyStochastic_eq_rowStochastic_inf_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R],
  doublyStochastic R n = Matrix.rowStochastic R n ⊓ Matrix.colStochastic R n
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- `N <r M` means that `N` is a `IsStrictRestriction` of `M`.  -/
Matroid.«term_<r_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.NumberField.Norm
RingOfIntegers.coe_algebraMap_norm : ∀ {L : Type u_1} (K : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (x : NumberField.RingOfIntegers L),
  ↑((algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) ((RingOfIntegers.norm K) x)) =
    (algebraMap K L) ((Algebra.norm K) ↑x)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, (m₁ ∩ m₂).getKeyD k fallback = if k ∈ m₂ then m₁.getKeyD k fallback else fallback
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.addUnit_spec : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} (h : IsAddUnit a), ↑h.addUnit = a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ (k : α), m₁.Equiv m₂ → (m₁.erase k).Equiv (m₂.erase k)
-- Init.Data.Range.Basic
Std.Legacy.Range.mk : ℕ → ℕ → (step : ℕ) → 0 < step → Std.Legacy.Range
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- A linear map `T` is zero, if and only if the identity `⟪T x, x⟫_ℂ = 0` holds for all `x`.
 -/
inner_map_self_eq_zero : ∀ {V : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℂ V] (T : V →ₗ[ℂ] V),
  (∀ (x : V), inner ℂ (T x) x = 0) ↔ T = 0
-- Batteries.Lean.Meta.UnusedNames
/-- Result type of `Lean.Name.matchUpToIndexSuffix`. See there for details.
 -/
Lean.Name.MatchUpToIndexSuffix : Type
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pos.revSkip?_char_eq_revSkip?_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos}, pos.revSkip? c = pos.revSkip? fun x => x == c
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → k ∉ t₁ ∩ t₂
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_le_iff : ∀ {M : Type u_2} [inst : AddZeroClass M] {S₁ : AddSubmonoid M} {S₂ : AddSubmonoid Mᵃᵒᵖ}, S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
-- Mathlib.Algebra.Algebra.Hom
IsScalarTower.toAlgHom_apply : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [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] (y : S),
  (IsScalarTower.toAlgHom R S A) y = (algebraMap S A) y
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.instForInProdOfMonad : {m : Type w → Type w'} →
  {α : Type u_1} →
    {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → [Monad m] → ForIn m (Lean.PersistentHashMap α β) (α × β)
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.Precylinder.unop_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Cᵒᵖ} (P : HomotopicalAlgebra.Precylinder A),
  P.unop.ι = P.π.unop
-- Lean.Meta.Closure
Lean.Meta.Closure.collectExprAux : Lean.Expr → Lean.Meta.Closure.ClosureM Lean.Expr
-- Init.Data.Array.Monadic
Array.forIn_pure_yield_eq_foldl : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  (f : α → β → β) (init : β),
  (forIn xs init fun a b => pure (ForInStep.yield (f a b))) = pure (Array.foldl (fun b a => f a b) init xs)
-- Init.Data.Range.Polymorphic.UInt
UInt16.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite UInt16
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.nat_le_card : ∀ {o : Ordinal.{u_1}} {n : ℕ}, ↑n ≤ o.card ↔ ↑n ≤ o
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
/-- `F.OplaxLinear C` equips `F : D ⥤ D'` with a family of morphisms
`δₗ F : ∀ (c : C) (d : D), c ⊙ₗ F.obj d ⟶ F.obj (c ⊙ₗ d)`
that is natural in each variable and coherent with respect to left actions
of `C` on `D` and `D'`.  -/
CategoryTheory.Functor.OplaxRightLinear : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        CategoryTheory.Functor D D' →
          (C : Type u_3) →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [CategoryTheory.MonoidalCategory.MonoidalRightAction C D] →
                  [CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] → Type (max (max u_1 u_3) v_2)
-- Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
/-- Let `K` be the field of fraction of an integrally closed domain `R` and let `L` be an extension
of `K`, generated by an integral power basis `B` such that the minimal polynomial of `B.gen` is
Eisenstein at `p`. Given `z : L` integral over `R`, if `p • z ∈ R[B.gen]`, then
`z ∈ R[B.gen]`.  -/
mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt : ∀ {R : Type u} {K : Type v} {L : Type z} {p : R} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : Algebra R L] [inst_5 : Algebra R K] [IsScalarTower R K L] [IsDomain R]
  [IsFractionRing R K] [IsIntegrallyClosed R] {B : PowerBasis K L},
  Prime p →
    IsIntegral R B.gen →
      ∀ {z : L}, IsIntegral R z → p • z ∈ R[B.gen] → (minpoly R B.gen).IsEisensteinAt (R ∙ p) → z ∈ R[B.gen]
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.coeFn_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p : ENNReal} {μ : MeasureTheory.Measure α} {G : Type u_7}
  [inst_1 : NormedAddCommGroup G] [inst_2 : PartialOrder G] (f g : ↥(MeasureTheory.Lp.simpleFunc G p μ)),
  ↑↑↑f ≤ᵐ[μ] ↑↑↑g ↔ f ≤ g
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.IterM.run_toList_mk' : ∀ {α β : Type u} [inst : Std.Iterator α Id β] (a : α), { internalState := a }.toList.run = { internalState := a }.toList
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_neg : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (φ : M₁ ⟶ M₂),
  TopModuleCat.Hom.hom (-φ) = -TopModuleCat.Hom.hom φ
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_zero_right : ∀ {α : Type u_1} (n : ℕ), Multiset.powersetCard (n + 1) 0 = 0
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The vector span of a singleton is finite-dimensional.  -/
finiteDimensional_vectorSpan_singleton : ∀ (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), FiniteDimensional k ↥(vectorSpan k {p})
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Summable.toNNReal : ∀ {α : Type u_1} {f : α → ℝ}, Summable f → Summable fun n => (f n).toNNReal
-- Lean.Meta.SizeOf
/-- Return `some x` if `fvar` has type of the form `... -> motive ... fvar` where `motive` in `motiveFVars`.
That is, `x` "produces" one of the recursor motives.
 -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.isInductiveHypothesis? : Array Lean.Expr → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f], CategoryTheory.Mono f
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.compCreatesColimit : {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} →
                  {B : Type u₄} →
                    [inst_4 : CategoryTheory.Category.{v₄, u₄} B] →
                      {H : CategoryTheory.Functor E B} →
                        [CategoryTheory.CreatesColimit G H] → CategoryTheory.CreatesColimit (F.comp G) H
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp_assoc_right_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d}
  (h_1 : F.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h))
      (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (F.map h))
        (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
          (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom) h_1)))
-- Mathlib.Order.KrullDimension
Order.krullDim_le_of_krullDim_preimage_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : PartialOrder β] {m : ℕ} (f : α →o β),
  (∀ (x : β), Order.krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m) → Order.krullDim α ≤ (↑m + 1) * Order.krullDim β + ↑m
-- Mathlib.GroupTheory.Perm.Centralizer
/-- A choice of elements in each cycle  -/
Equiv.Perm.Basis.toFun : {α : Type u_1} →
  [inst : DecidableEq α] → [inst_1 : Fintype α] → {g : Equiv.Perm α} → g.Basis → ↥g.cycleFactorsFinset → α
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.descUniq_hom_app : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D)
  (q : CategoryTheory.Functor ((i : I) × C i) D) (h : (i : I) → (CategoryTheory.Sigma.incl i).comp q ≅ F i) (i : I)
  (X : C i), (CategoryTheory.Sigma.descUniq F q h).hom.app ⟨i, X⟩ = (h i).hom.app X
-- Mathlib.RingTheory.Invariant.Basic
MulSemiringAction.charpoly.eq_1 : ∀ {B : Type u_2} (G : Type u_3) [inst : CommRing B] [inst_1 : Group G] [inst_2 : MulSemiringAction G B]
  [inst_3 : Fintype G] (b : B), MulSemiringAction.charpoly G b = ∏ g, (Polynomial.X - Polynomial.C (g • b))
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- Given a monotone family `U` of complete submodules of `E` with dense span supremum,
and a fixed `x : E`, the orthogonal projection of `x` on `U i` tends to `x` along `at_top`.  -/
Submodule.starProjection_tendsto_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : Preorder ι] (U : ι → Submodule 𝕜 E) [inst_4 : ∀ (t : ι), (U t).HasOrthogonalProjection],
  Monotone U →
    ∀ (x : E),
      ⊤ ≤ (⨆ t, U t).topologicalClosure → Filter.Tendsto (fun t => (U t).starProjection x) Filter.atTop (nhds x)
-- Mathlib.Topology.Constructions
Topology.IsInducing.subtypeVal : ∀ {Y : Type v} [inst : TopologicalSpace Y] {t : Set Y}, Topology.IsInducing Subtype.val
-- Mathlib.GroupTheory.OrderOfElement
/-- If the order of `x` is finite, then `x` is a unit with inverse `x ^ (orderOf x - 1)`.  -/
IsOfFinOrder.unit : {M : Type u_6} → [inst : Monoid M] → {x : M} → IsOfFinOrder x → Mˣ
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.splitOn.loop.eq_def : ∀ (s : Substring.Raw) (sep : String) (b i j : String.Pos.Raw) (r : List Substring.Raw),
  Substring.Raw.splitOn.loop✝ s sep b i j r =
    if h : i.byteIdx < s.bsize then
      have this := ⋯;
      if (s.get i == String.Pos.Raw.get sep j) = true then
        have i := s.next i;
        have j := String.Pos.Raw.next sep j;
        if String.Pos.Raw.atEnd sep j = true then
          Substring.Raw.splitOn.loop✝ s sep i i 0 (s.extract b (i.unoffsetBy j) :: r)
        else Substring.Raw.splitOn.loop✝ s sep b i j r
      else Substring.Raw.splitOn.loop✝ s sep b (s.next i) 0 r
    else
      have r :=
        if String.Pos.Raw.atEnd sep j = true then "".toRawSubstring :: s.extract b (i.unoffsetBy j) :: r
        else s.extract b i :: r;
      r.reverse
-- Mathlib.Logic.Function.Basic
Function.invFun.eq_1 : ∀ {α : Sort u} {β : Sort u_3} [inst : Nonempty α] (f : α → β) (y : β),
  Function.invFun f y = if h : ∃ x, f x = y then h.choose else Classical.arbitrary α
-- Mathlib.Algebra.Group.Defs
AddSemigroup.ext : ∀ {G : Type u} {x y : AddSemigroup G}, Add.add = Add.add → x = y
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Internal.Raw₀.diff.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.diff m₂ =
    if (↑m₁).size ≤ (↑m₂).size then Std.DHashMap.Internal.Raw₀.filter (fun k x => !m₂.contains k) m₁
    else ↑(m₁.eraseManyEntries ↑m₂)
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.exists_finite_support : ∀ {α : Type u} (x : FreeCommRing α), ∃ s, s.Finite ∧ x.IsSupported s
-- Init.Data.SInt.IntToBitVec
ISize.eq_iff_toBitVec32_eq : ∀ {a b : ISize} (h : System.Platform.numBits = 32), a = b ↔ a.toBitVec32 h = b.toBitVec32 h
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.isEof : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] → [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι Bool
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.mk_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β) (h : ∀ {a b : α}, (↑f).toFun a ≤ (↑f).toFun b ↔ a ≤ b), { toMulEquiv := ↑f, map_le_map_iff' := h } = f
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → Bool} {k : α},
  (Std.ExtDTreeMap.filter (fun k x => f k) t).getKey! k = (Option.filter f (t.getKey? k)).get!
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.stieltjesOfMeasurableRat.congr_simp : ∀ {α : Type u_1} [inst : MeasurableSpace α] (f f_1 : α → ℚ → ℝ) (e_f : f = f_1) (hf : Measurable f) (a a_1 : α),
  a = a_1 → ProbabilityTheory.stieltjesOfMeasurableRat f hf a = ProbabilityTheory.stieltjesOfMeasurableRat f_1 ⋯ a_1
-- Mathlib.Data.EReal.Basic
EReal.lt_iff_exists_rat_btwn : ∀ {a b : EReal}, a < b ↔ ∃ x, a < ↑↑x ∧ ↑↑x < b
-- Batteries.Tactic.PrintPrefix
/-- `reverseName name` reverses the components of a name.
 -/
_private.Batteries.Tactic.PrintPrefix.0.Batteries.Tactic.reverseName : Lean.Name → optParam Lean.Name Lean.Name.anonymous → Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_sub_two_pi : ∀ (x : ℂ), Complex.cos (x - 2 * ↑Real.pi) = Complex.cos x