mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvalues.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A A_1 : Matrix n n 𝕜} (e_A : A = A_1)
  {inst_2 : DecidableEq n} [inst_3 : DecidableEq n] (hA : A.IsHermitian) (a a_1 : n),
  a = a_1 → hA.eigenvalues a = ⋯.eigenvalues a_1
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- `C` has disjoint binary coproducts if every binary coproduct is disjoint.  -/
CategoryTheory.Limits.BinaryCoproductsDisjoint : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.mk.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R} (i i_1 : A)
  (e_i : i = i_1) (j j_1 : A) (e_j : j = j_1) (k k_1 : A) (e_k : k = k_1) (i_mul_i : i * i = c₁ • 1 + c₂ • i)
  (j_mul_j : j * j = c₃ • 1) (i_mul_j : i * j = k) (j_mul_i : j * i = c₂ • j - k),
  { i := i, j := j, k := k, i_mul_i := i_mul_i, j_mul_j := j_mul_j, i_mul_j := i_mul_j, j_mul_i := j_mul_i } =
    { i := i_1, j := j_1, k := k_1, i_mul_i := ⋯, j_mul_j := ⋯, i_mul_j := ⋯, j_mul_i := ⋯ }
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The `ValueGroupWithZero R` is the "minimal" value group (with zero) among all value groups
of valuations that are compatible with the valuative relation, in the sense that it is canonically
isomorphic to the subgroup (with zero) generated by `v '' R` for any compatible `v`.
`ValueGroupWithZero.embed v` is exactly this isomorphism map; it will later be upgraded to
`ValueGroupWithZero.orderMonoidIso v`.  -/
ValuativeRel.ValueGroupWithZero.embed : {R : Type u_2} →
  {Γ : Type u_3} →
    [inst : Ring R] →
      [inst_1 : ValuativeRel R] →
        [inst_2 : LinearOrderedCommGroupWithZero Γ] →
          (v : Valuation R Γ) →
            [v.Compatible] → ValuativeRel.ValueGroupWithZero R →*₀ (MonoidWithZeroHom.ofClass v).ValueGroup₀
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.forIn_filterM : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β γ : Type u_1} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadAttach n]
  [WeaklyLawfulMonadAttach n] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_10 : MonadLiftT n o]
  [LawfulMonadLiftT n o] [inst_12 : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_14 : Std.IteratorLoop α m o]
  [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β} {f : β → n (ULift.{u_1, 0} Bool)} {init : γ}
  {g : β → γ → o (ForInStep γ)},
  forIn (Std.IterM.filterM f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out)
      if __do_lift.down = true then g out acc else pure (ForInStep.yield acc)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMapTR.go.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instSMul : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module S F] →
                      {M : Type u_7} →
                        [inst_6 : Monoid M] →
                          [inst_7 : DistribMulAction M F] → [SMulCommClass S M F] → SMul M (E →ₛₗ.[σ] F)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.sum : ∀ {α : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] {ι : Type u_4} {f : ι → α → M},
  (∀ (i : ι), Function.HasFiniteSupport (f i)) → ∀ (s : Finset ι), Function.HasFiniteSupport fun a => ∑ i ∈ s, f i a
-- Std.Async.System
Std.Async.System.instDecidableEqUserId : DecidableEq Std.Async.System.UserId
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [Std.TransCmp cmp] {k : α}, t.keysArray.contains k = t.contains k
-- Mathlib.RingTheory.Ideal.Prod
Ideal.ideal_prod_prime_aux : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} {J : Ideal S},
  (I.prod J).IsPrime → I = ⊤ ∨ J = ⊤
-- Lean.Meta.Check
_private.Lean.Meta.Check.0.Lean.Meta.checkConstant : Lean.Name → List Lean.Level → Lean.MetaM Unit
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mapId_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.mapId C).hom.app X =
    (match X with
      | CategoryTheory.WithTerminal.of a => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of a)
      | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.forget_obj : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) (X : F.Grothendieck),
  (CategoryTheory.Pseudofunctor.Grothendieck.forget F).obj X = X.base
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.sec_fst_ne_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : S}, x ≠ 0 → (IsLocalization.sec M x).1 ≠ 0
-- Mathlib.LinearAlgebra.Coevaluation
/-- The coevaluation map is a linear map from a field `K` to a finite-dimensional
vector space `V`.  -/
coevaluation : (K : Type u) →
  [inst : Field K] →
    (V : Type v) →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → [FiniteDimensional K V] → K →ₗ[K] TensorProduct K V (Module.Dual K V)
-- Mathlib.CategoryTheory.Limits.Opposites
/-- The colimit of `F.rightOp` is the opposite of `limit F`.  -/
CategoryTheory.Limits.colimitRightOpIsoUnopLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ C) →
          [inst_2 : CategoryTheory.Limits.HasLimit F] →
            CategoryTheory.Limits.colimit F.rightOp ≅ Opposite.op (CategoryTheory.Limits.limit F)
