mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonParameterInformation : Lean.ToJson Lean.Lsp.ParameterInformation
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.rIso_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {adj₁ adj₂ : a ⟶ b}
  (e : adj₁ ≅ adj₂), (CategoryTheory.Bicategory.Adj.rIso e).inv = e.hom.τr
-- Mathlib.Algebra.Group.Units.Equiv
MulEquiv.inv.eq_1 : ∀ (G : Type u_6) [inst : DivisionCommMonoid G],
  MulEquiv.inv G = { toFun := Inv.inv, invFun := Inv.inv, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts
/-- The monoidal structure coming from finite coproducts is symmetric.
 -/
CategoryTheory.symmetricOfHasFiniteCoproducts : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasInitial C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] → CategoryTheory.SymmetricCategory C
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₁.eq_1 : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F),
  AlgebraicTopology.DoldKan.Compatibility.equivalence₁ hF =
    (AlgebraicTopology.DoldKan.Compatibility.equivalence₀ eA e').changeFunctor hF
-- Mathlib.Algebra.Free
FreeAddMagma.traverse_pure : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : α), traverse F (pure x) = pure <$> F x
-- Mathlib.RepresentationTheory.Rep.Basic
/-- A predicate for representations that fix every element.  -/
Rep.IsTrivial : {k : Type u} → {G : Type v} → [inst : Ring k] → [inst_1 : Monoid G] → Rep.{u_1, u, v} k G → Prop
-- Mathlib.CategoryTheory.Types.Basic
equivEquivIso_inv : ∀ {X Y : Type u} (e : X ≅ Y), equivEquivIso.symm e = e.toEquiv
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
/-- The functor `F.mapDerivedCategory` is induced
by `F.mapHomotopyCategory (ComplexShape.up ℤ)`.  -/
CategoryTheory.Functor.mapDerivedCategoryFactorsh : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    [inst_1 : CategoryTheory.Abelian C₁] →
      [inst_2 : HasDerivedCategory C₁] →
        {C₂ : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_4 : CategoryTheory.Abelian C₂] →
              [inst_5 : HasDerivedCategory C₂] →
                (F : CategoryTheory.Functor C₁ C₂) →
                  [inst_6 : F.Additive] →
                    [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F] →
                      [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] →
                        DerivedCategory.Qh.comp F.mapDerivedCategory ≅
                          (F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh
-- Mathlib.RingTheory.Valuation.Basic
Valuation.val_lt_one_iff : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  (v : Valuation K Γ₀) {x : K}, x ≠ 0 → (v x < 1 ↔ 1 < v x⁻¹)
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.quotPrecheck.allowSectionVars : Lean.Option Bool
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
SubMulAction.ofStabilizer.snoc.eq_1 : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {a : α} {n : ℕ}
  (x : Fin n ↪ ↥(SubMulAction.ofStabilizer G a)),
  SubMulAction.ofStabilizer.snoc x =
    Fin.Embedding.snoc (x.trans (Function.Embedding.subtype fun x => x ∈ SubMulAction.ofStabilizer G a)) ⋯
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.isLocallyFiniteMeasure_of_smulInvariant : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α},
  IsOpen U → U.Nonempty → μ U ≠ ⊤ → MeasureTheory.IsLocallyFiniteMeasure μ
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : MeasurableSpace α] [inst_1 : SizeOf α] (posPart negPart : MeasureTheory.Measure α)
  [posPart_finite : MeasureTheory.IsFiniteMeasure posPart] [negPart_finite : MeasureTheory.IsFiniteMeasure negPart]
  (mutuallySingular : posPart.MutuallySingular negPart),
  sizeOf
      { posPart := posPart, negPart := negPart, posPart_finite := posPart_finite, negPart_finite := negPart_finite,
        mutuallySingular := mutuallySingular } =
    1 + sizeOf posPart + sizeOf negPart + sizeOf posPart_finite + sizeOf negPart_finite + sizeOf mutuallySingular
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodePi.match_3.splitter : (motive : (n : ℕ) → (f : Fin n → ℕ) → Fin (Fin.prod f) → Sort u_1) →
  (n : ℕ) →
    (f : Fin n → ℕ) →
      (x : Fin (Fin.prod f)) →
        ((x : Fin 0 → ℕ) → (x_1 : Fin (Fin.prod x)) → motive 0 x x_1) →
          ((n : ℕ) → (f : Fin (n + 1) → ℕ) → (x : ℕ) → (hx : x < Fin.prod f) → motive n.succ f ⟨x, hx⟩) → motive n f x
