mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ_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.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LeftLinear C] (c : C) (d : D) {Z : D'}
  (h : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d) h) =
    h
-- Mathlib.Data.String.Basic
String.instLinearOrder : LinearOrder String
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
MeasureTheory.withDensityᵥ_rnDeriv_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν] [MeasureTheory.SigmaFinite μ] {f : α → E},
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable f μ → (ν.withDensityᵥ fun x => (μ.rnDeriv ν x).toReal • f x) = μ.withDensityᵥ f
-- Mathlib.Order.Minimal
/-- If `P y` holds, and everything satisfying `P` is above `y`, then `y` is the unique minimal
element satisfying `P`.  -/
minimal_iff_eq : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : PartialOrder α],
  P y → (∀ ⦃x : α⦄, P x → y ≤ x) → (Minimal P x ↔ x = y)
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iic_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Iic a)), Subtype.val '' Set.Ici b = Set.Icc (↑b) a
-- Std.Async.ContextAsync
/-- Runs a `ContextAsync` computation with a new context that cancels after the execution of the computation.
See also `ContextAsync.runIn` for running with an existing context.
 -/
Std.Async.ContextAsync.run : {α : Type} → Std.Async.ContextAsync α → Std.Async.Async α
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
_private.Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Logic.Relator
Relator.RightTotal.symm : ∀ {α : Type u_1} {β : Type u_2} {r₁₂ : α → β → Prop} {r₂₁ : β → α → Prop},
  (∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) → Relator.RightTotal r₁₂ → Relator.LeftTotal r₂₁
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.starCenterIsoCentroid_apply : ∀ {α : Type u_1} [inst : NonAssocSemiring α] [inst_1 : StarRing α] (a : ↥(NonUnitalStarSubsemiring.center α)),
  CentroidHom.starCenterIsoCentroid a = CentroidHom.starCenterToCentroid a
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.IsStrongGenerator.colimitsCardinalClosure_eq_isCardinalPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v, u} P],
  P.IsStrongGenerator →
    P ≤ CategoryTheory.isCardinalPresentable C κ →
      CategoryTheory.isCardinalPresentable C κ = P.colimitsCardinalClosure κ
-- Mathlib.Algebra.GCDMonoid.Basic
instAssociativeLcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α], Std.Associative lcm
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_functorPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} (R : CategoryTheory.Presieve (F.obj X)),
  CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F R) ≤ R
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.instNonemptyCarrierObjTopCatToTop₀ : ∀ (n : SimplexCategory), Nonempty ↑(SimplexCategory.toTop₀.obj n)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- Construction of a limit cone for a functor `J ⥤ ShortComplex C` using the limits
of the three components `J ⥤ C`.  -/
CategoryTheory.ShortComplex.limitCone : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) →
            [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)] →
              [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)] →
                [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)] → CategoryTheory.Limits.Cone F