-- Std.Time.DateTime.PlainDateTime
/-- Wraps a `PlainDate` in a `PlainDateTime` with midnight as the time component.
 -/
Std.Time.PlainDateTime.ofPlainDate : Std.Time.PlainDate → Std.Time.PlainDateTime
-- Init.Data.Vector.Lemmas
Vector.foldl_eq_foldr_reverse : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : β → α → β} {b : β},
  Vector.foldl f b xs = Vector.foldr (fun x y => f y x) b xs.reverse
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.powers_le : ∀ {M : Type u_1} [inst : Monoid M] {n : M} {P : Submonoid M}, Submonoid.powers n ≤ P ↔ n ∈ P
-- Mathlib.Topology.Constructions.SumProd
Prod.tendsto_iff : ∀ {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z] {X : Type u_5} (seq : X → Y × Z)
  {f : Filter X} (p : Y × Z),
  Filter.Tendsto seq f (nhds p) ↔
    Filter.Tendsto (fun n => (seq n).1) f (nhds p.1) ∧ Filter.Tendsto (fun n => (seq n).2) f (nhds p.2)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} [inst_1 : Inhabited (β k)],
  (Std.ExtDHashMap.filter f m).get! k = (Option.filter (f k) (m.get? k)).get!
-- Init.Data.List.Basic
List.contains_nil : ∀ {α : Type u} {a : α} [inst : BEq α], [].contains a = false
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mulAction.eq_1 : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] (p : SubMulAction R M),
  p.mulAction = p.mulAction'
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.id_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Center C), (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.fst
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.MonadCommRing.getCommRing : {m : Type → Type} → [self : Lean.Meta.Grind.Arith.CommRing.MonadCommRing m] → m Lean.Meta.Grind.Arith.CommRing.CommRing
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
Differentiable.comp_mdifferentiableWithinAt : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F'] {g : F → F'}
  {f : M → F} {s : Set M} {x : M}, Differentiable 𝕜 g → MDiffAt[s] f x → MDiffAt[s] (g ∘ f) x
-- Mathlib.Combinatorics.Additive.CovBySMul
CovByVAdd.nonneg : ∀ {M : Type u_1} {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M X] {K : ℝ} {A B : Set X},
  CovByVAdd M K A B → 0 ≤ K
-- Batteries.Data.List.Lemmas
List.disjoint_symm : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ → l₂.Disjoint l₁
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- Taking a sum over `f : α →₀ M` is the same as adding the value on a
single element `y ∈ f.support` to the sum over `erase y f`.  -/
Finsupp.add_sum_erase : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α →₀ M) (y : α)
  (g : α → M → N), y ∈ f.support → g y (f y) + (Finsupp.erase y f).sum g = f.sum g
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.instToJsonOptions.toJson : Lean.Lsp.CreateFile.Options → Lean.Json
-- Mathlib.Data.Fintype.Inv
/-- The inverse of an embedding `f : α ↪ β`, of the type `↥(Set.range f) → α`.
This is the computable version of `Function.invFun` that requires `Fintype α` and `DecidableEq β`,
or the function version of applying `(Equiv.ofInjective f f.injective).symm`.
This function should not usually be used for actual computation because for most cases,
an explicit inverse can be stated that has better computational properties.
This function computes by checking all terms `a : α` to find the `f a = b`, so it is O(N) where
`N = Fintype.card α`.
 -/
Function.Embedding.invOfMemRange : {α : Type u_1} → {β : Type u_2} → [Fintype α] → [DecidableEq β] → (f : α ↪ β) → ↑(Set.range ⇑f) → α
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.ext_iff : ∀ {x y : YoungDiagram}, x = y ↔ x.cells = y.cells
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1_smul : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (c : ℝ) (x : G),
  MeasureTheory.condExpIndL1 hm μ s (c • x) = c • MeasureTheory.condExpIndL1 hm μ s x
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.singleton_inj : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x y : α}, {x} = {y} ↔ x = y
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Given any distinguished triangle `T`, then we know `T.rotate` is also distinguished.
 -/
CategoryTheory.Pretriangulated.rot_of_distTriang : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    T.rotate ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.exists_integral_multiples : ∀ (R : Type u_1) {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [NoZeroDivisors R]
  [alg : Algebra.IsAlgebraic R A] (s : Finset A), ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 0 → G) → ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesIso₀ A).inv
      (CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 0) h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH0 A).f
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).inv h)
-- Mathlib.Order.Filter.SmallSets
/-- Generalized **squeeze theorem** (also known as **sandwich theorem**). If `s : α → Set β` is a
family of sets that tends to `Filter.smallSets lb` along `la` and `f : α → β` is a function such
that `f x ∈ s x` eventually along `la`, then `f` tends to `lb` along `la`.

