mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Given a function `m : Set X → ℝ≥0∞`, `mkMetric' m` is the supremum of `μ r`
over `r > 0`, where `μ r` is the maximal outer measure `μ` such that `μ s ≤ m s`
for all `s`. While each `μ r` is an *outer* measure, the supremum is a measure.  -/
MeasureTheory.Measure.mkMetric' : {X : Type u_2} →
  [inst : EMetricSpace X] → [inst_1 : MeasurableSpace X] → [BorelSpace X] → (Set X → ENNReal) → MeasureTheory.Measure X
-- Init.Data.SInt.Bitwise
ISize.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : ISize}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Mathlib.RingTheory.RingHomProperties
/-- A property `RespectsIso` if it still holds when composed with an isomorphism  -/
RingHom.RespectsIso : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_subset_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s₁ s₂ t₁ t₂ : Finset β},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂
-- Mathlib.Algebra.CharP.MixedCharZero
/-- Split any `Prop` over `R` into the three cases:
- positive characteristic.
- equal characteristic zero.
- mixed characteristic `(0, p)`.
 -/
split_by_characteristic : ∀ (R : Type u_1) [inst : CommRing R] {P : Prop},
  (∀ (p : ℕ), p ≠ 0 → CharP R p → P) → (∀ (a : Algebra ℚ R), P) → (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → P
-- Mathlib.Analysis.RCLike.Extend
Module.Dual.extendRCLike.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : AddCommGroup F] [inst_2 : Module ℝ F] [inst_3 : Module 𝕜 F]
  [inst_4 : IsScalarTower ℝ 𝕜 F] (fr fr_1 : Module.Dual ℝ F), fr = fr_1 → fr.extendRCLike = fr_1.extendRCLike
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Equivalence.mapAction_inverse : ∀ {V : Type u_2} {W : Type u_3} [inst : CategoryTheory.Category.{v_2, u_2} V]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} W] (G : Type u_4) [inst_2 : Monoid G] (E : V ≌ W),
  (CategoryTheory.Equivalence.mapAction G E).inverse = E.inverse.mapAction G
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_symm_add : ∀ {A : Type u_3} {E : Type u_4} (x' y' : E) [inst : AddCommGroup E],
  (WithCStarModule.equiv A E).symm (x' + y') = (WithCStarModule.equiv A E).symm x' + (WithCStarModule.equiv A E).symm y'
-- Mathlib.Data.Matrix.Block
/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
"top left" submatrix.  -/
Matrix.toBlocks₁₁ : {l : Type u_1} →
  {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type u_12} → Matrix (n ⊕ o) (l ⊕ m) α → Matrix n l α
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.succeeded.sizeOf_spec : ∀ (goal : Lean.MVarId) (steps? : Option (Array Aesop.Script.LazyStep)),
  sizeOf (Aesop.NormRuleResult.succeeded goal steps?) = 1 + sizeOf goal + sizeOf steps?
