mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.forM_eq_forM : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} {m : Type w → Type w'} [inst : Std.TransCmp cmp]
  [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → m PUnit.{w + 1}}, Std.ExtTreeSet.forM f t = forM t f
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.updateUsedSimpsWithZetaDelta : Lean.Meta.Simp.Context → Lean.Meta.Simp.Stats → Lean.MetaM Lean.Meta.Simp.Stats
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.X.congr_simp : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K K_1 : HomologicalComplex C c),
  K = K_1 → ∀ (a a_1 : Option ι), a = a_1 → HomologicalComplex.extend.X K a = HomologicalComplex.extend.X K_1 a_1
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_nsmul_addOrderOf_sub : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ},
  addOrderOf x ≠ 0 → n ∣ addOrderOf x → addOrderOf ((addOrderOf x / n) • x) = n
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.μ_naturality₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C))
  {m n m' n' : M} (f : m ⟶ m') (g : n ⟶ n') (X : C) [inst_3 : F.LaxMonoidal],
  CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X))
      (CategoryTheory.CategoryStruct.comp ((F.obj n').map ((F.map f).app X))
        ((CategoryTheory.Functor.LaxMonoidal.μ F m' n').app X)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F m n).app X)
      ((F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)).app X)
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
instIsRegularCardinalOrderOrdinal : IsRegularCardinalOrder Ordinal.{u_2}
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmoothOfRelativeDimension.of_algEquiv : ∀ (n : ℕ) {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_1}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T) [Algebra.IsStandardSmoothOfRelativeDimension n R S],
  Algebra.IsStandardSmoothOfRelativeDimension n R T
-- Mathlib.Data.Set.Restrict
Set.domRestrict_id : ∀ {α : Type u_1} (s : Set α), s.domRestrict id = Subtype.val
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.CofibrantObject.homMk_homMk_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] {X Y Z : C} [inst_3 : HomotopicalAlgebra.IsCofibrant X]
  [inst_4 : HomotopicalAlgebra.IsCofibrant Y] [inst_5 : HomotopicalAlgebra.IsCofibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z)
  {Z_1 : HomotopicalAlgebra.CofibrantObject C} (h : HomotopicalAlgebra.CofibrantObject.mk Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.homMk f)
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.homMk g) h) =
    CategoryTheory.CategoryStruct.comp
      (HomotopicalAlgebra.CofibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g)) h
-- Mathlib.Data.Multiset.AddSub
Multiset.instSub : {α : Type u_1} → [DecidableEq α] → Sub (Multiset α)
-- Mathlib.Data.Finset.Basic
Finset.erase_union_distrib : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (a : α), (s ∪ t).erase a = s.erase a ∪ t.erase a
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_conj : ∀ {α : Type u_2} {f g : Equiv.Perm α} {x y : α}, (g * f * g⁻¹).SameCycle x y ↔ f.SameCycle (g⁻¹ x) (g⁻¹ y)
-- Mathlib.Data.Multiset.Filter
Multiset.filter_add_not : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Multiset α),
  Multiset.filter p s + Multiset.filter (fun a => ¬p a) s = s
-- Mathlib.Analysis.Fourier.AddCircle
ContinuousMap.toLp.congr_simp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  (𝕜 : Type u_3) [inst_6 : Fact (1 ≤ p)] [inst_7 : NormedRing 𝕜] [inst_8 : Module 𝕜 E] [inst_9 : IsBoundedSMul 𝕜 E],
  ContinuousMap.toLp p μ 𝕜 = ContinuousMap.toLp p μ 𝕜
-- Mathlib.Order.Hom.Basic
map_inv_lt_map_inv_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : EquivLike F α β]
  [OrderIsoClass F α β] (f : F) {a b : β}, EquivLike.inv f b < EquivLike.inv f a ↔ b < a
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet_ι_app : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : CategoryTheory.CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop)
  [inst_1 : ∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] (j : Subtype P),
  (CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSet P).ι.app j =
    CategoryTheory.ObjectProperty.homMk ((PartOrdEmb.coconeOfPredicateSet P).ι.app j)