If `s x` is the closed interval `[g x, h x]` for some functions `g`, `h` that tend to the same limit
`𝓝 y`, then we obtain the standard squeeze theorem, see
`tendsto_of_tendsto_of_tendsto_of_le_of_le'`.  -/
Filter.Tendsto.of_smallSets : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {s : α → Set β} {f : α → β},
  Filter.Tendsto s la lb.smallSets → (∀ᶠ (x : α) in la, f x ∈ s x) → Filter.Tendsto f la lb
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf₂_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {κ : ι → Sort u_5} {f : (i : ι) → κ i → α},
  BddBelow (⋃ i, Set.range (f i)) → ∀ (i : ι) (j : κ i), ⨅ i, ⨅ j, f i j ≤ f i j
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isTopologicalRing : ∀ {ι : 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 : ι) → Ring (R i)]
  [inst_3 : ∀ (i : ι), SubringClass (S i) (R i)] [∀ (i : ι), IsTopologicalRing (R i)],
  IsTopologicalRing (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Dart.edge.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} (d : G.Dart), d.edge = s(d.toProd.1, d.toProd.2)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.whiskerRight_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.AddMon C) {Y Z : CategoryTheory.AddMon C} (f : Y ⟶ Z),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom
-- Mathlib.Analysis.ODE.PicardLindelof
/-- A key step in the inductive case of `dist_iterate_next_apply_le`  -/
ODE.FunSpace.dist_comp_iterate_next_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r) (n : ℕ) (t : ↑(Set.Icc tmin tmax)) {α β : ODE.FunSpace t₀ x₀ r L},
  dist (((ODE.FunSpace.next hf hx)^[n] α).toFun t) (((ODE.FunSpace.next hf hx)^[n] β).toFun t) ≤
      (↑K * |↑t - ↑t₀|) ^ n / ↑n.factorial * dist α β →
    dist (f (↑t) (((ODE.FunSpace.next hf hx)^[n] α).toFun t)) (f (↑t) (((ODE.FunSpace.next hf hx)^[n] β).toFun t)) ≤
      ↑K ^ (n + 1) * |↑t - ↑t₀| ^ n / ↑n.factorial * dist α β
-- Lean.DocString.Types
/-- An ordered list.
 -/