-- Mathlib.Algebra.Group.Basic
eq_of_zero_sub_eq_zero_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, 0 - a = 0 - b → a = b
-- Init.Internal.Order.Basic
Lean.Order.iterates.below : {α : Sort u} →
  [inst : Lean.Order.CCPO α] →
    {f : α → α} → {motive : (a : α) → Lean.Order.iterates f a → Prop} → {a : α} → Lean.Order.iterates f a → Prop
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- An auxiliary definition for `mkOfAdjointifyCounit`.  -/
CategoryTheory.Bicategory.adjointifyCounit : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        {g : b ⟶ a} →
          (CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g) →
            (CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b) →
              (CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b)
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.extendIso`.

---

A cone extended by an isomorphism is isomorphic to the original cone.  -/
CategoryTheory.Limits.Cones.extendIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cone F) → {X : C} → (f : s.pt ≅ X) → s ≅ s.extend f.inv
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.stalkAlgebra : (R : Type u) →
  [inst : CommRing R] → (p : PrimeSpectrum R) → Algebra R ↑((AlgebraicGeometry.Spec.structureSheaf R).presheaf.stalk p)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_add : ∀ {a b : ISize} (h : System.Platform.numBits = 32), (a + b).toBitVec32 h = a.toBitVec32 h + b.toBitVec32 h
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instCoeMonCat.eq_1 : AddCommMonCat.instCoeMonCat = { coe := (CategoryTheory.forget₂ AddCommMonCat AddMonCat).obj }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.equiv_hom_hom_apply_snd : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Cone.equiv F).hom) c).snd = c.π
-- Init.Data.List.Sublist
List.IsInfix.length_le : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.length ≤ l₂.length
-- Mathlib.LinearAlgebra.Dimension.Torsion.Finite
/-- A torsion module has rank zero.  -/
Module.IsTorsion.rank_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R],
  Module.IsTorsion R M → Module.rank R M = 0
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.congr' : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c₁ c₂ : ℝ} {l : Filter α}
  {f₁ f₂ : α → E} {g₁ g₂ : α → F},
  Asymptotics.IsBigOWith c₁ l f₁ g₁ → c₁ = c₂ → f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → Asymptotics.IsBigOWith c₂ l f₂ g₂
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsStableUnderComposition.sInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : Set (CategoryTheory.MorphismProperty C)},
  (∀ W' ∈ W, W'.IsStableUnderComposition) → (sInf W).IsStableUnderComposition
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.rangeRestrictField_bijective : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L),
  Function.Bijective ⇑f.rangeRestrictField
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_update_update : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M)
  [inst_5 : DecidableEq ι] {i j : ι}, i ≠ j → ∀ (m : M), f (Function.update (Function.update v i m) j m) = 0
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_image_ofColex_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  StrictMono f → StrictMono fun s => toColex (Finset.image f (ofColex s))
-- Mathlib.Topology.EMetricSpace.Defs
/-- `EMetric.ball x ε` is the set of all points `y` with `edist y x < ε`  -/
Metric.eball : {α : Type u} → [EDist α] → α → ENNReal → Set α
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `*` is a commutative semigroup, if it admits an injective map that
preserves `*` to a commutative semigroup.  See note [reducible non-instances].  -/
Function.Injective.commSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : CommSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → CommSemigroup M₁
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_addNatEmb_Ico : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Finset.map (Fin.addNatEmb m) (Finset.Ico i j) = Finset.Ico (i.addNat m) (j.addNat m)
-- Mathlib.Order.BooleanAlgebra.Basic
le_sdiff : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If M is the midpoint of the segment AB and C is the same distance from A as it is from B
then ∠CMA = π / 2.  -/
EuclideanGeometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  dist p₃ p₁ = dist p₃ p₂ → EuclideanGeometry.angle p₃ (midpoint ℝ p₁ p₂) p₁ = Real.pi / 2
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_hom_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).hom.app X_1).fst.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.fst.obj X_2)
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- If a set has the unique differential property, then its image under a local
diffeomorphism also has the unique differential property.  -/
UniqueMDiffOn.uniqueMDiffOn_preimage : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set M},
  UniqueMDiff[s] →
    ∀ {e : OpenPartialHomeomorph M M'},
      OpenPartialHomeomorph.MDifferentiable I I' e → UniqueMDiff[e.target ∩ ↑e.symm ⁻¹' s]
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.brecOn.go : {pu : Lean.Compiler.LCNF.Purity} →
  {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u} →
    {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} →
      {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u} →
        {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} →
          {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u} →
            {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} →
              (t : Lean.Compiler.LCNF.Code pu) →
                ((t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t) →
                  ((t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t) →
                    ((t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t) →
                      ((t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t) →
                        ((t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t) →
                          ((t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t) →
                            motive_4 t ×' t.below
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.toCircle.eq_1 : ∀ {N : ℕ} [inst : NeZero N], ZMod.toCircle = AddCircle.toCircle_addChar.compAddMonoidHom ZMod.toAddCircle
-- Std.Sync.StreamMap
/-- Wait for the first value inside of the stream map.
 -/
Std.StreamMap.recv : {α β : Type} → Std.StreamMap α β → Std.Async.Async (α × β)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_neg : ∀ (x : ℝ), Real.arctan (-x) = -Real.arctan x
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.unopSymm_d : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex Vᵒᵖ c.symm) (i j : ι),
  X.unopSymm.d i j = (X.d j i).unop
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_bot : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P : l}, Lean.Order.join P Lean.Order.bot = P
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instNonUnitalCommSemiring : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [NonUnitalCommSemiring R] → NonUnitalCommSemiring (l.Germ R)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.trans_assoc : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃),
  ((p.trans q).trans r).Homotopic (p.trans (q.trans r))
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.card_mul_mulConst : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G), ↑A.card * A.mulConst B = ↑(A * B).card
-- Init.Data.SInt.Bitwise
Int16.toBitVec_xor : ∀ (a b : Int16), (a ^^^ b).toBitVec = a.toBitVec ^^^ b.toBitVec
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.surjOn_iff_le_map : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H : Subgroup G} {K : Subgroup N},
  Set.SurjOn ⇑f ↑H ↑K ↔ K ≤ Subgroup.map f H
-- Mathlib.Algebra.Lie.Loop
/-- A loop algebra is the base change of a Lie algebra `L` over `R` by `R[z,z⁻¹]`. We make a
slightly more general definition which coincides with the Laurent polynomial construction when
`A = ℤ`  -/
LieAlgebra.loopAlgebra : (R : Type u_1) →
  Type u_2 →
    (L : Type u_3) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Type (max (max u_2 u_1) u_3)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_eq_sum_primesLE : ∀ (x : ℝ), Chebyshev.theta x = ∑ p ∈ ⌊x⌋₊.primesLE, Real.log ↑p
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.Functor.mapShortComplex_map_τ₁ : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y),
  (F.mapShortComplex.map φ).τ₁ = F.map φ.τ₁
-- Mathlib.Topology.Category.TopPair
TopPair.incl_map : ∀ {X Y : TopCat} (f : X ⟶ Y), TopPair.incl.map f = TopPair.ofHom f (CategoryTheory.CategoryStruct.id TopPair.snd) ⋯
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Iso.retract_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y), e.retract.i = e.hom
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.add_add : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {c₁ c₂ : ℝ} {l : Filter α} {f₁ f₂ : α → E'}
  {g₁ g₂ : α → ℝ},
  Asymptotics.IsBigOWith c₁ l f₁ g₁ →
    Asymptotics.IsBigOWith c₂ l f₂ g₂ →
      Asymptotics.IsBigOWith (max c₁ c₂) l (fun x => f₁ x + f₂ x) fun x => ‖g₁ x‖ + ‖g₂ x‖
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.doSeqToCode : List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_of_zero_length : ∀ {w i : ℕ}, w = 0 → ∀ (x : BitVec w), x.getMsbD i = false
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.add_eq_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.AddMonObj.add =
    CategoryTheory.SemiCartesianMonoidalCategory.fst M M + CategoryTheory.SemiCartesianMonoidalCategory.snd M M
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.reindex_over : ∀ {n m : Type u} (i : m → n) (S : AlgebraicGeometry.Scheme),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex i S)
      (AlgebraicGeometry.AffineSpace m S ↘ S) =
    AlgebraicGeometry.AffineSpace n S ↘ S
-- Mathlib.Combinatorics.Matroid.Basic
/-- For any bases `B`, `B'` and `e ∈ B \ B'`, there is some `f ∈ B' \ B` for which `B-e+f`
is a base.  -/
Matroid.isBase_exchange : ∀ {α : Type u_1} (self : Matroid α), Matroid.ExchangeProperty self.IsBase
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.isClosed : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : TopologicalSpace.Closeds α), IsClosed ↑s
-- Mathlib.LinearAlgebra.RootSystem.RootPairingCat
RootPairingCat.weightIsAddCommGroup : {R : Type u} → [inst : CommRing R] → (self : RootPairingCat R) → AddCommGroup self.weight
-- Mathlib.Topology.Separation.Basic
isOpen_ne : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x : X}, IsOpen {y | y ≠ x}
-- Mathlib.Data.Sym.Basic
Sym.mem_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {b : β} {l : Sym α n}, b ∈ Sym.map f l ↔ ∃ a ∈ l, f a = b
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.coe_equiv_snd_eq_one_iff_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G},
  1 ∈ T → (↑(hST.equiv g).2 = 1 ↔ g ∈ S)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.op_le_iff : ∀ {G : Type u_2} [inst : AddGroup G] {S₁ : AddSubgroup G} {S₂ : AddSubgroup Gᵃᵒᵖ}, S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk_eq_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (s : ↥S) (m : M),
  LocalizedModule.mk m s = IsLocalizedModule.mk' (LocalizedModule.mkLinearMap S M) m s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.two_mul_arctan_add_pi : ∀ {x : ℝ}, 1 < x → 2 * Real.arctan x = Real.arctan (2 * x / (1 - x ^ 2)) + Real.pi
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : AlgebraicGeometry.Flat f]
  [hg : AlgebraicGeometry.Flat g], AlgebraicGeometry.Flat (CategoryTheory.CategoryStruct.comp f g)