-- Std.Do.SPred.SPred
Std.Do.SPred.ext_cons_iff : ∀ {σs : List (Type u)} {σ : Type u} {P Q : Std.Do.SPred (σ :: σs)}, P = Q ↔ ∀ (s : σ), P s = Q s
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.UnfoldLift.modifyGet : ∀ {m : Type u → Type v} {n : Type u → Type u_1} {σ α : Type u} [inst : MonadLift m n] [inst_1 : MonadStateOf σ m]
  (f : σ → α × σ), MonadStateOf.modifyGet f = monadLift (MonadStateOf.modifyGet f)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.sum_filter_pairs_eq_sum_powersetCard_sum : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : DecidableEq σ] [inst_2 : Fintype σ] (k : ℕ)
  (f : Finset σ × σ → MvPolynomial σ R),
  ∑ t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k with t.1.card = k, f t =
    ∑ A ∈ Finset.powersetCard k Finset.univ, ∑ j ∈ A, f (A, j)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instLeftCancelSemigroupOfMulOpposite : {M : Type u_1} → [LeftCancelSemigroup Mᵐᵒᵖ] → LeftCancelSemigroup Mᵈᵐᵃ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂).getKey? k = none
-- Init.Data.List.MinMaxOn
List.max_map : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [inst_2 : Max β] [Std.IsLinearPreorder β]
  [Std.LawfulOrderLeftLeaningMax β] {xs : List α} {f : α → β} (h : xs ≠ []),
  (List.map f xs).max ⋯ = f (List.maxOn f xs h)
-- Mathlib.Order.Ideal
/-- **Alias** of the forward direction of `Order.Ideal.isProper_iff_top_notMem`. -/
Order.Ideal.IsProper.top_notMem : ∀ {P : Type u_1} [inst : LE P] [inst_1 : OrderTop P] {I : Order.Ideal P}, I.IsProper → ⊤ ∉ I
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_sub_pi_div_two : ∀ (θ : Real.Angle), (θ - ↑(Real.pi / 2)).cos = θ.sin
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Structure for quickly initializing a lazy discrimination tree with a large number
of elements using concurrent functions for generating entries.

This preliminary structure is converted to a `RefinedDiscrTree` via `toRefinedDiscrTree`.
 -/
Lean.Meta.RefinedDiscrTree.PreDiscrTree : Type → Type
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.filter_eq : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : l.HasBasis p s), ⋯.filter = l
-- Mathlib.Data.Finset.Defs
/-- The underlying multiset  -/
Finset.val : {α : Type u_4} → Finset α → Multiset α
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.isCorepresentable_comp_uliftFunctor_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)},
  (F.comp CategoryTheory.uliftFunctor.{w, v}).IsCorepresentable ↔ F.IsCorepresentable
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_iff_isSuccLimit_of_not_isMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α], ¬IsMin a → (Order.IsSuccPrelimit a ↔ Order.IsSuccLimit a)
-- Mathlib.Data.Set.Sups
Set.sups_subset_self : ∀ {α : Type u_2} [inst : SemilatticeSup α] {s : Set α}, s ⊻ s ⊆ s ↔ SupClosed s
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result.hasFailed : Lean.Meta.Grind.Result → Bool
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_def : MeasureTheory.volume = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Signature.mk.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (name : Lean.Name) (levelParams : List Lean.Name) (type : Lean.Expr)
  (params : Array (Lean.Compiler.LCNF.Param pu)) (safe : Bool),
  sizeOf { name := name, levelParams := levelParams, type := type, params := params, safe := safe } =
    1 + sizeOf name + sizeOf levelParams + sizeOf type + sizeOf params + sizeOf safe
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.coe_dualMap : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : SpecialLinearGroup R V) [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V], ↑A.dualMap = (↑A).dualMap
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
linearIndependent_unique_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] {v : ι → M} [inst_5 : Unique ι],
  LinearIndependent R v ↔ v default ≠ 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_lt_add_left : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [inst_1 : LT α] [AddLeftStrictMono α], x ≠ ⊤ → y < z → x + y < x + z
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.mem_center_iff : ∀ {G : Type u_1} [inst : Group G] {z : G}, z ∈ Subgroup.center G ↔ ∀ (g : G), g * z = z * g
-- Mathlib.CategoryTheory.Core
/-- The functor `functorToCore (inclusion C)` is isomorphic to the identity on `Core C`.  -/
CategoryTheory.Core.functorToCoreInclusionIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Core.functorToCore (CategoryTheory.Core.inclusion C) ≅
      CategoryTheory.Functor.id (CategoryTheory.Core C)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_functor_obj : ∀ {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.Cocone F)ᵒᵖ),
  CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.functor.obj c =
    CategoryTheory.Limits.coneLeftOpOfCocone (Opposite.unop c)
