mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `aᶜ` is defined as `a ⇨ ⊥`  -/
Order.Frame.himp_bot : ∀ {α : Type u_1} [self : Order.Frame α] (a : α), a ⇨ ⊥ = aᶜ
-- Mathlib.CategoryTheory.ShrinkYoneda
/-- `uliftCoyoneda` identifies to `shrinkCoyoneda`.  -/
CategoryTheory.uliftYonedaIsoShrinkCoyoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.uliftCoyoneda.{w', v, u} ≅ CategoryTheory.shrinkCoyoneda.{max w' v, v, u}
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normal_of_characteristic : ∀ {A : Type u_4} [inst : AddGroup A] (H : AddSubgroup A) [h : H.Characteristic], H.Normal
-- Mathlib.Analysis.LocallyConvex.Separation
/-- If `A` is convex with nonempty interior and `x ∉ interior A`, then there is a nonzero
continuous `𝕜`-linear functional whose real part attains its maximum on `A` at `x`.  -/
RCLike.geometric_hahn_banach_of_nonempty_interior_point : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {x : E}
  [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  {A : Set E},
  Convex ℝ A → x ∉ interior A → (interior A).Nonempty → ∃ f, f ≠ 0 ∧ ∀ a ∈ A, RCLike.re (f a) ≤ RCLike.re (f x)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instStarSubtypeAEEqFunMemAddSubgroup : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} →
      {R : Type u_6} →
        [inst : NormedAddCommGroup R] →
          [inst_1 : StarAddMonoid R] → [NormedStarGroup R] → {p : ENNReal} → Star ↥(MeasureTheory.Lp R p μ)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toList.congr_simp : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α] (r r_1 : Std.Roo α),
  r = r_1 → r.toList = r_1.toList
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_sq : ∀ {R : Type u_3} [inst : CommRing R] [inst_1 : Invertible 2],
  QuadraticMap.associated QuadraticMap.sq = LinearMap.mul R R
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial.eq_1 : ∀ {R : Type u} [inst : Semiring R] (n : ℕ),
  Polynomial.monomial n =
    { toFun := fun t => { toFinsupp := AddMonoidAlgebra.single n t }, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget_createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections],
  CommMonCat.forget_createsLimit F =
    CategoryTheory.createsLimitOfNatIso
      (CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((CategoryTheory.forget CommMonCat).obj x))
          @CommMonCat.forget_createsLimit._proof_1).symm
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `ℂ_[p]` extends the norm on `ℚ_[p]`.  -/
PadicComplex.norm_extends' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℚ_[p]), ‖↑((algebraMap ℚ_[p] (PadicAlgCl p)) x)‖ = ‖x‖
-- Mathlib.Order.PFilter
/-- A filter on a preorder `P` is a subset of `P` that is
- nonempty
- downward directed
- upward closed.  -/
Order.PFilter : (P : Type u_1) → [Preorder P] → Type u_1
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.πQ.congr_simp : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {ι : CategoryTheory.Functor A C} {X₂ : A} {X₃ : C}
  (f₂ f₂_1 : ι.obj X₂ ⟶ X₃),
  f₂ = f₂_1 →
    ∀ {Q : A} (β β_1 : X₃ ⟶ ι.obj Q),
      β = β_1 →
        ∀ [inst_2 : ι.Full],
          CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β =
            CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂_1 β_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_filter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool},
  (Std.TreeSet.filter f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = false
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insert k v)[k]? = some v
-- Mathlib.Logic.Equiv.Basic
Equiv.sigmaAssocProd_apply_snd_fst : ∀ {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a : (a : α × β) × γ a.1 a.2),
  (Equiv.sigmaAssocProd a).snd.fst = ((Equiv.sigmaEquivProd α β).symm.sigmaCongrLeft' a).fst.snd
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (inner : Std.DHashMap.Raw α fun x => β),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {f : (a : α) → β a → Option (γ a)}
  {k : α}, (Std.ExtDTreeMap.filterMap f t).getKey! k = ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).get!
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_hom₂_ne_zero : ∀ {ι : Type u_2} {M : Type u_5} {N : Type u_6} {O : Type u_7} [inst : CommMonoid M] [inst_1 : CommMonoid N]
  [inst_2 : CommMonoid O] {s : Multiset ι},
  s ≠ 0 →
    ∀ (f : M → N → O),
      (∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d) →
        ∀ (f₁ : ι → M) (f₂ : ι → N),
          (Multiset.map (fun i => f (f₁ i) (f₂ i)) s).prod = f (Multiset.map f₁ s).prod (Multiset.map f₂ s).prod
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.getBasis.eq_def : ∀ {basis : Tactic.ComputeAsymptotics.Basis} (ex : Tactic.ComputeAsymptotics.BasisExtension basis),
  ex.getBasis =
    match basis, ex with
    | .([]), Tactic.ComputeAsymptotics.BasisExtension.nil => []
    | .(basis_hd :: basis_tl), Tactic.ComputeAsymptotics.BasisExtension.keep basis_hd ex => basis_hd :: ex.getBasis
    | basis, Tactic.ComputeAsymptotics.BasisExtension.insert f ex => f :: ex.getBasis
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.add : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {s : Set E},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g s → AnalyticOn 𝕜 (f + g) s
-- Mathlib.Topology.Order
continuous_sup_rng_left : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β},
  Continuous f → Continuous f
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opow_def : ∀ (o₁ o₂ : ONote), o₁ ^ o₂ = o₂.opowAux2 o₁.split
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instBoundedContinuousMapClass : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  [inst_3 : FunLike F α β] [ZeroAtInftyContinuousMapClass F α β], BoundedContinuousMapClass F α β
-- Mathlib.Logic.Function.Basic
/-- **Alias** of `Function.IsPartialInv.injective`. -/
Function.injective_of_isPartialInv : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α}, Function.IsPartialInv f g → Function.Injective f
-- Std.Time.DateTime
/-- Getter for the `Second` inside of a `DateTime`
 -/