-- Std.Http.Data.Body.Empty
/-- Receives from an empty body, always returning end-of-stream.
 -/
Std.Http.Body.Empty.recv : Std.Http.Body.Empty → Std.Async.Async (Option Std.Http.Chunk)
-- Init.Data.UInt.Lemmas
USize.toFin_div : ∀ (a b : USize), (a / b).toFin = a.toFin / b.toFin
-- Mathlib.CategoryTheory.Limits.FintypeCat
/-- Help typeclass inference to infer creation of finite limits for the forgetful functor.  -/
CategoryTheory.Limits.FintypeCat.instCreatesLimitsOfShapeFintypeCatForgetFunObjFiniteOfFinCategory : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget FintypeCat)
-- Mathlib.CategoryTheory.Action.Monoidal
Action.β_hom_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] [inst_3 : CategoryTheory.BraidedCategory V] {X Y : Action V G},
  (β_ X Y).hom.hom = (β_ X.V Y.V).hom
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulMono.to_covariantClass_nonneg_mul_le : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [PosMulMono α],
  CovariantClass { x // 0 ≤ x } α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.mk : Lean.Name → ℕ → ℕ → ℕ → ℕ → Lean.Compiler.LCNF.CtorInfo
-- Mathlib.Order.Basic
Std.Refl.compl : ∀ {α : Type u_2} (r : α → α → Prop) [Std.Refl r], Std.Irrefl rᶜ
-- Mathlib.Topology.MetricSpace.ProperSpace
/-- In a proper pseudometric space, any closed ball is a `CompactSpace` when considered as a
subtype.  -/
instCompactSpaceElemClosedBallOfProperSpace : ∀ {α : Type u_3} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ), CompactSpace ↑(Metric.closedBall x r)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.isMulCommutative_iSup : ∀ {R : Type u} [inst : NonAssocSemiring R] {ι : Sort u_1} [Nonempty ι] {S : ι → Subsemiring R}
  [hS : ∀ (i : ι), IsMulCommutative ↥(S i)], Directed (fun x1 x2 => x1 ≤ x2) S → IsMulCommutative ↥(⨆ i, S i)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.small_Iio : ∀ (a : Cardinal.{u}), Small.{u, u + 1} ↑(Set.Iio a)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddMonoidHom.withBotMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N),
  ⇑f.withBotMap = WithBot.map ⇑f
