mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.ext : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {φ ψ : ρ.Equiv σ}, ⇑φ = ⇑ψ → φ = ψ
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.role.fakeClose : Lean.Syntax
-- Mathlib.Analysis.Real.Sqrt
Real.neg_sqrt_lt_of_sq_lt : ∀ {x y : ℝ}, x ^ 2 < y → -√y < x
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- The equivalence of sheaf categories.  -/
CategoryTheory.Equivalence.sheafCongr : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (K : CategoryTheory.GrothendieckTopology D) →
            (e : C ≌ D) →
              (A : Type u₃) →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                  [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] →
                    CategoryTheory.Sheaf J A ≌ CategoryTheory.Sheaf K A
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.comp_right_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.CosimplicialObject.Augmented C}
  (a : X ⟶ Y) (a_1 : Y ⟶ Z) (X_1 : SimplexCategory),
  (CategoryTheory.CategoryStruct.comp a a_1).right.app X_1 =
    CategoryTheory.CategoryStruct.comp (a.right.app X_1) (a_1.right.app X_1)
-- Mathlib.Algebra.Algebra.Tower
Algebra.lsmul_injective : ∀ (R : Type u) (A : Type w) (B : Type u₁) (M : Type v₁) [inst : CommSemiring R] [inst_1 : Semiring A] [IsDomain A]
  [inst_3 : Semiring B] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : AddCommGroup M] [inst_7 : Module R M]
  [inst_8 : Module A M] [inst_9 : Module B M] [inst_10 : IsScalarTower R A M] [inst_11 : IsScalarTower R B M]
  [inst_12 : SMulCommClass A B M] [Module.IsTorsionFree A M] {x : A},
  x ≠ 0 → Function.Injective ⇑((Algebra.lsmul R B M) x)
-- Init.Data.SInt.Lemmas
Int8.toInt32_ofNat' : ∀ {n : ℕ}, ↑n ≤ Int8.maxValue.toInt → (Int8.ofNat n).toInt32 = Int32.ofNat n
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_congr : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {f : α →₀ M}
  {g1 g2 : α → M → N}, (∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) → f.prod g1 = f.prod g2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → {aig : Std.Sat.AIG α} → aig.RefVec w → ℕ → (curr : ℕ) → curr ≤ w → aig.RefVec curr → aig.RefVec w
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b}, curveIntegralFun (ω₁ - ω₂) γ = curveIntegralFun ω₁ γ - curveIntegralFun ω₂ γ
-- Mathlib.Algebra.ContinuedFractions.Basic
ContFract.instInhabited : {α : Type u_1} → [inst : One α] → [inst_1 : Zero α] → [inst_2 : LT α] → Inhabited (ContFract α)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.coe_iInf : ∀ {M : Type u_1} [inst : Add M] {ι : Sort u_3} {S : ι → AddSubsemigroup M}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instCompactlySupportedContinuousMapClass : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β],
  CompactlySupportedContinuousMapClass (CompactlySupportedContinuousMap α β) α β
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
dense_submonoidClosure_iff_subgroupClosure : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] {s : Set G},
  Dense ↑(Submonoid.closure s) ↔ Dense ↑(Subgroup.closure s)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows.hom_idx : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {Y : C} {g : Y ⟶ S} (hf : CategoryTheory.Presieve.ofArrows X f g),
  f hf.idx = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {hc : t.maxKey he ∈ t}, t.getKey (t.maxKey he) hc = t.maxKey he
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedCommSemiring : Inhabited Lean.Meta.Grind.Arith.CommRing.CommSemiring
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.unitOfList_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α], Std.DHashMap.Raw.Const.unitOfList [] = ∅
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_delete : ∀ {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α), (M.delete D₁).delete D₂ = M.delete (D₁ ∪ D₂)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- The angle at the center of a circle equals twice the angle at the circumference, oriented vector
angle form.  -/
Orientation.oangle_eq_two_zsmul_oangle_sub_of_norm_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y z : V},
  x ≠ y → x ≠ z → ‖x‖ = ‖y‖ → ‖x‖ = ‖z‖ → o.oangle y z = 2 • o.oangle (y - x) (z - x)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.addFn? : Lean.Meta.Grind.Arith.CommRing.Semiring → Option Lean.Expr
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α] {f : (a : α) → β a → Option (γ a)}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getEntry? k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      (Std.Internal.List.getEntry? k l).bind fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Qh.IsLocalization (HomotopyCategory.subcategoryAcyclic C).trW
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.HasProp.mk : ∀ {P : TopCat → Prop} {X : Type u} [inst : TopologicalSpace X], P (TopCat.of X) → CompHausLike.HasProp P X
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.ForgetEnrichment.homOf_eId : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] (X : C),
  CategoryTheory.ForgetEnrichment.homOf W (CategoryTheory.eId W X) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of W X)