Std.Time.DateTime.second : Std.Time.DateTime → Std.Time.Second.Ordinal true
-- Mathlib.Order.Filter.Pi
Filter.coprodᵢ_mono : ∀ {ι : Type u_1} {α : ι → Type u_2} {f₁ f₂ : (i : ι) → Filter (α i)},
  (∀ (i : ι), f₁ i ≤ f₂ i) → Filter.coprodᵢ f₁ ≤ Filter.coprodᵢ f₂
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.fold_eq_foldl_toList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w},
  m.WF →
    ∀ {f : δ → α → β → δ} {init : δ}, Std.HashMap.Raw.fold f init m = List.foldl (fun a b => f a b.1 b.2) init m.toList
-- Init.Control.Lawful.MonadLift.Lemmas
liftM_seqRight : ∀ {m : Type u → Type v} {n : Type u → Type w} [inst : Monad m] [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (x : m α) (y : m β),
  liftM (x *> y) = liftM x *> liftM y
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly : Type
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
CategoryTheory.instPreservesFiniteColimitsHomologicalComplexMapHomologicalComplexOfHasFiniteColimits : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) {ι : Type u_3} (c : ComplexShape ι) [CategoryTheory.Limits.HasFiniteColimits C]
  [inst_5 : F.PreservesZeroMorphisms] [CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.Limits.PreservesFiniteColimits (F.mapHomologicalComplex c)
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- `ReflectsFilteredColimitsOfSize_shrink.{w, w'} F` tries to obtain
`ReflectsFilteredColimitsOfSize.{w, w'} F` from some other `ReflectsFilteredColimitsOfSize F`.
 -/
CategoryTheory.Limits.reflectsFilteredColimitsOfSize_shrink : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Init.Data.SInt.Basic
instMinInt8 : Min Int8
-- Aesop.Tree.Data
Aesop.NormalizationState.notNormal.sizeOf_spec : sizeOf Aesop.NormalizationState.notNormal = 1
-- Std.Data.ExtDTreeMap.Basic
/-- Returns a list of all keys present in the tree map in ascending  order.  -/
Std.ExtDTreeMap.keys : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → List α
-- Lean.LoadDynlib
/-- Dynamically loads a shared library so that its symbols can be used by
the Lean interpreter (e.g., for interpreting `@[extern]` declarations).
Equivalent to passing `--load-dynlib=path` to `lean`.

**Lean never unloads libraries.** Attempting to load a library that defines
symbols shared with a previously loaded library (including itself) will error.
If multiple libraries share common symbols, those symbols should be linked
and loaded as separate libraries.
 -/
Lean.loadDynlib : System.FilePath → IO Unit
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.head_cons : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (a : Γ) (l : Turing.ListBlank Γ), (Turing.ListBlank.cons a l).head = a
-- Aesop.RuleSet
_private.Aesop.RuleSet.0.Aesop.LocalRuleSet.rulePredicate : {α : Type} → Lean.Options → Aesop.LocalRuleSet → (Aesop.Rule α → Bool) → Aesop.Rule α → Bool
-- Init.Data.List.Count
List.filter_eq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] [inst_2 : DecidableEq α] {l : List α} (a : α),
  List.filter (fun x => decide (x = a)) l = List.replicate (List.count a l) a
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The intermediate object in the factorization given by the
small object argument.  -/
CategoryTheory.SmallObject.obj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] → [I.IsCardinalForSmallObjectArgument κ] → {X Y : C} → (X ⟶ Y) → C
-- Lean.Parser.Command
Lean.Parser.Command.optDefDeriving.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      (∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') →
        (∀ (k : α), Std.DHashMap.Raw.Const.get? m₁ k = Std.DHashMap.Raw.Const.get? m₂ k) → m₁.Equiv m₂
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMax'.match_3.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → Sort u_2) (l : Ordnode α) (x : α) (size : ℕ) (rl : Ordnode α)
  (rx : α) (rr : Ordnode α) (h_1 : (l : Ordnode α) → (x : α) → motive l x Ordnode.nil)
  (h_2 :
    (l : Ordnode α) →
      (x : α) → (size : ℕ) → (rl : Ordnode α) → (rx : α) → (rr : Ordnode α) → motive l x (Ordnode.node size rl rx rr)),
  (match l, x, Ordnode.node size rl rx rr with
    | l, x, Ordnode.nil => h_1 l x
    | l, x, Ordnode.node size rl rx rr => h_2 l x size rl rx rr) =
    h_2 l x size rl rx rr
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.toStalk_stalkSpecializes_apply : ∀ {R : Type u_1} [inst : CommRing R] {x y : PrimeSpectrum R} (h : x ⤳ y) (x_1 : R),
  (CategoryTheory.ConcreteCategory.hom ((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalkSpecializes h))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.toStalk R y)) x_1) =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.StructureSheaf.toStalk R x)) x_1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_le_one_iff_le : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b : α}, a * b⁻¹ ≤ 1 ↔ a ≤ b
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A sequential limit of strongly measurable functions is strongly measurable.  -/
stronglyMeasurable_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} {m : MeasurableSpace α} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] (u : Filter ι) [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → β}
  {g : α → β},
  (∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) → Filter.Tendsto f u (nhds g) → MeasureTheory.StronglyMeasurable g
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.AlmostMono.mk.sizeOf_spec : ∀ {α : Type u_5} {ι : Type u_6} {κ : Type u_7} {C : (ι → Option α) → κ} [inst : SizeOf α] [inst_1 : SizeOf ι]
  [inst_2 : SizeOf κ] (line : Combinatorics.Line (Option α) ι) (color : κ)
  (has_color : ∀ (x : α), C (↑line (some x)) = color),
  sizeOf { line := line, color := color, has_color := has_color } = 1 + sizeOf line + sizeOf color
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Triangulated.Localization.instAdditiveLocalizationShiftFunctorInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (W : CategoryTheory.MorphismProperty C) [inst_6 : W.HasLeftCalculusOfFractions]
  [inst_7 : W.IsCompatibleWithTriangulation] (n : ℤ), (CategoryTheory.shiftFunctor W.Localization n).Additive
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
/-- If all `f i`, `i ∈ s`, are nonnegative and each `f i` is less than or equal to `g i`, then the
product of `f i` is less than or equal to the product of `g i`. See also `Finset.prod_le_prod'` for
the case of an ordered commutative multiplicative monoid.  -/
Finset.prod_le_prod : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f g : ι → R} {s : Finset ι}, (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ g i) → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjHomologySelfIso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B) {Z : C} (h : ((HomologicalComplex.single C c j).obj B).homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j A).inv
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((HomologicalComplex.single C c j).map f) j)
        h) =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjHomologySelfIso c j B).inv h)
