mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mapFourδ₄Toδ₃'_comp._auto_3),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
      (X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₄ i₅ hi₀₁ hi₁₂ ⋯ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) =
    X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.instInhabitedRwKey : Inhabited Mathlib.Tactic.ClickSuggestions.RwKey
-- Mathlib.Order.Hom.Basic
OrderIso.apply_eq_iff_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x y : α}, e x = e y ↔ x = y
-- Init.Data.List.Lemmas
List.foldr_flatten : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {L : List (List α)},
  List.foldr f b L.flatten = List.foldr (fun l b => List.foldr f b l) b L
-- Lean.Expr
Lean.SExprMap : Type → Type
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.normal_centralizer : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [H.Normal], (Subgroup.centralizer ↑H).Normal
-- Mathlib.Control.Monad.Cont
/-- reduce the equivalence between two continuation passing monads to the equivalence between
their underlying monad  -/
ContT.equiv : {m₁ : Type u₀ → Type v₀} →
  {m₂ : Type u₁ → Type v₁} →
    {α₁ r₁ : Type u₀} → {α₂ r₂ : Type u₁} → m₁ r₁ ≃ m₂ r₂ → α₁ ≃ α₂ → ContT r₁ m₁ α₁ ≃ ContT r₂ m₂ α₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a k : α} {v : β},
  Std.ExtDTreeMap.Const.get? (t.insert k v) a = if cmp k a = Ordering.eq then some v else Std.ExtDTreeMap.Const.get? t a
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- As it is stated in `Splitting.hom_ext`, a morphism `f : X ⟶ Y` from a split
simplicial object to any simplicial object is determined by its restrictions
`s.φ f n : s.N n ⟶ Y _⦋n⦌` to the distinguished summands in each degree `n`.  -/
CategoryTheory.SimplicialObject.Splitting.φ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) → (X ⟶ Y) → (n : ℕ) → s.N n ⟶ Y.obj (Opposite.op { len := n })
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.effectiveEpiFamilyStructOfEquivalence_aux : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (e : C ≌ D) {B : C} {α : Type u_3} (X : α → C) (π : (a : α) → X a ⟶ B)
  {W : D} (ε : (a : α) → e.functor.obj (X a) ⟶ W),
  (∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
      CategoryTheory.CategoryStruct.comp g₁ (e.functor.map (π a₁)) =
          CategoryTheory.CategoryStruct.comp g₂ (e.functor.map (π a₂)) →
        CategoryTheory.CategoryStruct.comp g₁ (ε a₁) = CategoryTheory.CategoryStruct.comp g₂ (ε a₂)) →
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
        CategoryTheory.CategoryStruct.comp g₁
            ((fun a => CategoryTheory.CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₁) =
          CategoryTheory.CategoryStruct.comp g₂
            ((fun a => CategoryTheory.CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₂)
-- Init.Data.Bool
Bool.toInt_true : true.toInt = 1
-- Lean.Parser.Term.Doc
/-- Additional information.  -/
Lean.Parser.Term.Doc.RecommendedSpelling.additionalInformation? : Lean.Parser.Term.Doc.RecommendedSpelling → Option String
-- Init.Data.Vector.Lemmas
Vector.append_inj_left : ∀ {α : Type u_1} {n m : ℕ} {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m}, xs₁ ++ ys₁ = xs₂ ++ ys₂ → xs₁ = xs₂
-- Mathlib.RingTheory.TwoSidedIdeal.Kernel
TwoSidedIdeal.ker_ringCon : ∀ {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_3}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) {x y : R},
  (TwoSidedIdeal.ker f).ringCon x y ↔ f x = f y
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.symm_image_image : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (S : Set A), ⇑e.symm '' ⇑e '' S = S
-- Lean.Parser.Syntax
Lean.Parser.Syntax.numPrec.formatter : Lean.PrettyPrinter.Formatter
-- Aesop.RulePattern
Aesop.RulePattern.open : Aesop.RulePattern → Lean.MetaM (Array Lean.MVarId × Array Lean.LMVarId × Lean.Expr)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- The restriction of a pretrivialization to a set with nonempty intersection with the base set.  -/
Bundle.Pretrivialization.restrictPreimage : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            (e : Bundle.Pretrivialization F proj) →
              {s : Set B} → (s ∩ e.baseSet).Nonempty → Bundle.Pretrivialization F (s.restrictPreimage proj)
-- Init.MetaTypes
/-- If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all`
will fail if they do not make progress.
 -/
Lean.Meta.Simp.Config.failIfUnchanged : Lean.Meta.Simp.Config → Bool
-- Mathlib.Data.List.SplitBy
List.isChain_of_mem_splitBy : ∀ {α : Type u_1} {m : List α} {r : α → α → Bool} {l : List α},
  m ∈ List.splitBy r l → List.IsChain (fun x y => r x y = true) m
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.mk_mul : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (a c : M) (b d : ↥S),
  Localization.mk a b * Localization.mk c d = Localization.mk (a * c) (b * d)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Ring.one? : Lean.Meta.Sym.Arith.Ring → Option Lean.Expr
-- Lean.Attributes
Lean.AttributeKind.global : Lean.AttributeKind
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_bot : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M],
  Submodule.restrictScalars S ⊥ = ⊥
-- Lean.Expr
/-- Replace occurrences of the free variables `fvars` in `e` with `vs`  -/
Lean.Expr.replaceFVars : Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.Expr
-- Mathlib.Analysis.Seminorm
Seminorm.ball_norm_mul_subset : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ}, p.ball 0 (‖k‖ * r) ⊆ k • p.ball 0 r
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getCast!.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) [inst_2 : Inhabited (β a)]
  (a_1 a_2 : Std.DHashMap.Internal.AssocList α β),
  a_1 = a_2 → Std.DHashMap.Internal.AssocList.getCast! a a_1 = Std.DHashMap.Internal.AssocList.getCast! a a_2
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.smul_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_8}
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α) (S : Submodule R M),
  a • S = Submodule.span R ↑(a • S)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toArray_eq_toArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.toArray = t.toListModel.toArray
-- Mathlib.Algebra.Group.Defs
AddCommSemigroup.toAddSemigroup : {G : Type u} → [self : AddCommSemigroup G] → AddSemigroup G
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α}
  {f : β → β}, k' ∈ t.modify k f ↔ k' ∈ t
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
_private.Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen.0.Convex.condExp_mem_of_isFiniteMeasure : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} [MeasureTheory.IsFiniteMeasure μ],
  m ≤ mα →
    MeasureTheory.Integrable f μ → IsClosed s → Convex ℝ s → (∀ᵐ (a : α) ∂μ, f a ∈ s) → ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
-- Mathlib.Data.Set.Card
Set.encard_singleton : ∀ {α : Type u_1} (e : α), {e}.encard = 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.coprod.map_mono : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Mono f] [CategoryTheory.Mono g]
  [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct W X] [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct Y Z],
  CategoryTheory.Mono (CategoryTheory.Limits.coprod.map f g)
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.createsLimitsOfSize : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → CategoryTheory.CreatesLimitsOfSize.{w, w', v, v, max u v, u} (CategoryTheory.Under.forget X)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.node4L : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α},
  l.Sized → m.Sized → r.Sized → (l.node4L x m y r).Sized
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.insert_nonempty : ∀ (u v : ZFSet.{u_1}), (insert u v).Nonempty
-- Mathlib.Order.Directed
IsMax.not_isMin : ∀ {β : Type u_2} [inst : PartialOrder β] [Nontrivial β] [IsDirectedOrder β] {b : β}, IsMax b → ¬IsMin b
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.whiskeringEquivalence_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  (CategoryTheory.Limits.Cone.whiskeringEquivalence e).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun s =>
        CategoryTheory.Limits.Cone.ext
          (CategoryTheory.Iso.refl
            ((((CategoryTheory.Limits.Cone.whiskering e.inverse).comp
                        (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom)).comp
                    (CategoryTheory.Limits.Cone.whiskering e.functor)).obj
                s).pt)
          ⋯)
      ⋯
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUTimes.user : Std.Internal.UV.System.CPUTimes → UInt64
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.mk_eq_zero : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Preorder α] {x : α} (hx : 0 ≤ x), ⟨x, hx⟩ = 0 ↔ x = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_eq_getD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, t[a]! = t.getD a default
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.snd_dirac_unit_compProd_const : ∀ {β : Type u_2} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure β) [MeasureTheory.SFinite μ],
  ((MeasureTheory.Measure.dirac ()).compProd (ProbabilityTheory.Kernel.const Unit μ)).snd = μ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.startsWith_string_empty : ∀ {s : String}, s.startsWith "" = true
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_erase_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF → ∀ {k : α}, Std.DHashMap.Internal.Raw₀.Const.get! (m.erase k) k = default
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.two_pow_le_mul_lcmUpto : ∀ (n : ℕ), 2 ^ n ≤ (n + 1) * n.lcmUpto
-- Batteries.Data.List.Matcher
/-- Make KMP matcher from list pattern.  -/
List.Matcher.ofList : {α : Type u_1} → [BEq α] → List α → List.Matcher α
-- Init.Data.List.Lemmas
List.getElem_eq_getElem?_get : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : i < l.length), l[i] = l[i]?.get ⋯
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_fst_assoc : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.X y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))
          (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
        (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) h)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_of_stronglyMeasurable : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] (hm : m ≤ m₀) [hμm : MeasureTheory.SigmaFinite (μ.trim hm)] {f : α → E},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.Integrable f μ → μ[f | m] = f
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Dist.ext : ∀ {α : Type u_3} {x y : Dist α}, dist = dist → x = y
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_const_sub_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.Integrable X μ →
    ∀ (c : ℝ), ProbabilityTheory.covariance (fun ω => c - X ω) Y μ = -ProbabilityTheory.covariance X Y μ
-- Init.Data.List.Perm
List.isEmpty.eq_1 : ∀ {α : Type u}, [].isEmpty = true
-- Mathlib.Algebra.Group.Basic
mul_eq_of_eq_div : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a = c / b → a * b = c
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
_private.Mathlib.Tactic.CategoryTheory.Coherence.Normalize.0.Mathlib.Tactic.BicategoryLike.evalWhiskerLeft.match_1.eq_2 : ∀ (motive : Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.NormalExpr → Sort u_1)
  (f : Mathlib.Tactic.BicategoryLike.Atom₁) (e : Mathlib.Tactic.BicategoryLike.Mor₂)
  (α : Mathlib.Tactic.BicategoryLike.Structural) (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft)
  (ηs : Mathlib.Tactic.BicategoryLike.NormalExpr)
  (h_1 :
    (f : Mathlib.Tactic.BicategoryLike.Mor₁) →
      (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
        (α : Mathlib.Tactic.BicategoryLike.Structural) → motive f (Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α))
  (h_2 :
    (f : Mathlib.Tactic.BicategoryLike.Atom₁) →
      (e : Mathlib.Tactic.BicategoryLike.Mor₂) →
        (α : Mathlib.Tactic.BicategoryLike.Structural) →
          (η : Mathlib.Tactic.BicategoryLike.WhiskerLeft) →
            (ηs : Mathlib.Tactic.BicategoryLike.NormalExpr) →
              motive (Mathlib.Tactic.BicategoryLike.Mor₁.of f) (Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs))
  (h_3 :
    (e : Lean.Expr) →
      (f g : Mathlib.Tactic.BicategoryLike.Mor₁) →
        (η : Mathlib.Tactic.BicategoryLike.NormalExpr) → motive (Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g) η)
  (h_4 :
    (e : Lean.Expr) →
      (a : Mathlib.Tactic.BicategoryLike.Obj) →
        (η : Mathlib.Tactic.BicategoryLike.NormalExpr) → motive (Mathlib.Tactic.BicategoryLike.Mor₁.id e a) η),
  (match Mathlib.Tactic.BicategoryLike.Mor₁.of f, Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs with
    | f, Mathlib.Tactic.BicategoryLike.NormalExpr.nil e α => h_1 f e α
    | Mathlib.Tactic.BicategoryLike.Mor₁.of f, Mathlib.Tactic.BicategoryLike.NormalExpr.cons e α η ηs => h_2 f e α η ηs
    | Mathlib.Tactic.BicategoryLike.Mor₁.comp e f g, η => h_3 e f g η
    | Mathlib.Tactic.BicategoryLike.Mor₁.id e a, η => h_4 e a η) =
    h_2 f e α η ηs
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.isCoboundedUnder_ge : ∀ {α : Type u_1} {γ : Type u_3} {u : γ → α} {l : Filter γ} [inst : Preorder α] [l.NeBot],
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l u → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) l u
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The evaluation `e C i₁ ··· e C iᵣ : C → ℤ` of a formal product `[i₁, i₂, ..., iᵣ]`.  -/
Profinite.NobelingProof.Products.eval : {I : Type u} → (C : Set (I → Bool)) → [inst : LinearOrder I] → Profinite.NobelingProof.Products I → LocallyConstant ↑C ℤ
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ μ : MeasureTheory.Measure (α × β)}, ρ ≤ μ → ρ.fst ≤ μ.fst
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- The `HasFibers` on `p : 𝒳 ⥤ 𝒮` given by the fibers of `p`  -/
HasFibers.canonical : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] → (p : CategoryTheory.Functor 𝒳 𝒮) → HasFibers p
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.of_mul_of : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} [inst_1 : Add ι] [inst_2 : (i : ι) → AddCommMonoid (A i)]
  [inst_3 : DirectSum.GNonUnitalNonAssocSemiring A] {i j : ι} (a : A i) (b : A j),
  (DirectSum.of A i) a * (DirectSum.of A j) b = (DirectSum.of A (i + j)) (GradedMonoid.GMul.mul a b)
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsStableUnderBaseChangeEpiModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.epiModSerre.IsStableUnderBaseChange
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- Given a morphism of simplicial sets `f : X ⟶ Y` and a subcomplex `A` of `X`,
this is the induced morphism from `A` to `A.image f`.  -/
SSet.Subcomplex.toImage : {X Y : SSet} → (A : X.Subcomplex) → (f : X ⟶ Y) → A.toSSet ⟶ (A.image f).toSSet
-- Mathlib.Algebra.Ring.Defs
NonAssocSemiring.toNatCast : {α : Type u} → [self : NonAssocSemiring α] → NatCast α
-- Aesop.Forward.State
Aesop.ForwardState.instEmptyCollection : EmptyCollection Aesop.ForwardState
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- An element associated to a uniformizer is itself a uniformizer.  -/
Valuation.IsUniformizer.of_associated : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] {v : Valuation K Γ}
  [hv : v.IsRankOneDiscrete] {π₁ π₂ : ↥v.valuationSubring}, v.IsUniformizer ↑π₁ → Associated π₁ π₂ → v.IsUniformizer ↑π₂
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- Given two locally ringed spaces `X` and `Y`, an isomorphism between `X` and `Y` as _sheafed_
spaces can be lifted to an isomorphism `X ⟶ Y` as locally ringed spaces.

This is related to the property that the functor `forgetToSheafedSpace` reflects isomorphisms.
In fact, it is slightly stronger as we do not require `f` to come from a morphism between
_locally_ ringed spaces.
 -/
AlgebraicGeometry.LocallyRingedSpace.isoOfSheafedSpaceIso : {X Y : AlgebraicGeometry.LocallyRingedSpace} → (X.toSheafedSpace ≅ Y.toSheafedSpace) → (X ≅ Y)
-- Mathlib.Analysis.LocallyConvex.Bounded
Filter.HasBasis.isVonNBounded_iff : ∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] {q : ι → Prop} {s : ι → Set E} {A : Set E},
  (nhds 0).HasBasis q s → (Bornology.IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_inter_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter m₂ ⋯).get? k = none
-- Mathlib.Algebra.Group.Shrink
Shrink.instIsLeftCancelMul : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Mul α] [IsLeftCancelMul α], IsLeftCancelMul (Shrink.{v, u_2} α)
-- Batteries.Tactic.GeneralizeProofs
_private.Batteries.Tactic.GeneralizeProofs.0.Batteries.Tactic.GeneralizeProofs.elabConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Batteries.Tactic.GeneralizeProofs.Config
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.congrLeftFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (E : Type u_3) [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {X Y : C ≌ D} (f : X ⟶ Y),
  (CategoryTheory.Equivalence.congrLeftFunctor C D E).map f =
    (CategoryTheory.Equivalence.mkHom
        ((CategoryTheory.Functor.whiskeringLeft D C E).map
          ((CategoryTheory.conjugateEquiv Y.toAdjunction X.toAdjunction) (CategoryTheory.Equivalence.asNatTrans f)))).op
-- Mathlib.Algebra.Category.Ring.Basic
/-- **Alias** of `CategoryTheory.forget_obj`. -/
CommRingCat.forget_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] (X : C), (CategoryTheory.forget C).obj X = CategoryTheory.ToType X
-- Std.Data.HashMap.Basic
/-- Support for the `for` loop construct in `do` blocks.  -/
Std.HashMap.forIn : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        {m : Type w → Type w'} → [Monad m] → {γ : Type w} → (α → β → γ → m (ForInStep γ)) → γ → Std.HashMap α β → m γ
-- Std.Data.HashSet.Raw
/-- Compares two hash sets using Boolean equality on keys.

Returns `true` if the sets contain the same keys, `false` otherwise.
 -/
Std.HashSet.Raw.beq : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → Std.HashSet.Raw α → Bool
-- Mathlib.Algebra.Group.Equiv.TypeTags
MonoidHom.mk.congr_simp : ∀ {M : Type u_10} {N : Type u_11} [inst : MulOne M] [inst_1 : MulOne N] (toOneHom toOneHom_1 : OneHom M N)
  (e_toOneHom : toOneHom = toOneHom_1)
  (map_mul' : ∀ (x y : M), toOneHom.toFun (x * y) = toOneHom.toFun x * toOneHom.toFun y),
  { toOneHom := toOneHom, map_mul' := map_mul' } = { toOneHom := toOneHom_1, map_mul' := ⋯ }
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instIsZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @AlgebraicGeometry.IsSeparated
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOn.congr_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι} {g : α → β}, TendstoUniformlyOn F f p s → Set.EqOn f g s → TendstoUniformlyOn F g p s
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Set.addSubgroupClosure_add_nsmul : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G},
  s.Nonempty → ∀ (n : ℕ), ↑(AddSubgroup.closure s) + n • s = ↑(AddSubgroup.closure s)
-- Init.Data.SInt.Lemmas
Int8.toInt32_lt : ∀ {a b : Int8}, a.toInt32 < b.toInt32 ↔ a < b
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldTR_loop_congr : ∀ {α : Type u} {n m : ℕ} (w : n = m) (f : (i : ℕ) → i < n → α → α) (j : ℕ) (h : j ≤ n) (init : α),
  Nat.foldTR.loop✝ n f j h init = Nat.foldTR.loop✝ m (fun i h => f i ⋯) j ⋯ init
-- Mathlib.Data.Nat.SuccPred
Nat.instPredOrder : PredOrder ℕ