-- Mathlib.Algebra.Module.Equiv.Opposite
/-- The function `op` is a linear equivalence.  -/
MulOpposite.opLinearEquiv : (R : Type u) → {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M ≃ₗ[R] Mᵐᵒᵖ
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosed.roots_eq_zero_iff : ∀ {k : Type u} [inst : Field k] [IsSepClosed k] {p : Polynomial k},
  p.Separable → (p.roots = 0 ↔ p = Polynomial.C (p.coeff 0))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.HasPullback.comp_left_right_iff_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z Z' : C} {f : X ⟶ Z} {g : Y ⟶ Z'} (i : Z ⟶ Z')
  [inst_1 : CategoryTheory.IsIso i],
  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) g ↔
    CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.inv i))
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesParams : Type
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_injective : ∀ {R : Type u_1} [inst : Semiring R], Function.Injective ⇑Polynomial.toLaurent
-- Lean.Meta.Tactic.Grind.Types
/-- Executes `f` to each term in the equivalence class containing `e`, and stops as soon as `f` returns `true`.
 -/
Lean.Meta.Grind.findEqc : Lean.Expr → (Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Bool) → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddCommMonCat.instIsRightAdjointForgetAddMonoidHomCarrier : (CategoryTheory.forget AddCommMonCat).IsRightAdjoint
-- Lean.Elab.Match
Lean.Elab.Term.PatternElabException.pathToIndex : Lean.Elab.Term.PatternElabException → List ℕ
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (X : CategoryTheory.FreeMonoidalCategory C)
  {Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C} (f : Y₁.Hom Y₂),
  sizeOf (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f) = 1 + sizeOf X + sizeOf Y₁ + sizeOf Y₂ + sizeOf f
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.ext : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] {f g : E₁ →ₚ[R] E₂}, (∀ (x : E₁), f x = g x) → f = g
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ]
  [inst_6 : IsLocalization.AtPrime Rₚ p] [inst_7 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ]
  [inst_9 : Algebra S Sₚ] [inst_10 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
  [inst_11 : Algebra Rₚ Sₚ] [inst_12 : IsDomain R] [inst_13 : IsDedekindDomain S] [inst_14 : Module.IsTorsionFree R S]
  [inst_15 : Algebra R Sₚ] [inst_16 : IsScalarTower R S Sₚ] [inst_17 : IsScalarTower R Rₚ Sₚ] [p.IsMaximal] (hp : p ≠ ⊥)
  (P : ↑(p.primesOver S)),
  (IsLocalRing.maximalIdeal Rₚ).inertiaDeg' ↑((IsDedekindDomain.primesOverEquivPrimesOver p Rₚ Sₚ hp) P) =
    p.inertiaDeg' ↑P
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
/-- Given an entourage `U` and a time `n`, a dynamical net has a smaller cardinality than
a dynamical cover. This lemma is the first of two key results to compare two versions of
topological entropy: with cover and with nets, the second being `coverMincard_le_netMaxcard`.  -/
Dynamics.IsDynNetIn.card_le_card_of_isDynCoverOf : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} {F : Set X} {s t : Finset X},
  Dynamics.IsDynNetIn T F U n ↑s → Dynamics.IsDynCoverOf T F U n ↑t → s.card ≤ t.card
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, k ∉ m₂ → (m₁ \ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Batteries.Data.AssocList
Batteries.AssocList.forIn_eq : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [inst : Monad m] (l : Batteries.AssocList α β)
  (init : δ) (f : α × β → δ → m (ForInStep δ)), forIn l init f = forIn l.toList init f
-- Mathlib.Data.Fintype.Sets
Finset.fintypeCoeSort : {α : Type u} → (s : Finset α) → Fintype ↥s
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.ne.sizeOf_spec : ∀ (lhs rhs : ℕ) (proof : Lean.Expr),
  sizeOf (Mathlib.Tactic.Order.AtomicFact.ne lhs rhs proof) = 1 + sizeOf lhs + sizeOf rhs + sizeOf proof
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The restriction map `M.map f` of a presheaf of modules `M`, bundled as a semilinear map
along the ring map `R.map f`.  -/
PresheafOfModules.restrictₛₗ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (M : PresheafOfModules R) → {X Y : Cᵒᵖ} → (f : X ⟶ Y) → ↑(M.obj X) →ₛₗ[RingCat.Hom.hom (R.map f)] ↑(M.obj Y)
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
/-- Radius such that every point of the space is within `R` of `carrier`.  -/
Delone.DeloneSet.coveringRadius : {X : Type u_3} → [inst : MetricSpace X] → Delone.DeloneSet X → NNReal
-- Init.Data.BEq
instEquivBEqOfLawfulBEq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α], EquivBEq α
-- Mathlib.Data.EReal.Basic
EReal.coe_ennreal_mul : ∀ (x y : ENNReal), ↑(x * y) = ↑x * ↑y
-- Mathlib.Algebra.GroupWithZero.Regular
IsRightRegular.mul_right_eq_zero_iff : ∀ {R : Type u_1} [inst : MulZeroClass R] {a b : R}, IsRightRegular b → (a * b = 0 ↔ a = 0)
-- Mathlib.Algebra.Field.Basic
Lex.instDivisionRing : {K : Type u_1} → [DivisionRing K] → DivisionRing (Lex K)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.smulZeroClass : {R : Type u} → [inst : Semiring R] → {S : Type u_1} → [SMulZeroClass S R] → SMulZeroClass S (Polynomial R)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.map₂_rightUnitor_hom_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b))
      (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b))
        (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom) h))
