mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Covering.Basic
Bundle.Trivialization.mk.congr_simp : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace Z] {proj : Z → B}
  (toOpenPartialHomeomorph toOpenPartialHomeomorph_1 : OpenPartialHomeomorph Z (B × F))
  (e_toOpenPartialHomeomorph : toOpenPartialHomeomorph = toOpenPartialHomeomorph_1) (baseSet baseSet_1 : Set B)
  (e_baseSet : baseSet = baseSet_1) (open_baseSet : IsOpen baseSet)
  (source_eq : toOpenPartialHomeomorph.source = proj ⁻¹' baseSet)
  (target_eq : toOpenPartialHomeomorph.target = baseSet ×ˢ Set.univ)
  (proj_toFun : ∀ p ∈ toOpenPartialHomeomorph.source, (↑toOpenPartialHomeomorph p).1 = proj p),
  { toOpenPartialHomeomorph := toOpenPartialHomeomorph, baseSet := baseSet, open_baseSet := open_baseSet,
      source_eq := source_eq, target_eq := target_eq, proj_toFun := proj_toFun } =
    { toOpenPartialHomeomorph := toOpenPartialHomeomorph_1, baseSet := baseSet_1, open_baseSet := ⋯, source_eq := ⋯,
      target_eq := ⋯, proj_toFun := ⋯ }
-- Mathlib.Order.Filter.Basic
Filter.inhabitedMem : {α : Type u} → {f : Filter α} → Inhabited { s // s ∈ f }
-- Mathlib.Data.Nat.Squarefree
Nat.MinSqFacProp.eq_1 : ∀ (n : ℕ), n.MinSqFacProp none = Squarefree n
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.add : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    {F : CategoryTheory.Functor J RingCat} →
      RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instNontrivial : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) [Nontrivial R], Nontrivial (WithAbs v)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.id.inj : ∀ {e : Lean.Expr} {a : Mathlib.Tactic.BicategoryLike.Obj} {e_1 : Lean.Expr} {a_1 : Mathlib.Tactic.BicategoryLike.Obj},
  Mathlib.Tactic.BicategoryLike.Mor₁.id e a = Mathlib.Tactic.BicategoryLike.Mor₁.id e_1 a_1 → e = e_1 ∧ a = a_1
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the largest key that is less than or equal to the
given key, panicking if no such key exists.
 -/
Std.ExtTreeMap.getKeyLE! : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeMap α β cmp → α → α
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopFunctor_additive : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Preadditive V], (HomologicalComplex.unopFunctor V c).Additive
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertListIfNewUnit_of_contains : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α}
  {k : α},
  Std.Internal.List.containsKey k l = true →
    Std.Internal.List.getKey! k (Std.Internal.List.insertListIfNewUnit l toInsert) = Std.Internal.List.getKey! k l
-- Init.Data.Array.Lemmas
Array.forall_getElem : ∀ {α : Type u_1} {xs : Array α} {p : α → Prop}, (∀ (i : ℕ) (h : i < xs.size), p xs[i]) ↔ ∀ a ∈ xs, p a
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.covering_mem : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s) {p : X × Set X},
  p ∈ h.index → h.covering p ∈ f p.1
-- Mathlib.Data.List.Rotate
List.isRotated_nil_iff : ∀ {α : Type u} {l : List α}, l ~r [] ↔ l = []
-- Mathlib.Logic.Equiv.Defs
Equiv.le_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : LE β] (a b : α), e a ≤ e b ↔ a ≤ b
-- Mathlib.FieldTheory.SeparableDegree
/-- Same as `Polynomial.natSepDegree_eq_natDegree_of_separable`, but enables the use of
dot notation.  -/
Polynomial.Separable.natSepDegree_eq_natDegree : ∀ {F : Type u} [inst : Field F] {f : Polynomial F}, f.Separable → f.natSepDegree = f.natDegree
-- Mathlib.Algebra.Homology.ExactSequence
/-- Functoriality maps for `ComposableArrows.sc`.  -/
CategoryTheory.ComposableArrows.scMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        {S₁ S₂ : CategoryTheory.ComposableArrows C n} →
          (S₁ ⟶ S₂) →
            (h₁ : S₁.IsComplex) →
              (h₂ : S₂.IsComplex) →
                (i : ℕ) →
                  (hi : autoParam (i + 2 ≤ n) CategoryTheory.ComposableArrows.scMap._auto_1) →
                    S₁.sc h₁ i hi ⟶ S₂.sc h₂ i hi
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_sup : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S₁ S₂ : Subsemiring Rᵐᵒᵖ), (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_neg : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Neg α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s : Finset α) (f : α → β), (-s).sup f = s.sup fun x => f (-x)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- Change the endpoints of a walk using equalities. This is helpful for relaxing
definitional equality constraints and to be able to state otherwise difficult-to-state
lemmas. While this is a simple wrapper around `Eq.rec`, it gives a canonical way to write it.

