mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.measure_set_eq : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s t : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    MeasureTheory.IsAddFundamentalDomain G t μ →
      ∀ {A : Set α}, MeasurableSet A → (∀ (g : G), (fun x => g +ᵥ x) ⁻¹' A = A) → μ (A ∩ s) = μ (A ∩ t)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.instClausePosFin : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
    (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.ofLE_toColimitPresentation : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (h : P.ColimitOfShape J X) {Q : CategoryTheory.ObjectProperty C}
  (hPQ : P ≤ Q), (h.ofLE hPQ).toColimitPresentation = h.toColimitPresentation
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
/-- The partial order on a C⋆-algebra defined by `x ≤ y` if and only if `y - x` is
selfadjoint and has nonnegative spectrum.

This is not declared as an instance because one may already have a partial order with better
definitional properties. However, it can be useful to invoke this as an instance in proofs.  -/
CStarAlgebra.spectralOrder : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_add_tdiv_mul : ∀ (m k : ℤ), m.tmod k + m.tdiv k * k = m
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionParams.range : Lean.Lsp.CodeActionParams → Lean.Lsp.Range
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.mk_sub_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] (m₁ m₂ : M) (s₁ s₂ : ↥⊤),
  AddLocalization.mk m₁ s₁ - AddLocalization.mk m₂ s₂ = AddLocalization.mk (m₁ + ↑s₂) ⟨↑s₁ + m₂, ⋯⟩
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonTextEdit.toJson : Lean.Lsp.TextEdit → Lean.Json
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [inst : ProbabilityTheory.IsSFiniteKernel κ] (f : α → β → ENNReal),
  κ.withDensity f =
    if hf : Measurable (Function.uncurry f) then { toFun := fun a => (κ a).withDensity (f a), measurable' := ⋯ } else 0
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.stronglyMeasurable_charFun : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [OpensMeasurableSpace E] [SecondCountableTopology E] [MeasureTheory.SFinite μ],
  MeasureTheory.StronglyMeasurable (MeasureTheory.charFun μ)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : Inhabited α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey! k = m₂.getKey! k
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmaKey.mk.sizeOf_spec : ∀ (type : Lean.Expr) (isPrivate defeq : Bool),
  sizeOf { type := type, isPrivate := isPrivate, defeq := defeq } = 1 + sizeOf type + sizeOf isPrivate + sizeOf defeq
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.sumArrowIsometryEquivProdArrow_symm_apply : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace γ] [inst_1 : Fintype α] [inst_2 : Fintype β]
  (p : (α → γ) × (β → γ)) (a : α ⊕ β), IsometryEquiv.sumArrowIsometryEquivProdArrow.symm p a = Sum.elim p.1 p.2 a
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instContinuousSMul : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} {R : Type u_4} [inst_1 : SMul R A]
  [inst_2 : TopologicalSpace R] [ContinuousSMul R A], ContinuousSMul R (CStarMatrix m n A)
-- Init.Data.Bool
Bool.and_eq_false_iff : ∀ {x y : Bool}, (x && y) = false ↔ x = false ∨ y = false
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.insert_union : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Finset α), insert a s ∪ t = insert a (s ∪ t)
-- Mathlib.Data.Nat.Totient
/-- Note this takes an explicit `Fintype ((ZMod n)ˣ)` argument to avoid trouble with instance
diamonds.  -/
ZMod.card_units_eq_totient : ∀ (n : ℕ) [NeZero n] [inst : Fintype (ZMod n)ˣ], Fintype.card (ZMod n)ˣ = n.totient
-- Mathlib.SetTheory.ZFC.Class
_private.Mathlib.SetTheory.ZFC.Class.0.ZFSet.coe_equiv_aux : ∀ {s : Set ZFSet.{u}} (hs : Small.{u, u + 1} ↑s),
  ↑(ZFSet.mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x))) = s