-- Mathlib.Topology.Instances.TrivSqZeroExt
/-- This is not an instance due to complaints by the `fails_quickly` linter. At any rate, we only
really care about the `IsTopologicalRing` instance below.  -/
TrivSqZeroExt.topologicalSemiring : ∀ {R : Type u_3} {M : Type u_4} [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M] [inst_2 : Semiring R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module Rᵐᵒᵖ M] [IsTopologicalSemiring R] [ContinuousAdd M]
  [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M], IsTopologicalSemiring (TrivSqZeroExt R M)
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- The equivalence between the dihedral group and the sum of `ZMod`s.  -/
DihedralGroup.equivSum : {n : ℕ} → DihedralGroup n ≃ ZMod n ⊕ ZMod n
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_singleton : ∀ {b n : ℕ}, Nat.ofDigits b [n] = n
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldlM_loop_lt : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n i : ℕ} [inst : Monad m] (f : α → Fin n → m α) (x : α) (h : i < n),
  Fin.foldlM.loop✝ n f x i = do
    let x ← f x ⟨i, h⟩
    Fin.foldlM.loop✝ n f x (i + 1)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Ring.lift_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonAssocSemiring (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)]
  [inst_6 : Nonempty ι] (P : Type u_7) [inst_7 : NonAssocSemiring P] (g : (i : ι) → G i →+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (i : ι) (x : G i),
  (DirectLimit.Ring.lift G f P g Hg) ((DirectLimit.Ring.of G f i) x) = (g i) x
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
RingHom.QuasiFiniteAt.eq_1 : ∀ {R : Type u_6} {S : Type u_7} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (p : Ideal S)
  [inst_2 : p.IsPrime], f.QuasiFiniteAt p = Algebra.QuasiFiniteAt R p
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.unsat_eqC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p : Lean.Grind.CommRing.Poly) (k : ℤ),
  Lean.Grind.CommRing.Stepwise.unsat_eq_certC p k c = true → Lean.Grind.CommRing.Poly.denote ctx p = 0 → False
-- Mathlib.CategoryTheory.ObjectProperty.Ind
CategoryTheory.ObjectProperty.le_ind : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C), P ≤ P.ind
-- Mathlib.Order.RelClasses
/-- **Alias** of `LE.le.not_ssuperset`.

---

Set notation form of `LE.le.not_gt` -/
LE.le.not_ssubset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊆ b → ¬b ⊂ a
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.mul : ∀ {α : Type u_1} {β : Type u_3} [inst : NormedField β] {t u v w : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l t u → Asymptotics.IsEquivalent l v w → Asymptotics.IsEquivalent l (t * v) (u * w)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The difference with `Finset.prod_involution` is that the involution is a non-dependent function,
rather than being allowed to use membership of the domain of the product.  -/
Finset.prod_ninvolution : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} (g : ι → ι),
  (∀ (a : ι), f a * f (g a) = 1) →
    (∀ (a : ι), f a ≠ 1 → g a ≠ a) → (∀ (a : ι), g a ∈ s) → (∀ (a : ι), g (g a) = a) → ∏ x ∈ s, f x = 1
-- Init.Data.Option.Lemmas
Option.bind_fun_some : ∀ {α : Type u_1} (x : Option α), x.bind some = x
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
/-- When `j` is at the boundary of the embedding `e` of complex shapes,
this is a homology data for `K.truncGE' e` in degree `j`: the homology is
given by `K.homology j'` where `e.f j = j'`.  -/
HomologicalComplex.truncGE'.homologyData : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsTruncGE] →
                    [inst_3 : ∀ (i' : ι'), K.HasHomology i'] →
                      (i j k : ι) →
                        c.next j = k → {j' : ι'} → e.f j = j' → e.BoundaryGE j → ((K.truncGE' e).sc' i j k).HomologyData
-- Mathlib.Condensed.AB
Condensed.instAB4CondensedMod : ∀ (R : Type (u + 1)) [inst : Ring R], CategoryTheory.AB4 (CondensedMod R)
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.injective : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N), Function.Injective ⇑e
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Polarization identity: The inner product, in terms of the norm.  -/
inner_eq_sum_norm_sq_div_four : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E),
  inner 𝕜 x y = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - RCLike.I • y‖ ^ 2 - ↑‖x + RCLike.I • y‖ ^ 2) * RCLike.I) / 4
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurveOn.mono : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s s' : Set ℝ},
  IsIntegralCurveOn γ v s → s' ⊆ s → IsIntegralCurveOn γ v s'
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedCancelSMul.le_of_smul_le_smul_right : ∀ {G : Type u_3} {P : Type u_4} {inst : LE G} {inst_1 : LE P} {inst_2 : SMul G P} [self : IsOrderedCancelSMul G P]
  (a b : G) (c : P), a • c ≤ b • c → a ≤ b