-- Mathlib.Order.Atoms
Pi.eq_bot_iff : ∀ {ι : Type u_4} {π : ι → Type u} [inst : (i : ι) → Bot (π i)] {f : (i : ι) → π i}, f = ⊥ ↔ ∀ (i : ι), f i = ⊥
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.ne_zero : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {μ : R},
  t.HasPrimitiveVectorWith m μ → m ≠ 0
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
basisOfLinearIndependentOfCardEqFinrank_repr_apply : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {b : ι → V} (lin_ind : LinearIndependent K b)
  (card_eq : Fintype.card ι = Module.finrank K V) (x : V),
  (basisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr x =
    lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range b)) LinearMap.id ⋯) x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_forall_contains_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.DTreeMap α (fun x => Unit) cmp}, (∀ (k : α), t₁.contains k = t₂.contains k) → t₁.Equiv t₂
-- Mathlib.RingTheory.LocalRing.LocalSubring
/-- `A` dominates `B` if and only if `B ≤ A` (as subrings) and `m_A ∩ B = m_B`.  -/
LocalSubring.le_def : ∀ {R : Type u_1} [inst : CommRing R] {A B : LocalSubring R},
  A ≤ B ↔ ∃ (h : A.toSubring ≤ B.toSubring), IsLocalHom (Subring.inclusion h)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.PointedMap.mk.congr_simp : ∀ {Γ : Type u} {Γ' : Type v} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f f_1 : Γ → Γ') (e_f : f = f_1)
  (map_pt' : f default = default), { f := f, map_pt' := map_pt' } = { f := f_1, map_pt' := ⋯ }