-- Mathlib.Data.PFun
PFun.image_inter : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s t : Set α), f.image (s ∩ t) ⊆ f.image s ∩ f.image t
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.not_isPrincipal_iff`. -/
Ordinal.not_principal_iff : ∀ {o : Ordinal.{u}} {op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}},
  ¬Ordinal.IsPrincipal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The **Banach-Alaoglu theorem**: closed balls of the dual of a normed space `E` are compact in
the weak-star topology.  -/
WeakDual.isCompact_closedBall : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [ProperSpace 𝕜] (x' : StrongDual 𝕜 E) (r : ℝ),
  IsCompact (⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall x' r)
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonForall : Array Lean.Expr → Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Order.Hom.Basic
OrderHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (toFun : α → β) (monotone' : Monotone toFun), sizeOf { toFun := toFun, monotone' := monotone' } = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso_inv_app_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor AugmentedSimplexCategoryᵒᵖ C),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObjectFunctorCompToArrowIso.inv.app X).left =
    CategoryTheory.CategoryStruct.id
      (X.obj
        (match CategoryTheory.WithTerminal.incl.obj (Opposite.op { len := 0 }) with
        | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
        | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star))
-- Mathlib.CategoryTheory.Square
/-- The equivalence `(Square C)ᵒᵖ ≌ Square Cᵒᵖ`.  -/
CategoryTheory.Square.opEquivalence : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (CategoryTheory.Square C)ᵒᵖ ≌ CategoryTheory.Square Cᵒᵖ
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
/-- If the columns of a square matrix are linearly independent, then the matrix is nonsingular.  -/
Matrix.Nonsingular.of_linearIndependent_col : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {A : Matrix n n R}, LinearIndependent R A.col → A.Nonsingular
-- Mathlib.Data.DFinsupp.BigOperators
/-- While we didn't need decidable instances to define it, we do to reduce it to a sum  -/
DFinsupp.sumZeroHom_apply : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] (φ : (i : ι) → ZeroHom (β i) γ)
  (f : Π₀ (i : ι), β i), (DFinsupp.sumZeroHom φ) f = f.sum fun x => ⇑(φ x)
-- Lean.Setup
Lean.instBEqIRPhases : BEq Lean.IRPhases
-- Mathlib.Order.WithBot
WithBot.le_unbotD_iff : ∀ {α : Type u_1} {a b : α} [inst : LE α] {x : WithBot α}, x ≠ ⊥ → (b ≤ WithBot.unbotD a x ↔ ↑b ≤ x)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.of_subsingleton : ∀ {V : Type u} {G : SimpleGraph V} [Subsingleton V], G.Preconnected
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.projRestricts_eq_id : ∀ {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [inst : (i : I) → Decidable (J i)],
  Profinite.NobelingProof.ProjRestricts C ⋯ = id
-- Init.Data.Order.Ord
Std.LawfulBEqCmp.opposite : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering} [Std.OrientedCmp cmp] [Std.LawfulBEqCmp cmp],
  Std.LawfulBEqCmp fun a b => cmp b a
-- Mathlib.Data.Finset.NAry
Finset.Nonempty.of_image₂_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  (Finset.image₂ f s t).Nonempty → s.Nonempty
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.eq_of_dist_eq_zero : ∀ {E : ℕ → Type u_1} (x y : (n : ℕ) → E n), dist x y = 0 → x = y
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.sZMod.eq_2 : ∀ (p i : ℕ), LucasLehmer.sZMod p i.succ = LucasLehmer.sZMod p i ^ 2 - 2
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_δ''_apply : ∀ {S : SSet} {n : ℕ} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : i ≤ j.castSucc)
  (x : S.obj (Opposite.op { len := n + 2 })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S (i.castLT ⋯)))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S j.succ)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i)) x)
-- Mathlib.Algebra.Ring.NonZeroDivisors
le_nonZeroDivisorsRight_iff_isRightRegular : ∀ {R : Type u_1} [inst : Ring R] {S : Submonoid R}, S ≤ nonZeroDivisorsRight R ↔ ∀ (s : ↥S), IsRightRegular ↑s
-- Init.System.IO
/-- Runs a `BaseIO` action, which cannot throw an exception, in any other `EIO` monad.

This function is usually used implicitly via [automatic monadic
lifting](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=lifting-monads) rather being than called explicitly.
 -/
BaseIO.toEIO : {α ε : Type} → BaseIO α → EIO ε α
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.left_distrib : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation.below ⋯
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.mono_set_ae : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f t μ → s ≤ᵐ[μ] t → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.subtype_map : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {p : α → Prop} {q : β → Prop}
  {f : α → β}, UniformContinuous f → ∀ (h : ∀ (x : α), p x → q (f x)), UniformContinuous (Subtype.map f h)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.toLinearIsometry_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F),
  (LinearIsometryEquiv.rTensor G f).toLinearIsometry = LinearIsometry.rTensor G f.toLinearIsometry
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.IsoLift.mk : Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → Mathlib.Tactic.BicategoryLike.IsoLift
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.length_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF → (Std.DTreeMap.Raw.Const.toList t).length = t.size
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The naturality for the left whiskering.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mkNaturalityWhiskerLeft : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m] →
    Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.NormalizedHom →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.Mor₁ →
              Mathlib.Tactic.BicategoryLike.Mor₁ →
                Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                  Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                    Mathlib.Tactic.BicategoryLike.Mor₂Iso →
                      Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → m Lean.Expr
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix_eq_apply_of_acc : ∀ {α : Sort u_2} {C : α → Sort u_1} [inst : ∀ (a : α), Nonempty (C a)] {R : α → α → Prop}
  {F : (a : α) → ((a' : α) → R a' a → C a') → C a} {a : α},
  Acc R a → WellFounded.partialExtrinsicFix R F a = F a fun a' x => WellFounded.partialExtrinsicFix R F a'
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.ge_of_finite : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] [IsCodirectedOrder α] [Finite β] {f : Filter β}
  {u : β → α}, Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_iff_continuousAt_domRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {x : α}
  {s : Set α} (h : x ∈ s), ContinuousWithinAt f s x ↔ ContinuousAt (s.domRestrict f) ⟨x, h⟩
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.fderivCLM_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  ⇑((ContDiffMapSupportedIn.fderivCLM 𝕜 n k) f) = if k + 1 ≤ n then fderiv ℝ ⇑f else 0
-- Mathlib.Algebra.Lie.CartanCriterion
/-- The Killing radical of a finite-dimensional Lie algebra is contained in the solvable radical.  -/
LieAlgebra.killingCompl_top_le_radical : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [CharZero R] [IsDomain R] [inst_3 : LieRing L]
  [inst_4 : LieAlgebra R L] [IsNoetherian R L] [Module.Free R L], LieIdeal.killingCompl R L ⊤ ≤ LieAlgebra.radical R L
-- Mathlib.Order.ULift
ULift.instMax_mathlib.eq_1 : ∀ {α : Type u} [inst : Max α], ULift.instMax_mathlib = { max := fun x y => { down := x.down ⊔ y.down } }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_left_strictMonoOn₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosMono G₀] {n : ℤ},
  0 < n → StrictMonoOn (fun a => a ^ n) {a | 0 ≤ a}
-- Mathlib.Topology.NhdsSet
nhdsSet_diagonal : ∀ (X : Type u_4) [inst : TopologicalSpace (X × X)], nhdsSet (Set.diagonal X) = ⨆ x, nhds (x, x)
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.eq_1 : ∀ {α : Type u_2} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s t : Set α),
  MeasureTheory.AEDisjoint μ s t = (μ (s ∩ t) = 0)
-- Lean.Parser.Syntax
Lean.Parser.Syntax.cat : Lean.Parser.Parser
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.getLastD.match_1.splitter : {α : Type u_1} →
  (motive : List α → α → Sort u_2) →
    (x : List α) →
      (x_1 : α) → ((a₀ : α) → motive [] a₀) → ((a : α) → (as : List α) → (x : α) → motive (a :: as) x) → motive x x_1
-- Mathlib.Order.Filter.Ring
Filter.EventuallyLE.add_le_add : ∀ {α : Type u} {β : Type v} [inst : Add β] [inst_1 : Preorder β] [AddLeftMono β] [AddRightMono β] {l : Filter α}
  {f₁ f₂ g₁ g₂ : α → β}, f₁ ≤ᶠ[l] f₂ → g₁ ≤ᶠ[l] g₂ → f₁ + g₁ ≤ᶠ[l] f₂ + g₂
-- Std.Data.ExtDTreeMap.Lemmas
/-- Simpler variant of `get!_filter` when `LawfulEqCmp` is available.  -/
Std.ExtDTreeMap.Const.get!_filter' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited β] {f : α → β → Bool} {k : α},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.filter f t) k =
    (Option.filter (f k) (Std.ExtDTreeMap.Const.get? t k)).get!
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.toList_of : ∀ {α : Type u_1} (x : α), FreeAddMonoid.toList (FreeAddMonoid.of x) = [x]
-- Mathlib.GroupTheory.FreeGroup.Orbit
FreeGroup.startsWith.smul_def : ∀ {α : Type u_1} {X : Type u_2} [inst : DecidableEq α] [inst_1 : MulAction (FreeGroup α) X] {w : α × Bool}
  {g : ↑(FreeGroup.startsWith w)} {x : X}, g • x = ↑g • x
-- Mathlib.Order.CompleteLattice.Defs
CompleteLinearOrder.toCompleteLattice : {α : Type u_8} → [self : CompleteLinearOrder α] → CompleteLattice α
-- Mathlib.Order.MinMax
min_eq_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.pullback_monoidHom.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : R1Space α] [inst_2 : Group α]
  [inst_3 : TopologicalSpace β] [inst_4 : R1Space β] [inst_5 : Group β] [inst_6 : ContinuousMul β]
  [inst_7 : NormedAddCommGroup γ] {φ : α →* β} (hφ : Topology.IsClosedEmbedding ⇑φ)
  (f : CompactlySupportedContinuousMap β γ) (b : β),
  CompactlySupportedContinuousMap.pullback_monoidHom hφ f b =
    { toFun := fun a => f (b * φ a), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.equivalenceOfReindexing_unitIso : ∀ {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}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  (CategoryTheory.Limits.Cocone.equivalenceOfReindexing e α).unitIso =
    CategoryTheory.NatIso.ofComponents' (fun s => CategoryTheory.Limits.Cocone.extInv (CategoryTheory.Iso.refl s.pt) ⋯)
        ⋯ ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Limits.Cocone.whiskering e.functor).rightUnitor.symm
          ((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
            (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv)) ≪≫
        CategoryTheory.Functor.isoWhiskerRight
            ((CategoryTheory.Limits.Cocone.whiskering e.functor).isoWhiskerLeft
              (CategoryTheory.NatIso.ofComponents'
                (fun s => CategoryTheory.Limits.Cocone.extInv (CategoryTheory.Iso.refl s.pt) ⋯) ⋯))
            ((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
              (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv)) ≪≫
          CategoryTheory.Functor.isoWhiskerRight
              ((CategoryTheory.Limits.Cocone.whiskering e.functor).associator
                  (CategoryTheory.Limits.Cocone.precompose α.inv) (CategoryTheory.Limits.Cocone.precompose α.hom)).symm
              ((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
                (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv)) ≪≫
            ((CategoryTheory.Limits.Cocone.whiskering e.functor).comp
                  (CategoryTheory.Limits.Cocone.precompose α.inv)).associator
              (CategoryTheory.Limits.Cocone.precompose α.hom)
              ((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
                (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv))
-- Init.Data.BEq
EquivBEq.toReflBEq : ∀ {α : Type u_1} {inst : BEq α} [self : EquivBEq α], ReflBEq α
-- Mathlib.Analysis.InnerProductSpace.Calculus
Differentiable.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E},
  Differentiable ℝ f → Differentiable ℝ g → Differentiable ℝ fun x => inner 𝕜 (f x) (g x)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextDocumentItem.toJson : Lean.Lsp.TextDocumentItem → Lean.Json
-- Init.Data.List.Lemmas
List.flatten_filter_not_isEmpty : ∀ {α : Type u_1} {L : List (List α)}, (List.filter (fun l => !l.isEmpty) L).flatten = L.flatten
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_middle_coeff : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → (Polynomial.trinomial k m n u v w).coeff m = v
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CanonArgKey.f : Lean.Meta.Grind.CanonArgKey → Lean.Expr
-- Mathlib.Algebra.Order.Field.Basic
div_lt_iff_of_neg' : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (b / c < a ↔ c * a < b)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix.injEq : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr)
  (lhs_1 : Bool) (s_1 : Lean.Grind.AC.Seq) (c₁_1 : Lean.Meta.Grind.AC.EqCnstr) (c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr),
  (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_suffix lhs_1 s_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Order.Filter.Prod
Filter.coprod_mono : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β}, f₁ ≤ f₂ → g₁ ≤ g₂ → f₁.coprod g₁ ≤ f₂.coprod g₂
-- Mathlib.Order.Disjoint
Complementeds.instBoundedOrder : {α : Type u_1} → [inst : Lattice α] → [inst_1 : BoundedOrder α] → BoundedOrder (Complementeds α)
-- Mathlib.Order.Bounds.Basic
bddBelow_preimage_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddBelow (⇑OrderDual.ofDual ⁻¹' s) ↔ BddAbove s
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.isBridge_sup_edge : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, (G ⊔ SimpleGraph.edge u v).IsBridge s(u, v) ↔ G.IsBridge s(u, v)
-- Init.Data.BitVec.Bitblast
BitVec.extractAndExtendBit.eq_1 : ∀ {w : ℕ} (idx len : ℕ) (x : BitVec w),
  BitVec.extractAndExtendBit idx len x = BitVec.zeroExtend len (BitVec.extractLsb' idx 1 x)
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given left-closed right-unbounded range as a list in ascending order.
 -/
Std.Rci.toList : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxi.IsAlwaysFinite α] → Std.Rci α → List α
-- Init.Data.Bool
Bool.coe_iff_coe : ∀ {a b : Bool}, (a = true ↔ b = true) ↔ a = b
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.frequently_ae_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {p : α → Prop}, (∃ᵐ (a : α) ∂μ, p a) ↔ μ {a | p a} ≠ 0
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.extractAndExtendAux.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (x = 0 → motive 0) → ((n' : ℕ) → x = n'.succ → motive n'.succ) → motive x
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C}
  (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl))
  (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c)
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  [CategoryTheory.Limits.MonoCoprod C] (inr : c₂.pt ⟶ c.pt),
  (∀ (i₂ : I₂), CategoryTheory.CategoryStruct.comp (c₂.inj i₂) inr = c.inj (Sum.inr i₂)) → CategoryTheory.Mono inr