-- Mathlib.Data.Finset.Sups
Finset.card_disjSups_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] (s t : Finset α), (s.disjSups t).card ≤ s.card * t.card
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_X_sub_pow : ∀ {R : Type u} [inst : CommRing R] (n k : ℕ) (c : R),
  (⇑Polynomial.derivative)^[k] ((Polynomial.X - Polynomial.C c) ^ n) =
    n.descFactorial k • (Polynomial.X - Polynomial.C c) ^ (n - k)
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_inter_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioi a ∩ Set.Iio b = Set.Ioo a b
-- Init.Data.Char.Lemmas
Char.ofNat_toNat : ∀ (c : Char), Char.ofNat c.toNat = c
-- Mathlib.Tactic.Push.Attr
Mathlib.Tactic.Push.instInhabitedHead : Inhabited Mathlib.Tactic.Push.Head
-- Lean.Elab.Tactic.Basic
/-- Backtracking `try`/`catch`. This is used for the `MonadExcept` instance for `TacticM`.
 -/
Lean.Elab.Tactic.tryCatchRestore : {α : Type} → Lean.Elab.Tactic.TacticM α → (Lean.Exception → Lean.Elab.Tactic.TacticM α) → Lean.Elab.Tactic.TacticM α
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_mono : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {f : α → β}, μ ≤ ν → Measurable f → MeasureTheory.Measure.map f μ ≤ MeasureTheory.Measure.map f ν
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.instCategory : (J : Type u_1) → [inst : LinearOrder J] → CategoryTheory.Category.{u_1, u_1} (CategoryTheory.SimplicialThickening J)
-- Mathlib.Order.WellFounded
WellFounded.min_le : ∀ {β : Type u_2} [inst : LinearOrder β] (h : WellFounded fun x1 x2 => x1 < x2) {x : β} {s : Set β} (hx : x ∈ s),
  h.min s ⋯ ≤ x
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.CokernelData.ofSection_lift : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) (f : M₁ →ₗ[A] M₂) {ι : Type w₁}
  (g₁ : ι → M₁) (s : M₂ → pres₂.G →₀ A) (hs : ∀ (m₂ : M₂), pres₂.π (s m₂) = m₂) (i : ι),
  (Module.Presentation.CokernelData.ofSection pres₂ f g₁ s hs).lift i = s (f (g₁ i))
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.algebraMap_rootFormIn : ∀ {ι : 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) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : P.IsValuedIn S] [inst_11 : Fintype ι] (x y : ↥(P.rootSpan S)),
  (algebraMap S R) (((P.RootFormIn S) x) y) = (P.RootForm ↑x) ↑y
-- Init.Meta.Defs
/-- Syntax that represents a command.
 -/
Lean.Syntax.Command : Type
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.pow_const : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] [inst_3 : UniformSpace β]
  {f : β → α}, UniformContinuous f → ∀ (n : ℕ), UniformContinuous fun x => f x ^ n
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ_res_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type u_2} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (x : ↑X) (hx : x ∈ U)
  [inst_3 : CategoryTheory.ConcreteCategory C FC] (s : CC (F.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (F.map i.op)) s) =
    (CategoryTheory.ConcreteCategory.hom (F.germ V x ⋯)) s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_snd_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  (U : CategoryTheory.Functor X Y) (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U).obj S).snd.obj X_1 =
    S.snd.obj (U.obj X_1)
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.version.getMinor : Unit → ℕ
-- Mathlib.Order.SuccPred.InitialSeg
InitialSeg.isSuccPrelimit_apply_iff : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ≤i β),
  Order.IsSuccPrelimit (f a) ↔ Order.IsSuccPrelimit a
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
/-- Embedding of `pathGraph 2` into the first two elements of `pathGraph n` for `2 ≤ n`  -/
SimpleGraph.pathGraph_two_embedding : (n : ℕ) → 2 ≤ n → SimpleGraph.pathGraph 2 ↪g SimpleGraph.pathGraph n
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The functor which sends a sheaf of modules to its type of sections.  -/
SheafOfModules.sectionsFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) → CategoryTheory.Functor (SheafOfModules R) (Type (max u₁ v))
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_of_condIndep_of_le_left : ∀ {Ω : Type u_1} {m' m₁ m₂ m₃ mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ → m₃ ≤ m₁ → ProbabilityTheory.CondIndep m' m₃ m₂ hm' μ
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).functor.Additive
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_associativity_assoc : ∀ {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'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] (d : D) (c c' : C)
  {Z : D'}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d) c) c' ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorObj c c'))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso (F.obj d) c c').hom h) =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c').hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxRightLinear.δᵣ F
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c')
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
            (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c) c')
          h))