-- Std.Http.Protocol.H1.Parser
/-- Consumes and ignores empty lines (`CRLF`) that appear before a request-line.

https://httpwg.org/specs/rfc9112.html#rfc.section.2.2:

"In the interest of robustness, a server that is expecting to receive and parse a request-line SHOULD
ignore at least one empty line (CRLF) received prior to the request-line."
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.skipLeadingRequestEmptyLines : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser Unit
-- Init.Control.Option
/-- Converts a computation from the underlying monad into one that could fail, even though it does not.

This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
lifting](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=monad-lifting).
 -/
OptionT.lift : {m : Type u → Type v} → [Monad m] → {α : Type u} → m α → OptionT m α
-- Init.Prelude
/-- Replaces the current value of the mutable state with a new one.
 -/
EStateM.set : {ε σ : Type u} → σ → EStateM ε σ PUnit.{u + 1}
-- Mathlib.Algebra.Lie.Loop
/-- A 2-cocycle on a loop algebra given by an invariant bilinear form.  -/
LieAlgebra.LoopAlgebra.twoCocycleOfBilinear : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : CommRing A] →
              [IsAddTorsionFree R] →
                [Algebra A R] →
                  (Φ : LinearMap.BilinForm R L) →
                    LinearMap.BilinForm.lieInvariant L Φ →
                      Φ.IsSymm →
                        ↥(LieModule.Cohomology.twoCocycle R (LieAlgebra.loopAlgebra R A L)
                            (TrivialLieModule R (LieAlgebra.loopAlgebra R A L) R))
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The infimum distance to `s` and `t` are the same, up to the Hausdorff distance
between `s` and `t`  -/
Metric.infDist_le_infDist_add_hausdorffDist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α},
  Metric.hausdorffEDist s t ≠ ⊤ → Metric.infDist x t ≤ Metric.infDist x s + Metric.hausdorffDist s t
-- Mathlib.Analysis.Normed.Lp.PiLp
LinearIsometryEquiv.piLpCongrLeft_symm : ∀ {p : ENNReal} {𝕜 : Type u_1} {ι : Type u_2} [hp : Fact (1 ≤ p)] [inst : Fintype ι] [inst_1 : Semiring 𝕜]
  {ι' : Type u_5} [inst_2 : Fintype ι'] {E : Type u_6} [inst_3 : SeminormedAddCommGroup E] [inst_4 : Module 𝕜 E]
  (e : ι ≃ ι'), (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e).symm = LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom₂.ofNatTrans.injEq : ∀ {C D : CategoryTheory.Cat} {F G : C ⟶ D} (toNatTrans toNatTrans_1 : F.toFunctor ⟶ G.toFunctor),
  ({ toNatTrans := toNatTrans } = { toNatTrans := toNatTrans_1 }) = (toNatTrans = toNatTrans_1)
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.termB : Lean.ParserDescr
-- Mathlib.Algebra.Order.Ring.Finset
Nat.cast_finsetSup : ∀ {ι : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : OrderBot R] [CanonicallyOrderedAdd R] (s : Finset ι) (f : ι → ℕ), ↑(s.sup f) = s.sup fun i => ↑(f i)
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.add_right_inj : ∀ {M : Type u_1} [inst : AddMonoid M] {a b c : M}, IsAddUnit a → (a + b = a + c ↔ b = c)
-- Mathlib.Topology.Constructions.SumProd
/-- If `Sum.elim f g` is an inducing map, then so is `g`.  -/
Topology.IsInducing.sumElim_right : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, Topology.IsInducing (Sum.elim f g) → Topology.IsInducing g
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.holdsForLocalizationAway : RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
-- Init.Data.String.Basic
String.prev_lt_of_pos : ∀ (s : String) (i : String.Pos.Raw), i ≠ 0 → (String.Pos.Raw.prev s i).byteIdx < i.byteIdx
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
/-- If `s` is finite, the product of the elements of the list `factors C s x`
is the delta function at `x`.  -/
Profinite.NobelingProof.factors_prod_eq_basis : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I)
  (x : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)),
  (Profinite.NobelingProof.factors C s x).prod = Profinite.NobelingProof.spanFinBasis C s x