-- Mathlib.GroupTheory.Index
AddSubgroup.two_smul_mem_of_index_two : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 2 → ∀ (a : G), 2 • a ∈ H
-- Mathlib.Analysis.Meromorphic.Basic
/-- `MeromorphicOn` is invariant under translation, special case where the set is a sphere.  -/
MeromorphicOn.meromorphicOn_sphere_comp_sub_const_iff_meromorphicOn_sphere : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicOn (f ∘ fun x => x - c) (Metric.sphere c R) ↔ MeromorphicOn f (Metric.sphere 0 R)
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry : Type
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- If `α` is an isomorphism between left adjoints, then its conjugate transformation is an
isomorphism. The converse is given in `conjugateEquiv_of_iso`.
 -/
CategoryTheory.conjugateEquiv_iso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : L₂ ⟶ L₁) [CategoryTheory.IsIso α], CategoryTheory.IsIso ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.ι_map_πQ : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {ι : CategoryTheory.Functor A C} {X₂ : A} {X₃ : C}
  (f₂ : ι.obj X₂ ⟶ X₃) {Q : A} (β : X₃ ⟶ ι.obj Q) [inst_2 : ι.Full],
  ι.map (CategoryTheory.Triangulated.AbelianSubcategory.πQ f₂ β) = CategoryTheory.CategoryStruct.comp f₂ β