The simp-normal form is for the `copy` to be pushed outward. That way calculations can
occur within the "copy context."  -/
SimpleGraph.Walk.copy : {V : Type u} → {G : SimpleGraph V} → {u v u' v' : V} → G.Walk u v → u = u' → v = v' → G.Walk u' v'
-- Mathlib.Order.Ideal
Order.Ideal.coe_sInf : ∀ {P : Type u_1} [inst : SemilatticeSup P] [inst_1 : OrderBot P] {S : Set (Order.Ideal P)}, ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.Algebra.Lie.Weights.Cartan
LieModule.Weight.congr_simp : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L], LieModule.Weight R L M = LieModule.Weight R L M
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.hoFunctor.preservesTerminal : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty SSet) SSet.hoFunctor
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.mk.sizeOf_spec : ∀ (textDocumentSync? : Option Lean.Lsp.TextDocumentSyncOptions)
  (completionProvider? : Option Lean.Lsp.CompletionOptions)
  (hoverProvider documentHighlightProvider documentSymbolProvider definitionProvider declarationProvider
    typeDefinitionProvider referencesProvider callHierarchyProvider : Bool)
  (renameProvider? : Option Lean.Lsp.RenameOptions) (workspaceSymbolProvider foldingRangeProvider : Bool)
  (semanticTokensProvider? : Option Lean.Lsp.SemanticTokensOptions)
  (codeActionProvider? : Option Lean.Lsp.CodeActionOptions) (inlayHintProvider? : Option Lean.Lsp.InlayHintOptions)
  (signatureHelpProvider? : Option Lean.Lsp.SignatureHelpOptions)
  (colorProvider? : Option Lean.Lsp.DocumentColorOptions) (experimental? : Option Lean.Lsp.LeanServerCapabilities),
  sizeOf
      { textDocumentSync? := textDocumentSync?, completionProvider? := completionProvider?,
        hoverProvider := hoverProvider, documentHighlightProvider := documentHighlightProvider,
        documentSymbolProvider := documentSymbolProvider, definitionProvider := definitionProvider,
        declarationProvider := declarationProvider, typeDefinitionProvider := typeDefinitionProvider,
        referencesProvider := referencesProvider, callHierarchyProvider := callHierarchyProvider,
        renameProvider? := renameProvider?, workspaceSymbolProvider := workspaceSymbolProvider,
        foldingRangeProvider := foldingRangeProvider, semanticTokensProvider? := semanticTokensProvider?,
        codeActionProvider? := codeActionProvider?, inlayHintProvider? := inlayHintProvider?,
        signatureHelpProvider? := signatureHelpProvider?, colorProvider? := colorProvider?,
        experimental? := experimental? } =
    1 + sizeOf textDocumentSync? + sizeOf completionProvider? + sizeOf hoverProvider +
                                    sizeOf documentHighlightProvider +
                                  sizeOf documentSymbolProvider +
                                sizeOf definitionProvider +
                              sizeOf declarationProvider +
                            sizeOf typeDefinitionProvider +
                          sizeOf referencesProvider +
                        sizeOf callHierarchyProvider +
                      sizeOf renameProvider? +
                    sizeOf workspaceSymbolProvider +
                  sizeOf foldingRangeProvider +
                sizeOf semanticTokensProvider? +
              sizeOf codeActionProvider? +
            sizeOf inlayHintProvider? +
          sizeOf signatureHelpProvider? +
        sizeOf colorProvider? +
      sizeOf experimental?