-- Mathlib.Order.Interval.Set.Monotone
Antitone.Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  Antitone f → Monotone g → Monotone fun x => Set.Ioo (f x) (g x)
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.sup_set_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (N : Submodule R M) (s t : Set S), (s ⊔ t) • N = s • N ⊔ t • N
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- `Fork.ofι ι w` is a limit cone if and only if `Cofork.ofπ ι'.op w'` in the opposite
category is a colimit cocone.  -/
CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y P : C} →
      {f g : X ⟶ Y} →
        (ι ι' : P ⟶ X) →
          (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) →
            (w' : CategoryTheory.CategoryStruct.comp f.op ι'.op = CategoryTheory.CategoryStruct.comp g.op ι'.op) →
              ι = ι' →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι ι w) ≃
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ ι'.op w')
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_monomial_mul : ∀ (R : Type u_1) [inst : Semiring R] (r : R) (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (n : ℕ),
  ((Polynomial.monomial n) r * p).smeval x = r • (x ^ n * p.smeval x)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.mk.congr_simp : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (lift lift_1 : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt) (e_lift : lift = lift_1)
  (fac :
    ∀ (s : CategoryTheory.Limits.Cone F) (j : J), CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j),
  { lift := lift, fac := fac } = { lift := lift_1, fac := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- A `ComponentCompl` specialization of `Quot.lift`, where soundness has to be proved only
for adjacent vertices.
 -/
SimpleGraph.ComponentCompl.lift : {V : Type u} →
  {G : SimpleGraph V} →
    {K : Set V} →
      {β : Sort u_1} →
        (f : ⦃v : V⦄ → v ∉ K → β) →
          (∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw) → G.ComponentCompl K → β
-- Mathlib.Order.CompleteLattice.Defs
le_iSup_iff_forall_lt : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLinearOrder α] {l : α} {f : ι → α}, l ≤ iSup f ↔ ∀ b < l, ∃ i, b < f i
-- Mathlib.Data.EReal.Inv
EReal.div_mul_div_comm : ∀ (a b c d : EReal), a / b * (c / d) = a * c / (b * d)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_arrow' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv
      (CategoryTheory.Limits.imageSubobject f).arrow =
    CategoryTheory.Limits.image.ι f
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.η F))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom h)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom) h
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side.  -/
EuclideanGeometry.tan_oangle_right_mul_dist_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₂ p₃ p₁).tan * dist p₃ p₂ = dist p₁ p₂
-- Init.Data.String.Lemmas.Splits
String.Slice.copy_slice_next : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.endPos}, (s.slice p (p.next h) ⋯).copy = String.singleton (p.get h)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
          k ∈ List.map Sigma.fst l → (m.insertMany l).getKey? k' = some k
-- Mathlib.Order.OrderDual
OrderDual.toDual_ofDual : ∀ {α : Type u_1} (a : αᵒᵈ), OrderDual.toDual (OrderDual.ofDual a) = a
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α},
  Metric.cthickening δ (closure s) = Metric.cthickening δ s
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- The property for `CommShift` structures on `F` and `G` to be compatible with an
adjunction `F ⊣ G`.
 -/
CategoryTheory.Adjunction.CommShift : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              (A : Type u_3) →
                [inst_2 : AddMonoid A] →
                  [inst_3 : CategoryTheory.HasShift C A] →
                    [inst_4 : CategoryTheory.HasShift D A] → [F.CommShift A] → [G.CommShift A] → Prop
-- Mathlib.Order.Bounds.Basic
isLUB_iff_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsLUB s a ↔ ∀ (b : α), a ≤ b ↔ b ∈ upperBounds s
-- Mathlib.Order.RelClasses
Subrelation.isWellFounded : ∀ {α : Type u} (r : α → α → Prop) [IsWellFounded α r] {s : α → α → Prop}, Subrelation s r → IsWellFounded α s
-- Init.Data.Array.Lemmas
Array.all_eq : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, xs.all p = decide (∀ (i : ℕ) (x : i < xs.size), p xs[i] = true)
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_add_right : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α}, (f + g).NeBot → g.NeBot
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Pattern.ctor.injEq : ∀ (ctorName : Lean.Name) (us : List Lean.Level) (params : List Lean.Expr) (fields : List Lean.Meta.Match.Pattern)
  (ctorName_1 : Lean.Name) (us_1 : List Lean.Level) (params_1 : List Lean.Expr)
  (fields_1 : List Lean.Meta.Match.Pattern),
  (Lean.Meta.Match.Pattern.ctor ctorName us params fields =
      Lean.Meta.Match.Pattern.ctor ctorName_1 us_1 params_1 fields_1) =
    (ctorName = ctorName_1 ∧ us = us_1 ∧ params = params_1 ∧ fields = fields_1)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.map_roots_le : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : IsDomain B]
  {p : Polynomial A} {f : A →+* B}, Polynomial.map f p ≠ 0 → Multiset.map (⇑f) p.roots ≤ (Polynomial.map f p).roots