-- Mathlib.Tactic.Translate.Reorder
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.ArgReorder.reverse.eq_def : ∀ (r : Mathlib.Tactic.Translate.ArgReorder),
  r.reverse =
    { perm := r.perm.reverse,
      argReorders :=
        Array.map (fun x => (Mathlib.Tactic.Translate.ArgReorder.reverse.permuteSingle✝ r x.1, x.2.reverse))
          r.argReorders }
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
ArithmeticFunction.eulerProduct.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] (f : ι → ArithmeticFunction R),
  ArithmeticFunction.eulerProduct f = ∏' (i : ι), f i
-- Mathlib.Order.Defs.Unbundled
IsStrictOrder.mk : ∀ {α : Sort u_1} {r : α → α → Prop} [toIrrefl : Std.Irrefl r] [toIsTrans : IsTrans α r], IsStrictOrder α r
-- Std.Do.SPred.DerivedLaws
/-- Provides a decomposition of a stateful predicate (`P`) into stateful and pure components (`P'` and
`φ`, respectively).
 -/
Std.Do.SPred.Tactic.HasFrame : {σs : List (Type u)} → Std.Do.SPred σs → outParam (Std.Do.SPred σs) → outParam Prop → Prop
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.find?_char_eq_some_iff : ∀ {c : Char} {s : String} {pos : s.Pos},
  s.find? c = some pos ↔ ∃ (h : pos ≠ s.endPos), pos.get h = c ∧ ∀ (pos' : s.Pos) (h' : pos' < pos), pos'.get ⋯ ≠ c
-- Std.Http.Protocol.H1
/-- Returns `true` when the reader is paused waiting for a `canContinue` decision
(server-side only; always `false` on the client side).
 -/
Std.Http.Protocol.H1.Machine.isReaderAwaitingContinue : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.Data.Finset.Sum
Finset.mem_toRight : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {b : β}, b ∈ u.toRight ↔ Sum.inr b ∈ u
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.instSubtypeMemSubalgebraMin_1 : {R : Type u} →
  [inst : CommSemiring R] →
    {C : Type u_1} →
      [inst_1 : CommSemiring C] → [inst_2 : Algebra R C] → (S₁ S₂ : Subalgebra R C) → Algebra ↥(S₁ ⊓ S₂) ↥S₂
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Evaluation at a point as a `MulActionHom`.  -/
Pi.evalMulActionHom : {ι : Type u_1} →
  {M : Type u_2} → {X : ι → Type u_3} → [inst : (i : ι) → SMul M (X i)] → (i : ι) → ((i : ι) → X i) →ₑ[id] X i
-- Mathlib.Probability.Independence.Process.Basic
/-- A random variable $X$ is independent from a stochastic process $(Y_s)_{s \in S}$  if
for all $s_1, ..., s_p \in S$ the variable $Y$ is independent from the family
$(X_{s_1}, ..., X_{s_p})$.  -/
ProbabilityTheory.IndepFun.indepFun_process : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : Type u_4} {𝓨 : S → Type u_5}
  [inst : MeasurableSpace 𝓧] [inst_1 : (i : S) → MeasurableSpace (𝓨 i)] {X : Ω → 𝓧} {Y : (i : S) → Ω → 𝓨 i},
  Measurable X →
    (∀ (i : S), Measurable (Y i)) →
      (∀ (I : Finset S), ProbabilityTheory.IndepFun X (fun ω i => Y (↑i) ω) P) →
        ∀ [MeasureTheory.IsZeroOrProbabilityMeasure P], ProbabilityTheory.IndepFun X (fun ω i => Y i ω) P
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.eq_6 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (a : Lean.Grind.CommRing.Expr) (k : ℕ)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_6 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match a.pow k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.var v => h_3 v
    | a.add b => h_4 a b
    | a.mul b => h_5 a b
    | a.pow k => h_6 a k
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_6 a k
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureInformation.documentation? : Lean.Lsp.SignatureInformation → Option Lean.Lsp.MarkupContent
-- Mathlib.Algebra.Group.Graph
MonoidHom.graph_toSubmonoid : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (f : G →* H), f.graph.toSubmonoid = f.mgraph
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
CategoryTheory.GrothendieckTopology.instHasEnoughPointsBot : ∀ {C : Type w} [inst : CategoryTheory.SmallCategory C], ⊥.HasEnoughPoints
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsClique.map : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {s : Set α},
  G.IsClique s → ∀ {f : α ↪ β}, (SimpleGraph.map (⇑f) G).IsClique (⇑f '' s)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfDom.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {k : P ≃+ M}
  (H : AddSubmonoid.map k.toAddMonoidHom T = S),
  f.ofAddEquivOfDom H = (f.toAddMonoidHom.comp k.toAddMonoidHom).toLocalizationMap ⋯ ⋯ ⋯
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Ioo_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (b : α i), Function.update f i '' Set.Ioo (f i) b = Set.Ioo f (Function.update f i b)
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- A graph is `n`-independent set free iff its complement is `n`-clique free.  -/
SimpleGraph.cliqueFree_compl : ∀ {α : Type u_1} (G : SimpleGraph α) {n : ℕ}, Gᶜ.CliqueFree n ↔ G.IndepSetFree n
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
mem_fixingSubgroup_iff : ∀ (M : Type u_1) {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s : Set α} {m : M},
  m ∈ fixingSubgroup M s ↔ ∀ y ∈ s, m • y = y