-- Mathlib.Algebra.CharP.LinearMaps
/-- For a commutative semiring `R` and an `R`-module `M`, if `M` contains an
element `x` that is not torsion, then the characteristic of `R` is equal to the
characteristic of the `R`-linear endomorphisms of `M`.  -/
Module.charP_end : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : ℕ}
  [hchar : CharP R p], (∃ x, Ideal.torsionOf R M x = ⊥) → CharP (M →ₗ[R] M) p
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.zero_toSimpleFunc : ∀ {α : Type u_1} (E : Type u_4) [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  (μ : MeasureTheory.Measure α), ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc 0) =ᵐ[μ] 0
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.repr_symm_single : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : DecidableEq ι] (b : HilbertBasis ι 𝕜 E) (i : ι),
  b.repr.symm (lp.single 2 i 1) = b i
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.dual.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β],
  sInfHom.dual =
    { toFun := fun f => { toFun := ⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual, map_sSup' := ⋯ },
      invFun := fun f => { toFun := ⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual, map_sInf' := ⋯ }, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.Data.Bool.Count
List.IsChain.count_false_le_count_true_add_one : ∀ {l : List Bool}, List.IsChain (fun x1 x2 => x1 ≠ x2) l → List.count false l ≤ List.count true l + 1
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- A variant of `LeftExtension.precomp` where we precompose, and then
"whisker" the diagram by a given natural transformation `(α : F₀ ⟶ L ⋙ F₁)`  -/
CategoryTheory.Functor.LeftExtension.precomp₂ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {F₀ : CategoryTheory.Functor C H} →
                  {L : CategoryTheory.Functor C D} →
                    {F₁ : CategoryTheory.Functor D H} →
                      (L' : CategoryTheory.Functor D D') →
                        (F₀ ⟶ L.comp F₁) → CategoryTheory.Functor (L'.LeftExtension F₁) ((L.comp L').LeftExtension F₀)
-- Mathlib.Algebra.Homology.CochainComplexOpposite
/-- The equivalence of categories `ChainComplex C ℤ ≌ CochainComplex C ℤ`.  -/
ChainComplex.cochainComplexEquivalence : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → ChainComplex C ℤ ≌ CochainComplex C ℤ
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.brecOn_1.eq : ∀ {motive_1 : Lean.Lsp.Ipc.ModuleHierarchy → Sort u} {motive_2 : Array Lean.Lsp.Ipc.ModuleHierarchy → Sort u}
  {motive_3 : List Lean.Lsp.Ipc.ModuleHierarchy → Sort u} (t : Array Lean.Lsp.Ipc.ModuleHierarchy)
  (F_1 : (t : Lean.Lsp.Ipc.ModuleHierarchy) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.Lsp.Ipc.ModuleHierarchy) → Lean.Lsp.Ipc.ModuleHierarchy.below_2 t → motive_3 t),
  Lean.Lsp.Ipc.ModuleHierarchy.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.Lsp.Ipc.ModuleHierarchy.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_of_lt_of_le_of_nonneg_of_pos : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α]
  [MulPosStrictMono α], a < b → c ≤ d → 0 ≤ a → 0 < d → a * c < b * d
-- Mathlib.MeasureTheory.Covering.LiminfLimsup
/-- Given a sequence of subsets `sᵢ` of a metric space, together with a sequence of radii `rᵢ`
such that `rᵢ → 0`, the set of points which belong to infinitely many of the
`rᵢ`-thickenings of `sᵢ` is unchanged almost everywhere for a uniformly locally doubling measure if
the `rᵢ` are all scaled by a positive constant.

This lemma is a generalisation of Lemma 9 appearing on page 217 of
[J.W.S. Cassels, *Some metrical theorems in Diophantine approximation. I*](cassels1950).

See also `blimsup_cthickening_mul_ae_eq`.