-- Mathlib.Data.Sym.Sym2
Equiv.sigmaQuotientFromRel_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (sym : Std.Symm r) {r' : Setoid β} (f : r →r ⇑r')
  (z : ↑(Sym2.fromRel sym)),
  (Equiv.sigmaQuotientFromRel sym f) z = Sym2.fromRelNdrec ↑z ⋯ (fun a₁ a₂ h => ⟨⟦f a₁⟧, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- A pair of morphisms `h : W ⟶ X` and `k : W ⟶ Y` satisfying `h ≫ f = k ≫ g` induces a morphism
`l : W ⟶ pullback f g` such that `l ≫ pullback.fst = h` and `l ≫ pullback.snd = k`.  -/
CategoryTheory.Limits.pullback.lift' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      {f : X ⟶ Z} →
        {g : Y ⟶ Z} →
          [inst_1 : CategoryTheory.Limits.HasPullback f g] →
            (h : W ⟶ X) →
              (k : W ⟶ Y) →
                CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g →
                  { l //
                    CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.fst f g) = h ∧
                      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.snd f g) = k }
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_sub : ∀ {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} (f g : ContIntertwiningMap π₁ π₂),
  (f - g).toContinuousLinearMap = f.toContinuousLinearMap - g.toContinuousLinearMap
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An open ball defined by `ArchimedeanClass.addSubgroup` of `UpperSet.Ioi c`.
For `c = ⊤`, we assign the junk value `⊥`.  -/
ArchimedeanClass.ballAddSubgroup : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → ArchimedeanClass M → AddSubgroup M
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntryD.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3)
  (fallback : (a : α) × β a) (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : (a : α) × β a) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_1 fallback
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.refl : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α}
  {f : α → γ}, AEMeasurable f μ → ProbabilityTheory.IdentDistrib f f μ μ
-- Init.Data.Float.Float32
/-- Multiplies 32-bit floating-point numbers according to IEEE 754. Typically used via the `*` operator.

This function has a logical model in terms of `Float32.Model`. It is compiled to the C multiplication operator.
 -/