-- Mathlib.Topology.Algebra.Group.Torsor
instIsTopologicalTorsorForall : ∀ {ι : Type u_1} {V : ι → Type u_2} {P : ι → Type u_3} [inst : (i : ι) → CommGroup (V i)]
  [inst_1 : (i : ι) → TopologicalSpace (V i)] [inst_2 : (i : ι) → Torsor (V i) (P i)]
  [inst_3 : (i : ι) → TopologicalSpace (P i)] [∀ (i : ι), IsTopologicalTorsor (P i)],
  IsTopologicalTorsor ((i : ι) → P i)
-- Mathlib.Algebra.Group.Support
Function.support_neg : ∀ {α : Type u_1} {G : Type u_3} [inst : SubtractionMonoid G] (f : α → G), Function.support (-f) = Function.support f
-- Init.Data.List.Erase
List.head_eraseP_mem : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} (h : List.eraseP p xs ≠ []), (List.eraseP p xs).head h ∈ xs
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
  {l : List ((a : α) × β a)},
  (Std.Internal.List.alterKey k f l).length =
    if h : Std.Internal.List.containsKey k l = true then
      if (f (some (Std.Internal.List.getValueCast k l h))).isSome = true then l.length else l.length - 1
    else if (f none).isSome = true then l.length + 1 else l.length
-- Mathlib.CategoryTheory.Monoidal.Category
/-- left whiskering for morphisms  -/
CategoryTheory.MonoidalCategoryStruct.whiskerLeft : {C : Type u} →
  {𝒞 : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.MonoidalCategoryStruct C] →
      (X : C) →
        {Y₁ Y₂ : C} →
          (Y₁ ⟶ Y₂) →
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y₁ ⟶
              CategoryTheory.MonoidalCategoryStruct.tensorObj X Y₂)
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.closure_singleton_le_iff_mem : ∀ {M : Type u_1} [inst : AddZeroClass M] (m : M) (p : AddSubmonoid M), AddSubmonoid.closure {m} ≤ p ↔ m ∈ p
-- Init.Data.String.Defs
/-- The start position of the string, as a `String.Pos.Raw.`  -/
String.rawStartPos : String → String.Pos.Raw
-- Std.Http.Data.Status
Std.Http.Status.unavailableForLegalReasons.sizeOf_spec : sizeOf Std.Http.Status.unavailableForLegalReasons = 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k k' : α},
  m.WF → m.getKey? k = some k' → (Std.HashMap.Raw.filterMap f m)[k]? = m[k]?.bind fun x => f k' x
-- Mathlib.Data.Seq.Basic
Stream'.Seq.update.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α) (n : ℕ) (f : α → α), s.update n f = ⟨Function.update (↑s) n (Option.map f (↑s n)), ⋯⟩
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.Lp.coeFn_const : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : NormedAddCommGroup E] [inst_1 : MeasureTheory.IsFiniteMeasure μ] (c : E),
  ↑↑((MeasureTheory.Lp.const p μ) c) =ᵐ[μ] Function.const α c
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Sheaf.epi_of_isLocallySurjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂) [J.HasSheafCompose (CategoryTheory.forget A)]
  [CategoryTheory.Sheaf.IsLocallySurjective φ], CategoryTheory.Epi φ
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsCoseparating.mk_of_exists_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  (∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x j, CategoryTheory.Mono j) → P.IsCoseparating
-- Mathlib.Order.Comparable
incompRel_swap : ∀ {α : Type u_1} (r : α → α → Prop), IncompRel (Function.swap r) = IncompRel r