NB: The `: Set α` type ascription is present because of
https://github.com/leanprover-community/mathlib/issues/16932.  -/
blimsup_thickening_mul_ae_eq : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α] [BorelSpace α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ] [IsUnifLocDoublingMeasure μ] (p : ℕ → Prop)
  (s : ℕ → Set α) {M : ℝ},
  0 < M →
    ∀ (r : ℕ → ℝ),
      Filter.Tendsto r Filter.atTop (nhds 0) →
        Filter.blimsup (fun i => Metric.thickening (M * r i) (s i)) Filter.atTop p =ᵐ[μ]
          Filter.blimsup (fun i => Metric.thickening (r i) (s i)) Filter.atTop p
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instSub : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → Sub (DoubleCentralizer 𝕜 A)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.associator_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H I : CategoryTheory.OplaxFunctor B C} (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) (a : B),
  (CategoryTheory.Oplax.OplaxTrans.associator η θ ι).hom.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPPiBinderNames : Lean.Options → Bool
-- Mathlib.Algebra.Group.Subgroup.Map
/-- An additive subgroup is isomorphic to its image under an injective function. If you
have an isomorphism, use `AddEquiv.addSubgroupMap` for better definitional equalities.  -/
AddSubgroup.equivMapOfInjective : {G : Type u_1} →
  [inst : AddGroup G] →
    {N : Type u_5} →
      [inst_1 : AddGroup N] → (H : AddSubgroup G) → (f : G →+ N) → Function.Injective ⇑f → ↥H ≃+ ↥(AddSubgroup.map f H)
-- Mathlib.Probability.Moments.SubGaussian
/-- A random variable `X` has a sub-Gaussian moment-generating function with parameter `c`
with respect to a kernel `κ` and a measure `ν` if for `ν`-almost all `ω'`, for all `t : ℝ`,
the moment-generating function of `X` with respect to `κ ω'` is bounded by `exp (c * t ^ 2 / 2)`.
This implies in particular that `X` has expectation 0.  -/
ProbabilityTheory.Kernel.HasSubgaussianMGF : {Ω : Type u_1} →
  {Ω' : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      {mΩ' : MeasurableSpace Ω'} →
        (Ω → ℝ) →
          NNReal →
            ProbabilityTheory.Kernel Ω' Ω →
              autoParam (MeasureTheory.Measure Ω') ProbabilityTheory.Kernel.HasSubgaussianMGF._auto_1 → Prop
-- Mathlib.CategoryTheory.Discrete.Basic
/-- For functors out of a discrete category,
a natural isomorphism is just a collection of isomorphisms,
as the naturality squares are trivial.
 -/
CategoryTheory.Discrete.natIso : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {I : Type u₁} →
      {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} →
        ((i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i) → (F ≅ G)
-- Lean.Environment
Lean.ImportM.Context.mk.inj : ∀ {env : Lean.Environment} {opts : Lean.Options} {env_1 : Lean.Environment} {opts_1 : Lean.Options},
  { env := env, opts := opts } = { env := env_1, opts := opts_1 } → env = env_1 ∧ opts = opts_1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_blastDivSubtractShift_r : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (assign : α → Bool)
  (lhs rhs : BitVec w) (n d : aig.RefVec w) (wn wr : ℕ) (q r : aig.RefVec w) (qbv rbv : BitVec w),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
      (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
        ∀ (idx : ℕ) (hidx : idx < w),
          ⟦assign,
              { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig,
                ref :=
                  (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).r.get idx
                    hidx }⟧ =
            (BitVec.divSubtractShift { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).r.getLsbD idx
-- Mathlib.FieldTheory.SeparableClosure
Field.finInsepDegree_top_le_finInsepDegree_of_isScalarTower : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Module.Finite F K],
  Field.finInsepDegree E K ≤ Field.finInsepDegree F K
-- Mathlib.Order.MinMax
AntitoneOn.map_min : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α} {a b : α},
  AntitoneOn f s → a ∈ s → b ∈ s → f (min a b) = max (f a) (f b)
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
/-- Right division by a nonzero element in a `GroupWithZero` is a permutation of the
underlying type.  -/
Equiv.divRight₀ : {G₀ : Type u_1} → [inst : GroupWithZero G₀] → (a : G₀) → a ≠ 0 → Equiv.Perm G₀
-- Init.Prelude
Applicative.toSeq : {f : Type u → Type v} → [self : Applicative f] → Seq f
-- Mathlib.Algebra.CubicDiscriminant
Cubic.discr_ne_zero_iff_roots_nodup : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K},
  P.a ≠ 0 → (Polynomial.map φ P.toPoly).Splits → (P.discr ≠ 0 ↔ (Cubic.map φ P).roots.Nodup)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.monotone_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N}, Monotone (AddSubsemigroup.comap f)
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qParam_tendsto_atImInfty : ∀ {h : ℝ}, 0 < h → Filter.Tendsto (fun τ => Function.Periodic.qParam h ↑τ) UpperHalfPlane.atImInfty (nhds 0)
-- Mathlib.Data.List.Basic
List.or_exists_of_exists_mem_cons : ∀ {α : Type u} {p : α → Prop} {a : α} {l : List α}, (∃ x ∈ a :: l, p x) → p a ∨ ∃ x ∈ l, p x
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.precomp_map_left : ∀ {C : Type u_1} {C' : Type u_2} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C'] [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor C' C)
  {X Y :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D H).obj L) (CategoryTheory.Functor.fromPUnit F)}
  (φ : X ⟶ Y), ((CategoryTheory.Functor.RightExtension.precomp L F G).map φ).left = φ.left
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.mk_hom : ∀ {S : AlgebraicGeometry.Scheme} {R : CommRingCat} (f : AlgebraicGeometry.Spec R ⟶ S)
  [inst : AlgebraicGeometry.Etale f], (AlgebraicGeometry.Scheme.AffineEtale.mk f).hom = f
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_1.congr_eq_3 : ∀ {n : ℕ} (motive : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → Sort u_1)
  (x : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (h_1 : Unit → motive none)
  (h_2 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, true)))
  (h_3 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, false)))
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n),
  x = some (l, false) →
    (match x with
      | none => h_1 ()
      | some (l, true) => h_2 l
      | some (l, false) => h_3 l) ≍
      h_3 l
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Lax unity.  -/
CategoryTheory.Lax.LaxTrans.naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.LaxTrans F G) (a : B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a))
      (self.naturality (CategoryTheory.CategoryStruct.id a)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).inv
        (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)))