-- Init.Data.Fin.Lemmas
Fin.rev_castAdd : ∀ {n : ℕ} (k : Fin n) (m : ℕ), (Fin.castAdd m k).rev = k.rev.addNat m
-- Mathlib.GroupTheory.Congruence.Defs
/-- A coercion from a congruence relation to its underlying binary relation.  -/
Con.instFunLikeForallProp : {M : Type u_1} → [inst : Mul M] → FunLike (Con M) M (M → Prop)
-- Mathlib.CategoryTheory.Generator.Basic
/-- The inclusion morphisms to `∐ (P.coproductFromFamily X)`.  -/
CategoryTheory.ObjectProperty.ιCoproductFrom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.ObjectProperty C) →
      {X : C} →
        [inst_1 : CategoryTheory.Limits.HasCoproduct (P.coproductFromFamily X)] →
          {Y : C} → (Y ⟶ X) → P Y → (Y ⟶ ∐ P.coproductFromFamily X)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.whisker_exchange : ∀ {B : Type u} [inst : Quiver B] {a b c : B} {f g : CategoryTheory.FreeBicategory.Hom a b}
  {h i : CategoryTheory.FreeBicategory.Hom b c} (η : CategoryTheory.FreeBicategory.Hom₂ f g)
  (θ : CategoryTheory.FreeBicategory.Hom₂ h i),
  CategoryTheory.FreeBicategory.Rel
    ((CategoryTheory.FreeBicategory.Hom₂.whisker_left f θ).vcomp (CategoryTheory.FreeBicategory.Hom₂.whisker_right i η))
    ((CategoryTheory.FreeBicategory.Hom₂.whisker_right h η).vcomp (CategoryTheory.FreeBicategory.Hom₂.whisker_left g θ))
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.mul_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [ContinuousMul α]
  {s : Set β}, Multipliable (f ∘ Subtype.val) → Multipliable (f ∘ Subtype.val) → Multipliable f
-- Mathlib.Topology.ClusterPt
clusterPt_iff_lift'_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X}, ClusterPt x F ↔ pure x ≤ F.lift' closure
-- Aesop.Rule
Aesop.instInhabitedNormRuleInfo : Inhabited Aesop.NormRuleInfo
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_hom_whiskerRight'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f] (Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.inv f) Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h) =
    h
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyRel.symm_trans : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ f₂ : C(X, Y)} {S : Set X}
  (F : f₀.HomotopyRel f₁ S) (G : f₁.HomotopyRel f₂ S), (F.trans G).symm = G.symm.trans F.symm
-- Mathlib.Data.Finset.Sym
Finset.sym_univ : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (n : ℕ), Finset.univ.sym n = Finset.univ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGet!_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited β],
          Std.DTreeMap.Internal.Impl.Const.get! t₁ k = Std.DTreeMap.Internal.Impl.Const.get! t₂ k
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Std.Do.PredTrans.pushExcept.match_1.eq_2 : ∀ {α ε : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.RingTheory.Spectrum.Maximal.Basic
MaximalSpectrum.equivSubtype_symm_apply_asIdeal : ∀ (R : Type u_1) [inst : CommSemiring R] (I : { I // I.IsMaximal }),
  ((MaximalSpectrum.equivSubtype R).symm I).asIdeal = ↑I
-- Mathlib.Data.List.Sublists
List.sublistsLenAux_zero : ∀ {α : Type u} {β : Type v} (l : List α) (f : List α → β) (r : List β), List.sublistsLenAux 0 l f r = f [] :: r
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey! k = default
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.LogConfig.mk : Option System.FilePath → Option (Std.HashSet String) → Option (Std.HashSet String) → Lean.Lsp.LogConfig
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_succEmb_Ioc : ∀ {n : ℕ} (i j : Fin n), Finset.map (Fin.succEmb n) (Finset.Ioc i j) = Finset.Ioc i.succ j.succ
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.equivStructuredArrow_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.Cocone.equivStructuredArrow F).counitIso =
    CategoryTheory.NatIso.ofComponents (fun x => x.eta.symm) ⋯