mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.DFinsupp.Order
DFinsupp.single_le_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [∀ (i : ι), CanonicallyOrderedAdd (α i)] [inst_3 : DecidableEq ι] {f : Π₀ (i : ι), α i} {i : ι} {a : α i},
  (fun₀ | i => a) ≤ f ↔ a ≤ f i
-- Batteries.Lean.NameMapAttribute
/-- Similar to `registerParametricAttribute` except that attributes do not
have to be assigned in the same file as the declaration.  -/
Lean.registerNameMapAttribute : {α : Type} → Lean.NameMapAttributeImpl α → IO (Lean.NameMapExtension α)
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_div_le : ∀ {a b : ENNReal}, a * (b / a) ≤ b
-- Mathlib.Topology.Constructions.SumProd
/-- The second projection in a product of topological spaces sends open sets to open sets.  -/
isOpenMap_snd : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpenMap Prod.snd
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul`. -/
ProbabilityTheory.Kernel.iIndepFun.measure_inter_preimage_eq_mul : ∀ {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {ι : Type u_8} {β : ι → Type u_9} (m : (x : ι) → MeasurableSpace (β x))
  (f : (i : ι) → Ω → β i),
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
      (∀ i ∈ S, MeasurableSet (sets i)) →
        ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.comap_mk : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] (φ : K →+* ℂ) (f : k →+* K),
  (NumberField.InfinitePlace.mk φ).comap f = NumberField.InfinitePlace.mk (φ.comp f)
-- Mathlib.Order.Bounds.Basic
lowerBounds_Ioi : ∀ {γ : Type u_3} [inst : LinearOrder γ] [DenselyOrdered γ] {a : γ}, lowerBounds (Set.Ioi a) = Set.Iic a
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.expandIfNecessary : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.packingNumber_eq_zero : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal}, Metric.packingNumber ε A = 0 ↔ A = ∅
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
CommGrpTypeEquivalenceCommGrp.inverse_obj_X : ∀ {A : CommGrpCat}, (CommGrpTypeEquivalenceCommGrp.inverse.obj A).X = ↑A
-- Std.Time.Date.Unit.Weekday
/-- Friday.  -/
Std.Time.Weekday.friday : Std.Time.Weekday
-- Mathlib.Data.Set.Pairwise.Basic
/-- **Alias** of `Set.pairwise_insert_of_symm`. -/
Set.pairwise_insert_of_symmetric : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} [Std.Symm r],
  (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instHasDetOneMinGeneralLinearGroup : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R]
  (Γ Γ' : Subgroup (GL n R)) [Γ.HasDetOne], (Γ ⊓ Γ').HasDetOne
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instPartialOrder.eq_1 : ∀ {α : Type u} [inst : AddGroup α],
  AddGroupTopology.instPartialOrder = PartialOrder.lift AddGroupTopology.toTopologicalSpace ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_none : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∉ t → t.getKey? a = none
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.core_obj_of : ∀ {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 : CategoryTheory.Core C), (F.core.obj X).of = F.obj X.of
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Const.get! : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → [Inhabited β] → Std.DTreeMap α (fun x => β) cmp → α → β
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instMulActionSubtypeMemAddSubgroupOfStarModule : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Star R] →
      [TrivialStar R] →
        [inst_2 : AddGroup A] →
          [inst_3 : StarAddMonoid A] →
            [inst_4 : Monoid R] → [inst_5 : MulAction R A] → [StarModule R A] → MulAction R ↥(selfAdjoint A)
-- Lean.Meta.Basic
/-- Given `e` of the form `fun ..xs ..ys => A`, execute `k xs (fun ..ys => A)` where
`xs.size ≤ maxFVars`.
This combinator will declare local declarations, create free variables for them,
execute `k` with updated local context, and make sure the cache is restored after executing `k`.

If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.
 -/
Lean.Meta.lambdaBoundedTelescope : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] → {α : Type} → Lean.Expr → ℕ → (Array Lean.Expr → Lean.Expr → n α) → optParam Bool false → n α
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.mem_stabilizer_finset' : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {a : G} [inst_2 : DecidableEq α]
  {s : Finset α}, a ∈ MulAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.instMonadShareCommonAlphaShareBuilderM : Lean.Meta.Sym.Internal.MonadShareCommon Lean.Meta.Sym.Internal.AlphaShareBuilderM
-- Mathlib.Data.List.Lattice
List.Disjoint.symm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ → l₂.Disjoint l₁
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon_uniqueness : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] {a b : ℤ} {X : C}
  (φ : (t.truncGELT a b).obj X ⟶ (t.truncLTGE a b).obj X),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X))
        (CategoryTheory.CategoryStruct.comp φ ((t.truncLTι b).app ((t.truncGE a).obj X))) =
      CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) ((t.truncGEπ a).app X) →
    (t.truncGELTToLTGE a b).app X = φ
-- Mathlib.LinearAlgebra.BilinearMap
/-- A version of `Function.Injective.comp` for composition of a bilinear map with a linear map.  -/
LinearMap.injective_compr₂ₛₗ_of_injective : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {R₄ : Type u_16} {M : Type u_17}
  {N : Type u_18} {P : Type u_19} {Q : Type u_20} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃]
  [inst_3 : CommSemiring R₄] [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : AddCommMonoid Q] [inst_8 : Module R M] [inst_9 : Module R₂ N] [inst_10 : Module R₃ P]
  [inst_11 : Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  [inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P)
  (g : P →ₛₗ[σ₃₄] Q), Function.Injective ⇑f → Function.Injective ⇑g → Function.Injective ⇑(f.compr₂ₛₗ g)
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A function which can be locally uniformly approximated by functions which are continuous
on a set is continuous on this set.  -/
continuousOn_of_locally_uniform_approx_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  (∀ x ∈ s, ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) →
    ContinuousOn f s
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.evalCLM_apply_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedAddCommGroup G]
  [inst_6 : NormedSpace ℝ G] [inst_7 : NormedSpace 𝕜 G] [inst_8 : SMulCommClass ℝ 𝕜 G] (f : SchwartzMap E (F →L[ℝ] G))
  (m : F) (x : E), ((SchwartzMap.evalCLM 𝕜 E G m) f) x = (f x) m
-- Mathlib.RingTheory.Bialgebra.Convolution
BialgHom.instMulWithConv : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring C] →
            [inst_3 : Bialgebra R A] → [inst_4 : Bialgebra R C] → [Coalgebra.IsCocomm R C] → Mul (WithConv (C →ₐc[R] A))
-- Mathlib.Data.Fin.SuccPred
Fin.succ_castAdd : ∀ {n m : ℕ} (i : Fin n),
  (Fin.castAdd m i).succ = if h : i.succ = Fin.last n then Fin.natAdd n 0 else Fin.castAdd (m + 1) ⟨↑i + 1, ⋯⟩
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.mapRingHom_comp : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring T] (f : S →+* T)
  (g : R →+* S), (Polynomial.mapRingHom f).comp (Polynomial.mapRingHom g) = Polynomial.mapRingHom (f.comp g)
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductBifunctor_map_app : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₂ C}
  (f : X ⟶ Y) (X_1 : J₁ × J₂),
  ((CategoryTheory.MonoidalCategory.externalProductBifunctor J₁ J₂ C).map f).app X_1 =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.1.app X_1.1) (X.2.obj X_1.2))
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Y.1.obj X_1.1) (f.2.app X_1.2))
-- Mathlib.RingTheory.Bialgebra.TensorProduct
TensorProduct.instBialgebra : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      (B : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Bialgebra S A] →
                  [inst_5 : Bialgebra R B] →
                    [inst_6 : Algebra R A] →
                      [inst_7 : Algebra R S] → [IsScalarTower R S A] → Bialgebra S (TensorProduct R A B)
-- Std.Http.Data.Method
/-- Retrieve headers for a resource, without the body.
Source: https://httpwg.org/specs/rfc9110.html#section-9.3.2
 -/
Std.Http.Method.head : Std.Http.Method
-- Mathlib.CategoryTheory.Whiskering
/-- The isomorphism between right-whiskering on the composition of functors and the composition
of two right-whiskering applications.  -/
CategoryTheory.Functor.whiskeringRightObjCompIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {D' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] →
                (F : CategoryTheory.Functor C D) →
                  (G : CategoryTheory.Functor D D') →
                    ((CategoryTheory.Functor.whiskeringRight E C D).obj F).comp
                        ((CategoryTheory.Functor.whiskeringRight E D D').obj G) ≅
                      (CategoryTheory.Functor.whiskeringRight E C D').obj (F.comp G)
-- Mathlib.Algebra.GroupWithZero.Defs
mul_inv_cancel_right₀ : ∀ {G₀ : Type u} [inst : GroupWithZero G₀] {b : G₀}, b ≠ 0 → ∀ (a : G₀), a * b * b⁻¹ = a
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- A Cartesian morphism lifting `f : R ⟶ S` with domain in the image of `Fib p R`  -/
HasFibers.pullbackMap : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        {p : CategoryTheory.Functor 𝒳 𝒮} →
          [inst_2 : HasFibers p] →
            [inst_3 : p.IsPreFibered] →
              {R S : 𝒮} →
                {a : 𝒳} → (f : R ⟶ S) → (ha : p.obj a = S) → (HasFibers.ι R).obj (HasFibers.mkPullback f ha) ⟶ a
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.comp_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' R'' : Φ.RightResolution X₂} (φ : R ⟶ R') (ψ : R' ⟶ R''),
  (CategoryTheory.CategoryStruct.comp φ ψ).f = CategoryTheory.CategoryStruct.comp φ.f ψ.f
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- A formula for `MeasureTheory.Measure.mkMetric`.  -/
MeasureTheory.Measure.mkMetric_apply : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (m : ENNReal → ENNReal)
  (s : Set X),
  (MeasureTheory.Measure.mkMetric m) s =
    ⨆ r,
      ⨆ (_ : 0 < r),
        ⨅ t,
          ⨅ (_ : s ⊆ Set.iUnion t),
            ⨅ (_ : ∀ (n : ℕ), Metric.ediam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (Metric.ediam (t n))
-- Mathlib.Data.Set.Finite.Lattice
Set.finite_sdiff_iUnion_Ioo : ∀ {α : Type u} [inst : LinearOrder α] (s : Set α), (s \ ⋃ x ∈ s, ⋃ y ∈ s, Set.Ioo x y).Finite
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS_nc.eq_def : ∀ (x : Lean.Grind.CommRing.Expr),
  x.toPolyS_nc =
    match x with
    | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num ↑n.natAbs
    | Lean.Grind.CommRing.Expr.var x => Lean.Grind.CommRing.Poly.ofVar x
    | a.add b => a.toPolyS_nc.combine b.toPolyS_nc
    | a.mul b => a.toPolyS_nc.mul_nc b.toPolyS_nc
    | a.pow k =>
      match a with
      | Lean.Grind.CommRing.Expr.num n => Lean.Grind.CommRing.Poly.num (↑n.natAbs ^ k)
      | Lean.Grind.CommRing.Expr.var x =>
        Lean.Grind.CommRing.Poly.ofMon (Lean.Grind.CommRing.Mon.mult { x := x, k := k } Lean.Grind.CommRing.Mon.unit)
      | x => a.toPolyS_nc.pow_nc k
    | Lean.Grind.CommRing.Expr.natCast n => Lean.Grind.CommRing.Poly.num ↑n
    | a.sub b => Lean.Grind.CommRing.Poly.num 0
    | a.neg => Lean.Grind.CommRing.Poly.num 0
    | Lean.Grind.CommRing.Expr.intCast k => Lean.Grind.CommRing.Poly.num 0
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
/-- The translation of set `x +ᵥ s` is defined as `{x +ᵥ y | y ∈ s}` in scope `Pointwise`.  -/
Set.vaddSet : {α : Type u_2} → {β : Type u_3} → [VAdd α β] → VAdd α (Set β)
-- Mathlib.GroupTheory.Congruence.BigOperators
AddCon.dfinsuppSum : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M]
  [inst_2 : (i : ι) → Zero (β i)] [inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : AddCon M)
  (h h' : (i : ι) → β i → M) {f g : Π₀ (i : ι), β i},
  (∀ (i : ι), c (h i 0) 0) →
    (∀ (i : ι), c (h' i 0) 0) → (∀ (i : ι), c (h i (f i)) (h' i (g i))) → c (f.sum h) (g.sum h')
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv'_symm_app_naturality_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) {P Q : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} (f : P ⟶ Q) (E : ℰ)
  (g : Q ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E)
  (p : CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P),
  ((CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A P E).symm (CategoryTheory.CategoryStruct.comp f g)).app p =
    ((CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A Q E).symm g).app
      ((CategoryTheory.CostructuredArrow.map f).obj p)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabitedPreDiscrTree : {a : Type} → Inhabited (Lean.Meta.LazyDiscrTree.PreDiscrTree a)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepFun.congr : ∀ {Ω : Type u_1} {β : Type u_6} {β' : Type u_7} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → β}
  {g : Ω → β'} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {f' : Ω → β} {g' : Ω → β'},
  ProbabilityTheory.IndepFun f g μ → f =ᵐ[μ] f' → g =ᵐ[μ] g' → ProbabilityTheory.IndepFun f' g' μ
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_inj : ∀ {a b : UInt16}, a.toUInt64 = b.toUInt64 ↔ a = b
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.unopOpIso_inv_app : ∀ {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ᵒᵖ), F.unopOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Data.Nat.Sqrt
Nat.eq_sqrt : ∀ {n a : ℕ}, a = n.sqrt ↔ a * a ≤ n ∧ n < (a + 1) * (a + 1)
-- Mathlib.Algebra.Group.Defs
/-- A monoid is torsion-free if power by every non-zero element `n : ℕ` is injective.  -/
IsMulTorsionFree : (M : Type u_2) → [Monoid M] → Prop
-- Mathlib.GroupTheory.Congruence.Defs
Con.le_conGen : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop}, r ≤ ⇑(conGen r)
-- Init.Meta.Defs
/-- Decodes a valid string gap after the `\`.
Note that this function matches `"\" whitespace+` rather than
the more restrictive `"\" newline whitespace*` since this simplifies the implementation.
Justification: this does not overlap with any other sequences beginning with `\`.
 -/
Lean.Syntax.decodeStringGap : String → String.Pos.Raw → Option String.Pos.Raw
-- Mathlib.Algebra.Module.GradedModule
/-- A graded version of `Semiring.toModule`.  -/
DirectSum.GSemiring.toGmodule : {ιA : Type u_1} →
  (A : ιA → Type u_3) →
    [inst : AddMonoid ιA] →
      [inst_1 : (i : ιA) → AddCommMonoid (A i)] → [h : DirectSum.GSemiring A] → DirectSum.Gmodule A A
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
/-- Given objects `X` and `Y` in `Cᵒᵖ`, this is the bijection
`(op (X.unop⟦n⟧) ⟶ Y) ≃ (X ⟶ Y⟦n⟧)` for any `n : ℤ`.  -/
CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {n : ℤ} →
        {X Y : Cᵒᵖ} →
          (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) ≃
            (X ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ n).obj Y)
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.stupidTruncMap_id : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c')
  [inst_3 : e.IsRelIff],
  HomologicalComplex.stupidTruncMap (CategoryTheory.CategoryStruct.id K) e =
    CategoryTheory.CategoryStruct.id (K.stupidTrunc e)
-- Init.Data.Rat.Basic
instToStringRat : ToString ℚ
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n}
  [hf : Fact (Module.finrank ℝ V = n)] {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (i : Fin (n + 1)),
      affineSpan ℝ (Set.range (s.faceOpposite i).points) = (s.exsphere signs).orthRadius (s.touchpoint signs i)
-- Mathlib.Data.Set.Enumerate
Set.enumerate.eq_2 : ∀ {α : Type u_1} (sel : Set α → Option α) (x : Set α) (n : ℕ),
  Set.enumerate sel x n.succ = do
    let a ← sel x
    Set.enumerate sel (x \ {a}) n
-- Mathlib.Data.Set.Card
Set.ncard_image_le : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β},
  autoParam s.Finite Set.ncard_image_le._auto_1 → (f '' s).ncard ≤ s.ncard
-- Mathlib.Algebra.Free
/-- Isomorphism between `Magma.AssocQuotient (FreeMagma α)` and `FreeSemigroup α`.  -/
FreeMagmaAssocQuotientEquiv : (α : Type u) → Magma.AssocQuotient (FreeMagma α) ≃* FreeSemigroup α
-- Init.SimpLemmas
instAssociativeAnd : Std.Associative And
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Adding a multiple of the first vector passed to `oangle` to the second vector does not change
the sign of the angle.  -/
Orientation.oangle_sign_smul_add_right : ∀ {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 : V) (r : ℝ), (o.oangle x (r • x + y)).sign = (o.oangle x y).sign
-- Mathlib.Topology.Instances.CantorSet
_private.Mathlib.Topology.Instances.CantorSet.0.preCantorSet.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousAddCoeCofinite : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))] [inst_2 : (i : ι) → Add (R i)]
  [inst_3 : ∀ (i : ι), AddMemClass (S i) (R i)] [∀ (i : ι), ContinuousAdd (R i)],
  ContinuousAdd (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
_private.Mathlib.NumberTheory.ModularForms.LevelOne.Basic.0.term𝕢 : Lean.ParserDescr
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_v_d_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j k : ℤ)
  (hij : i + -1 = j) (hik : k + -1 = i) {Z : C} (h : (CochainComplex.mappingCone φ).X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j hij)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d j i) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (φ.f i) ((CochainComplex.mappingCone.inr φ).f i) -
        CategoryTheory.CategoryStruct.comp (F.d i k) ((CochainComplex.mappingCone.inl φ).v k i hik))
      h
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_prod_of_mulSupport_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Finset α},
  Function.mulSupport f ⊆ ↑s → ∏ᶠ (i : α), f i = ∏ i ∈ s, f i
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- The Upper Set topology is homeomorphic to the Lower Set topology on the dual order
 -/
Topology.WithUpperSet.toDualHomeomorph : {α : Type u_1} → [inst : Preorder α] → Topology.WithUpperSet α ≃ₜ Topology.WithLowerSet αᵒᵈ
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.instQuasiCompactOfIsAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f], AlgebraicGeometry.QuasiCompact f
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isValidSearchFrom_iff_isValidSearchFrom_beq : ∀ {c : Char} {s : String.Slice} {p : s.Pos} {l : List (String.Slice.Pattern.SearchStep s)},
  String.Slice.Pattern.Model.IsValidSearchFrom c p l ↔
    String.Slice.Pattern.Model.IsValidSearchFrom (fun x => x == c) p l
-- Mathlib.Data.PNat.Interval
PNat.Ico_eq_finset_subtype : ∀ (a b : ℕ+), Finset.Ico a b = Finset.subtype (fun n => 0 < n) (Finset.Ico ↑a ↑b)
-- Lean.Meta.Tactic.Grind.CastLike
Lean.Meta.Grind.isCastLikeApp : Lean.Expr → Bool
-- Mathlib.Order.Bounds.Basic
isLeast_Ici : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsLeast (Set.Ici a) a
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_def : ∀ (z : ℂ), Complex.exp z = (Complex.exp' z).lim