-- Mathlib.Data.Prod.Basic
Prod.mk_left_injective : ∀ {α : Type u_5} {β : Type u_6} (b : β), Function.Injective fun a => (a, b)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.any_eq_false_iff_forall_contains_get : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {p : (a : α) → β a → Bool}, m.WF → (m.any p = false ↔ ∀ (a : α) (h : m.contains a = true), p a (m.get a h) = false)
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_left_injective : ∀ {α : Type u_1} (a : α), Function.Injective fun x => Multiset.replicate x a
-- Mathlib.Data.Multiset.Defs
Multiset.lift_coe : ∀ {α : Type u_3} {β : Type u_4} (x : List α) (f : List α → β) (h : ∀ (a b : List α), a ≈ b → f a = f b),
  Quotient.lift f h ↑x = f x
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k k' : α}, (k == k') = true → m.get? k = m.get? k'
-- Mathlib.Data.Option.NAry
Option.map_map₂_distrib : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
  {α' : Type u_5} {β' : Type u_6} {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) →
    Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g₁ a) (Option.map g₂ b)
-- Mathlib.ModelTheory.Quotients
/-- A prestructure is a first-order structure with a `Setoid` equivalence relation on it,
such that quotienting by that equivalence relation is still a structure.  -/
FirstOrder.Language.Prestructure : FirstOrder.Language → {M : Type u_1} → Setoid M → Type (max (max u_1 u_2) u_3)
-- Mathlib.Data.TwoPointing
TwoPointing.swap_snd : ∀ {α : Type u_1} (p : TwoPointing α), p.swap.toProd.2 = p.toProd.1
-- Mathlib.CategoryTheory.Abelian.Images
/-- There is a canonical monomorphism `i : coimage f ⟶ Q`.  -/
CategoryTheory.Abelian.factorThruCoimage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (f : P ⟶ Q) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] →
              CategoryTheory.Abelian.coimage f ⟶ Q