-- Mathlib.Order.Filter.Cofinite
boundary_principal : ∀ {α : Type u_2} (s : Set α), Coheyting.boundary (Filter.principal s) = ⊥
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.comp_appIso : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (U : X.Opens),
  AlgebraicGeometry.Scheme.Hom.appIso (CategoryTheory.CategoryStruct.comp f g) U =
    CategoryTheory.Functor.mapIso Z.presheaf (CategoryTheory.eqToIso ⋯).op ≪≫
      AlgebraicGeometry.Scheme.Hom.appIso g ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) ≪≫
        AlgebraicGeometry.Scheme.Hom.appIso f U
-- Init.Data.Order.Ord
List.instLawfulBEqOrd : ∀ {α : Type u_1} [inst : Ord α] [inst_1 : BEq α] [Std.LawfulBEqOrd α], Std.LawfulBEqOrd (List α)
-- Mathlib.CategoryTheory.Types.Basic
/-- A morphism in `Type _` is an epimorphism if and only if it is surjective.  -/
CategoryTheory.ofHom_epi_iff_surjective : ∀ {X Y : Type u} (f : X → Y), CategoryTheory.Epi (TypeCat.ofHom f) ↔ Function.Surjective f
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.coe_addRight : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : SeparatelyContinuousAdd G] (a : G),
  ⇑(Homeomorph.addRight a) = fun x => x + a
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_mk : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (f : A → B) (h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x)
  (h₂ : { toFun := f, map_smul' := h₁ }.toFun 0 = 0)
  (h₃ :
    ∀ (x y : A),
      { toFun := f, map_smul' := h₁ }.toFun (x + y) =
        { toFun := f, map_smul' := h₁ }.toFun x + { toFun := f, map_smul' := h₁ }.toFun y)
  (h₄ :
    ∀ (x y : A),
      { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
        { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
          { toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y),
  ⇑{ toFun := f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } = f
-- Mathlib.Order.Interval.Set.Basic
Set.decidableMemIic.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {b x : α} [inst_1 : Decidable (x ≤ b)], Set.decidableMemIic = inst_1
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.Total.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  {k l : CategoryTheory.Limits.ColimitPresentation.Total P} [inst_3 : SizeOf C] [inst_4 : SizeOf J]
  [inst_5 : (a : J) → SizeOf (I a)] (base : k.fst ⟶ l.fst) (hom : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map base) =
        CategoryTheory.CategoryStruct.comp hom ((P l.fst).ι.app l.snd))
      CategoryTheory.Limits.ColimitPresentation.Total.Hom.w._autoParam),
  sizeOf { base := base, hom := hom, w := w } = 1 + sizeOf base + sizeOf hom + sizeOf w
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.mk_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Subobject X),
  CategoryTheory.Subobject.mk P.arrow = P
-- Mathlib.Algebra.Free
FreeMagma.map_of : ∀ {α : Type u} {β : Type v} (f : α → β) (x : α), (FreeMagma.map f) (FreeMagma.of x) = FreeMagma.of (f x)
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
BoxIntegral.Box.measurableSet_coe : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) [Countable ι], MeasurableSet ↑I
-- ProofWidgets.Cancellable
ProofWidgets.CheckRequestResponse.running : ProofWidgets.CheckRequestResponse
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.constVAdd_toEquiv : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [inst_3 : IsIsometricVAdd G X] (c : G), (IsometryEquiv.constVAdd c).toEquiv = AddAction.toPerm c
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndep.condIndep : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : ι → MeasurableSpace Ω},
  ProbabilityTheory.iCondIndep m' hm' m μ → ∀ {i j : ι}, i ≠ j → ProbabilityTheory.CondIndep m' (m i) (m j) hm' μ