Lean.Doc.Block.ol : {i : Type u} → {b : Type v} → ℤ → Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block i b
-- Init.Data.SInt.Bitwise
Int64.xor_neg_one : ∀ {a : Int64}, a ^^^ -1 = ~~~a
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.instFromJsonOptions : Lean.FromJson Lean.Lsp.DeleteFile.Options
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
_private.Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification.0.NumberField.InfinitePlace.termStab : Lean.ParserDescr
-- Mathlib.Data.Part
Part.right_dom_of_mod_dom : ∀ {α : Type u_1} [inst : Mod α] {a b : Part α}, (a % b).Dom → b.Dom
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_inter_eq_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∈ t₂) → (t₁ ∩ t₂).size = t₁.size
-- Mathlib.Topology.ContinuousMap.StarOrdered
ContinuousMap.instStarOrderedRingOfContinuousSqrt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : PartialOrder R] [inst_2 : NonUnitalSemiring R]
  [inst_3 : StarRing R] [StarOrderedRing R] [inst_5 : TopologicalSpace R] [inst_6 : ContinuousStar R]
  [inst_7 : IsTopologicalSemiring R] [ContinuousSqrt R], StarOrderedRing C(α, R)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Mon C),
  CategoryTheory.IsMonHom (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F).hom
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mk.inj : ∀ {R : Type u} {A : Type v} {inst : CommSemiring R} {inst_1 : StarRing R} {inst_2 : Semiring A} {inst_3 : StarRing A}
  {inst_4 : Algebra R A} {inst_5 : StarModule R A} {toSubalgebra : Subalgebra R A}
  {star_mem' : ∀ {a : A}, a ∈ toSubalgebra.carrier → star a ∈ toSubalgebra.carrier} {toSubalgebra_1 : Subalgebra R A}
  {star_mem'_1 : ∀ {a : A}, a ∈ toSubalgebra_1.carrier → star a ∈ toSubalgebra_1.carrier},
  { toSubalgebra := toSubalgebra, star_mem' := star_mem' } =
      { toSubalgebra := toSubalgebra_1, star_mem' := star_mem'_1 } →
    toSubalgebra = toSubalgebra_1
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.instReprHeapNode.repr : {α : Type u_1} → [Repr α] → Batteries.BinomialHeap.Imp.HeapNode α → ℕ → Std.Format
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.lintegral_nnnorm_condExpIndSMul_le : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  ∫⁻ (a : α), ↑‖↑↑(MeasureTheory.condExpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊
-- Mathlib.RingTheory.LocalRing.Etale
/-- For a monogenic étale extension of local rings, the minimal polynomial of `β`
maps to the minimal polynomial of `β mod m_S` over the residue field.  -/
IsLocalRing.minpoly_map_residue : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing S] [inst_4 : IsLocalRing R] [inst_5 : Module.Finite R S] [inst_6 : FaithfulSMul R S]
  [Algebra.Etale R S] {β : S},
  R[β] = ⊤ →
    Polynomial.map (IsLocalRing.residue R) (minpoly R β) =
      minpoly (IsLocalRing.ResidueField R) ((IsLocalRing.residue S) β)
-- Mathlib.Algebra.RingQuot
RingQuot.instInhabited : {R : Type uR} → [inst : Semiring R] → (r : R → R → Prop) → Inhabited (RingQuot r)
-- Mathlib.CategoryTheory.Opposites
/-- The equivalence between isomorphisms of the form `A ≅ B` and `B.unop ≅ A.unop`.

Note this is definitionally the same as the other three variants:
* `(Opposite.op A ≅ B) ≃ (B.unop ≅ A)`
* `(A ≅ Opposite.op B) ≃ (B ≅ A.unop)`
* `(Opposite.op A ≅ Opposite.op B) ≃ (B ≅ A)`
 -/
CategoryTheory.isoOpEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (A B : Cᵒᵖ) → (A ≅ B) ≃ (Opposite.unop B ≅ Opposite.unop A)
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
/-- The right unitors are given by equalities  -/
CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b),
  CategoryTheory.Bicategory.rightUnitor f = CategoryTheory.eqToIso ⋯
-- Lean.Meta.Basic
Lean.Meta.instInhabitedContext.default : Lean.Meta.Context
-- Mathlib.Data.Fin.Basic
Fin.natCast_eq_last : ∀ (n : ℕ), ↑n = Fin.last n
-- Lean.Message
Lean.TraceData.mk.injEq : ∀ (cls : Lean.Name) (result? : Option Lean.TraceResult) (startTime stopTime : Float) (collapsed : Bool) (tag : String)
  (cls_1 : Lean.Name) (result?_1 : Option Lean.TraceResult) (startTime_1 stopTime_1 : Float) (collapsed_1 : Bool)
  (tag_1 : String),
  ({ cls := cls, result? := result?, startTime := startTime, stopTime := stopTime, collapsed := collapsed,
        tag := tag } =
      { cls := cls_1, result? := result?_1, startTime := startTime_1, stopTime := stopTime_1, collapsed := collapsed_1,
        tag := tag_1 }) =
    (cls = cls_1 ∧
      result? = result?_1 ∧ startTime = startTime_1 ∧ stopTime = stopTime_1 ∧ collapsed = collapsed_1 ∧ tag = tag_1)
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.realize.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : L.Term α → Sort u_4) (k : α)
  (h_1 : (k : α) → motive (FirstOrder.Language.var k))
  (h_2 : (l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.var k with
    | FirstOrder.Language.var k => h_1 k
    | FirstOrder.Language.func f ts => h_2 l f ts) =
    h_1 k
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mk_mem_target : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] (e' : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B}
  {y : F}, (b, y) ∈ e'.target ↔ b ∈ e'.baseSet
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.BitVecValue : Type
-- Mathlib.Algebra.Ring.TransferInstance
/-- Transfer `NonUnitalCommSemiring` across an `Equiv`  -/
Equiv.nonUnitalCommSemiring : {α : Type u_1} → {β : Type u_2} → α ≃ β → [NonUnitalCommSemiring β] → NonUnitalCommSemiring α
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.besselPotential_zero : ∀ (E : Type u_1) (F : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F],
  TemperedDistribution.besselPotential E F 0 = ContinuousLinearMap.id ℂ (TemperedDistribution E F)
-- Mathlib.Order.Disjointed
/-- `disjointed f` is the unique sequence that is pairwise disjoint and has the same partial sups
as `f`.  -/
disjointed_unique' : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] {f d : ι → α},
  Pairwise (Function.onFun Disjoint d) → partialSups d = partialSups f → d = disjointed f
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs : aig.RefVec w)
  (bit : aig.Ref),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastShiftConcat aig { lhs := lhs, bit := bit } =
    Std.Tactic.BVDecide.BVExpr.bitblast.blastZeroExtend aig
      { w := 1 + w, vec := ((Std.Sat.AIG.RefVec.emptyWithCapacity (w + 1)).push bit).append lhs }
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.Monadic.isPlausibleIndirectOutput_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerable α] {it : Std.IterM Id α} {out : α},
  it.IsPlausibleIndirectOutput out ↔
    ∃ n, (it.internalState.next.bind fun x => Std.PRange.succMany? n x) = some out ∧ out < it.internalState.upperBound