-- Mathlib.Order.Interval.Set.Disjoint
Set.biUnion_Ico_eq_Iio_self_iff : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α},
  ⋃ i, ⋃ (hi : p i), Set.Ico (f i hi) a = Set.Iio a ↔ ∀ x < a, ∃ i, ∃ (hi : p i), f i hi ≤ x
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedOrderRingIso`.

---

The isomorphism of ordered rings between two conditionally complete linearly ordered fields.  -/
LinearOrderedField.inducedOrderRingIso : (β : Type u_3) →
  (γ : Type u_4) →
    [inst : Field β] →
      [inst_1 : ConditionallyCompleteLinearOrder β] →
        [IsStrictOrderedRing β] →
          [inst_3 : Field γ] → [inst_4 : ConditionallyCompleteLinearOrder γ] → [IsStrictOrderedRing γ] → β ≃+*o γ
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.prop_of_mem_aeSeqSet : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α},
  x ∈ aeSeqSet hf p → p x fun n => aeSeq hf p n x
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instOrdOrdinal : Ord Std.Time.Nanosecond.Ordinal
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
CategoryTheory.Limits.weakKernel.lift.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasWeakKernel f] {W : C} (k k_1 : W ⟶ X) (e_k : k = k_1)
  (h : CategoryTheory.CategoryStruct.comp k f = 0),
  CategoryTheory.Limits.weakKernel.lift f k h = CategoryTheory.Limits.weakKernel.lift f k_1 ⋯
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- Constructor for functors to the category of triangles.  -/
CategoryTheory.Pretriangulated.Triangle.functorMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
          {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} →
            (obj₁ ⟶ obj₂) →
              (obj₂ ⟶ obj₃) →
                (obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) →
                  CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.Topology.UniformSpace.Cauchy
TotallyBounded.isCompact_of_isClosed : ∀ {α : Type u} [uniformSpace : UniformSpace α] [CompleteSpace α] {s : Set α},
  TotallyBounded s → IsClosed s → IsCompact s
-- Init.Data.List.Attach
List.filter_unattach : ∀ {α : Type u_1} {P : α → Prop} {xs : List (Subtype P)} {f : α → Bool},
  List.filter f xs.unattach =
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
        xs).unattach
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFn_zero : ∀ {α : Type u_3} (E : α → Type u_4) (p : ENNReal) [inst : (i : α) → NormedAddCommGroup (E i)], ↑0 = 0
-- Mathlib.RingTheory.MvPolynomial.Expand
MvPolynomial.map_iterateFrobenius_expand : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (p : ℕ) [inst_1 : ExpChar R p] (f : MvPolynomial σ R) (n : ℕ),
  (MvPolynomial.map (iterateFrobenius R p n)) ((MvPolynomial.expand (p ^ n)) f) = f ^ p ^ n
-- Init.Data.Vector.InsertIdx
Vector.insertIdx_comm : ∀ {α : Type u} {n : ℕ} (a b : α) {i j : ℕ} {xs : Vector α n} (x : i ≤ j) (x_1 : j ≤ n),
  (xs.insertIdx i a ⋯).insertIdx (j + 1) b ⋯ = (xs.insertIdx j b x_1).insertIdx i a ⋯
-- Mathlib.Data.Set.Operations
/-- **Alias** of `Set.mem_sdiff`. -/
Set.mem_diff : ∀ {α : Type u} {s t : Set α} (x : α), x ∈ s \ t ↔ x ∈ s ∧ x ∉ t
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- the index type of the coverings of the fibre products  -/
CategoryTheory.Functor.PreOneHypercoverDenseData.I₁ : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {S : C} → (self : F.PreOneHypercoverDenseData S) → self.I₀ → self.I₀ → Type w
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.map_floor : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {S : Type u_3}
  [inst_3 : Semiring S] [inst_4 : LinearOrder S] [inst_5 : FloorSemiring S] {F : Type u_4} [inst_6 : FunLike F R S]
  [RingHomClass F R S] [IsStrictOrderedRing R] [IsStrictOrderedRing S] (f : F), StrictMono ⇑f → ∀ (a : R), ⌊f a⌋₊ = ⌊a⌋₊