Float32.mul : Float32 → Float32 → Float32
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.gluing_ι : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (j : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j =
    CategoryTheory.Limits.Multicoequalizer.π (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram j
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
dist_triangle_left : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y z : α), dist x y ≤ dist z x + dist z y
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is an antitone function taking values in a conditionally complete linear order
and `g` tends to `atBot` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`.  -/
Antitone.ciSup_comp_tendsto_atBot_of_linearOrder : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLinearOrder γ]
  {l : Filter α} [l.NeBot] {f : β → γ},
  Antitone f → ∀ {g : α → β}, Filter.Tendsto g l Filter.atBot → ⨆ a, f (g a) = ⨆ b, f b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} {h' : k ∈ Std.DHashMap.Raw.filter f m} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).get k h' = m.get k ⋯
-- Mathlib.Data.Bool.Basic
/-- `carry x y c` is `x && y || x && c || y && c`.  -/
Bool.carry : Bool → Bool → Bool → Bool
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
/-- A least element of a set is the infimum of this set.  -/
IsLeast.csInf_eq : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α}, IsLeast s a → sInf s = a
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Two n-simplices among cospherical points in n-space have the same
circumcenter.  -/
EuclideanGeometry.circumcenter_eq_of_cospherical : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V],
  Module.finrank ℝ V = n →
    EuclideanGeometry.Cospherical ps →
      ∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
        Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumcenter = sx₂.circumcenter
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (h : m.WF) {l : List ((a : α) × β a)} {k : α} (contains_eq_false : (List.map Sigma.fst l).contains k = false)
  {h' : k ∈ m.insertMany l}, (m.insertMany l).get k h' = m.get k ⋯
-- Init.Data.Vector.Lemmas
Vector.toArray_swap : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (hi : i < n) (hj : j < n),
  (xs.swap i j hi hj).toArray = xs.toArray.swap i j ⋯ ⋯
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.mapRelations.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)),
  P.mapRelations F η =
    CategoryTheory.CategoryStruct.comp (SheafOfModules.mapFreeIso F P.relations.I η).hom
      (CategoryTheory.CategoryStruct.comp
        (F.map ((CategoryTheory.Limits.kernel P.generators.π).freeHomEquiv.symm P.relations.s))
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.kernel.ι P.generators.π))
          (SheafOfModules.mapFreeIso F P.generators.I η).inv))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.ofPresheaf_presheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : CategoryTheory.Functor Cᵒᵖ Ab) [inst_1 : (X : Cᵒᵖ) → Module ↑(R.obj X) ↑(M.obj X)]
  (map_smul :
    ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r : ↑(R.obj X)) (m : ↑(M.obj X)),
      (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
        (CategoryTheory.ConcreteCategory.hom (R.map f)) r • (CategoryTheory.ConcreteCategory.hom (M.map f)) m),
  (PresheafOfModules.ofPresheaf M map_smul).presheaf = M
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.all_eq_true_iff_forall_mem_get : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {p : α → Bool}, m.WF → (m.all p = true ↔ ∀ (a : α) (h : a ∈ m), p (m.get a h) = true)
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The triangle `(triangleh φ).rotate` is isomorphic to a triangle attached to a
degreewise split short exact sequence of cochain complexes.  -/
CochainComplex.mappingCone.trianglehRotateIsoTrianglehOfDegreewiseSplit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (φ : K ⟶ L) →
            (CochainComplex.mappingCone.triangleh φ).rotate ≅
              CochainComplex.trianglehOfDegreewiseSplit (CochainComplex.mappingCone.triangleRotateShortComplex φ)
                (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R), W'.add P P = W'.dblXYZ P
-- Init.Data.List.Lemmas
List.set_append : ∀ {α : Type u_1} {i : ℕ} {x : α} {s t : List α},
  (s ++ t).set i x = if i < s.length then s.set i x ++ t else s ++ t.set (i - s.length) x
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.n_lt_xn : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), n < Pell.xn a1 n
-- Init.Data.UInt.Lemmas
USize.ofNatLT_mul : ∀ {a b : ℕ} (ha : a < 2 ^ System.Platform.numBits) (hb : b < 2 ^ System.Platform.numBits)
  (hab : a * b < 2 ^ System.Platform.numBits), USize.ofNatLT (a * b) hab = USize.ofNatLT a ha * USize.ofNatLT b hb
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.bijective_algebraMap_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : Field R] [inst_1 : Semiring A] [Nontrivial A] [inst_3 : Algebra R A],
  Function.Bijective ⇑(algebraMap R A) ↔ ⊤ = ⊥
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fst_smul : ∀ {S : Type u_2} {R : Type u_3} {A : Type u_4} [inst : SMul S R] [inst_1 : SMul S A] (s : S) (x : Unitization R A),
  (s • x).toProd.1 = s • x.toProd.1
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps.mk.sizeOf_spec : ∀ (map : Lean.PHashMap Lean.Meta.Origin ℕ) (size : ℕ),
  sizeOf { map := map, size := size } = 1 + sizeOf map + sizeOf size
-- Mathlib.RingTheory.PolynomialAlgebra
coe_polyEquivTensor'_symm : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_4) [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  ⇑(polyEquivTensor' R A).symm = ⇑(polyEquivTensor R A).symm
-- Mathlib.Combinatorics.Graph.Simple
Graph.Loopless.mk : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, (∀ (e : β) (x : α), ¬G.IsLoopAt e x) → G.Loopless
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.mkNatLookupTableLifting : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoAppCounitObjOfFaithfulOfFull : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Faithful] [L.Full] {Y : C},
  CategoryTheory.IsIso (h.counit.app (L.obj Y))
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
SeparationQuotient.norm_liftNormedAddGroupHom_apply_le : ∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  (f : NormedAddGroupHom M N) (hf : ∀ (x : M), ‖x‖ = 0 → f x = 0) (x : SeparationQuotient M),
  ‖(SeparationQuotient.liftNormedAddGroupHom f hf) x‖ ≤ ‖f‖ * ‖x‖
-- Mathlib.Algebra.CubicDiscriminant
Cubic.d_eq_three_roots : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K} {x y z : K},
  P.a ≠ 0 → (Cubic.map φ P).roots = {x, y, z} → φ P.d = φ P.a * -(x * y * z)
-- Mathlib.Data.Set.Subsingleton
Set.Nontrivial.ne_singleton : ∀ {α : Type u} {s : Set α} {x : α}, s.Nontrivial → s ≠ {x}
-- Mathlib.Algebra.Field.Defs
Semifield.toNontrivial : ∀ {K : Type u_2} [self : Semifield K], Nontrivial K
-- Mathlib.Data.NNRat.Defs
Mathlib.Tactic.Qify.nnratCast_eq : ∀ (a b : ℚ≥0), a = b ↔ ↑a = ↑b
-- Mathlib.Tactic.ProdAssoc
/-- `prod_assoc%` elaborates to the "obvious" equivalence between iterated products of types,
regardless of how the products are parenthesized.
The `prod_assoc%` term uses the expected type when elaborating.
For example, `(prod_assoc% : (α × β) × (γ × δ) ≃ α × (β × γ) × δ)`.

The elaborator can handle holes in the expected type,
so long as they eventually get filled by unification.
```lean
example : (α × β) × (γ × δ) ≃ α × (β × γ) × δ :=
  (prod_assoc% : _ ≃ α × β × γ × δ).trans prod_assoc%
```
 -/
Lean.Expr.«termProd_assoc%» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.decomposeLinearEquiv_comp_subtype : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (ℳ : ι → Submodule R M) [inst_3 : DecidableEq ι] [inst_4 : DirectSum.Decomposition ℳ] {i : ι},
  ↑(DirectSum.decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype = DirectSum.lof R ι (fun i => ↥(ℳ i)) i
-- Mathlib.Logic.Godel.GodelBetaFunction
Nat.coprime_mul_succ : ∀ {n m a : ℕ}, m - n ∣ a → (n * a + 1).Coprime (m * a + 1)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.iso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasInjectiveResolutions C] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.injectiveResolutions C).map f) J.iso.hom =
      CategoryTheory.CategoryStruct.comp I.iso.hom ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ)
-- Mathlib.Order.WithBot
WithTop.toDual_le_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithBot αᵒᵈ} {y : WithTop α}, WithTop.toDual y ≤ x ↔ WithBot.ofDual x ≤ y
-- Mathlib.AlgebraicTopology.SimplicialNerve
/-- Auxiliary definition for `SimplicialThickening.functor`  -/
CategoryTheory.SimplicialThickening.functorMap : {J K : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : LinearOrder K] →
      (f : J →o K) →
        (i j : CategoryTheory.SimplicialThickening J) →
          CategoryTheory.Functor (i ⟶ j) ({ as := f i.as } ⟶ { as := f j.as })
-- Mathlib.Order.Disjoint
disjoint_self : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint a a ↔ a = ⊥
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- A variant of `deriv_const_mul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
deriv_const_mul_field : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {v : 𝕜 → 𝕜'} (u : 𝕜'), deriv (fun y => u * v y) x = u * deriv v x
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_add_const_left : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f : α → G} (C : G), Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => C + f x) l Filter.atTop
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
/-- The family of morphisms in `SSet` which consists of inner horn inclusions
`Λ[n, i].ι : Λ[n, i] ⟶ Δ[n]` (for `0 < i < n`).  -/
SSet.innerHornInclusions : CategoryTheory.MorphismProperty SSet
-- Lean.Meta.Check
Lean.Meta.throwLetTypeMismatchMessage : {α : Type} → Lean.FVarId → Lean.MetaM α
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_filter_lt_of_le_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}
  [inst_2 : DecidablePred fun x => x < c],
  c ≤ b → Multiset.filter (fun x => x < c) (Multiset.Ico a b) = Multiset.Ico a c
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.subtype_injective : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] (S' : A),
  Function.Injective ⇑(MulMemClass.subtype S')
-- Mathlib.Algebra.Group.Ideal
/-- In a monoid, the semigroup ideal generated by `s` is `Set.univ * s`.  -/
SemigroupIdeal.coe_closure' : ∀ {M : Type u_1} [inst : Monoid M] {s : Set M}, ↑(SemigroupIdeal.closure s) = Set.univ * s
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toStarRingEquiv_symm : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B), ↑e.symm = (↑e).symm
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- A continuous function from an `OpensMeasurableSpace` to a `BorelSpace`
is ae-measurable.  -/
Continuous.aemeasurable : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ] {f : α → γ},
  Continuous f → ∀ {μ : MeasureTheory.Measure α}, AEMeasurable f μ
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.eq_bot_iff_forall_not_adj : ∀ {V : Type u} {G : SimpleGraph V}, G = ⊥ ↔ ∀ (a b : V), ¬G.Adj a b
-- Mathlib.Topology.Sheaves.Points
/-- A point `x` of a topological space `X` specializes to `y` if and only iff
there is a (unique) morphism between the corresponding points of the site
`(Opens X, grothendieckTopology X)`.  -/
Opens.pointGrothendieckTopologyHomEquiv : {X : Type u} →
  [inst : TopologicalSpace X] →
    {x y : X} → (Opens.pointGrothendieckTopology x ⟶ Opens.pointGrothendieckTopology y) ≃ x ⤳ y