mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- See also `uliftYonedaEquiv_naturality'` for a more general version.  -/
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X Y : C} {F : CategoryTheory.Sheaf J (Type (max v v'))}
  (f : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) =
    J.uliftYonedaEquiv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).map g) f)
-- Mathlib.Data.String.Lemmas
String.IsSuffix.eq_1 : ∀ (x x_1 : String), x.IsSuffix x_1 = (x.toList <:+ x_1.toList)
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Arg.updateTypeImp : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Arg pu → Lean.Expr → Lean.Compiler.LCNF.Arg pu
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {l : List α} {k : α}
  {h' : k ∈ t.insertMany l} (contains : k ∈ t), (t.insertMany l).get k h' = t.get k contains
-- Mathlib.RingTheory.Ideal.Basis
/-- If `I : Ideal S` has a finite basis over `R`,
`x ∈ I` iff it is a linear combination of basis vectors.  -/
Basis.mem_ideal_iff' : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype ι] [inst_1 : CommSemiring R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] {I : Ideal S} (b : Module.Basis ι R ↥I) {x : S}, x ∈ I ↔ ∃ c, x = ∑ i, c i • ↑(b i)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.coe_comp : ∀ {M N K : SemiNormedGrp₁} (f : M ⟶ N) (g : N ⟶ K),
  ⇑↑(SemiNormedGrp₁.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑↑(SemiNormedGrp₁.Hom.hom g) ∘ ⇑↑(SemiNormedGrp₁.Hom.hom f)
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctor_ε : ∀ {M : Type u} [inst : AddMonoid M] {N : Type u'} [inst_1 : AddMonoid N] (F : M →+ N),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Discrete.addMonoidalFunctor F) =
    CategoryTheory.Discrete.eqToHom ⋯
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- The identity functor is fully faithful.  -/
CategoryTheory.Functor.FullyFaithful.id : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → (CategoryTheory.Functor.id C).FullyFaithful
-- Std.Time.Date.Unit.Month
Std.Time.Month.instReprOrdinal : Repr Std.Time.Month.Ordinal
-- Lean.Data.PersistentArray
Lean.instInhabitedPersistentArray.default : {α : Type u} → Lean.PersistentArray α
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.all_prop_eq : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice}, s.all P = s.copy.toList.all fun x => decide (P x)
-- Mathlib.CategoryTheory.Skeletal
/-- Convenience constructor for `ThinSkeleton`.  -/
CategoryTheory.ThinSkeleton.mk : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → C → CategoryTheory.ThinSkeleton C
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instSMul.eq_1 : ∀ {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [inst : (i : ι) → SMul α (M i)],
  Pi.instSMul = { smul := fun a f i => a • f i }
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_equiv : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {F' : Type u_3} [inst_2 : EquivLike F' R S]
  [inst_3 : RingEquivClass F' R S] (f : F'), RingHom.ker f = ⊥
-- Mathlib.Data.Set.Image
Set.preimage_const_of_notMem : ∀ {α : Type u_1} {β : Type u_2} {b : β} {s : Set β}, b ∉ s → (fun x => b) ⁻¹' s = ∅
-- Mathlib.Data.Finset.Basic
Finset.univ_finset_of_isEmpty : ∀ {α : Type u_4} [h : IsEmpty α], Set.univ = {∅}
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_bracket : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) (x : L) (m : ↥N), ↑⁅x, m⁆ = ⁅x, ↑m⁆
-- Mathlib.CategoryTheory.DinatTrans
/-- The commutativity square for a given morphism.  -/
CategoryTheory.DinatTrans.dinaturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)} (self : CategoryTheory.DinatTrans F G) {X Y : C}
  (f : X ⟶ Y) {Z : D} (h : (G.obj (Opposite.op X)).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app X)
      (CategoryTheory.CategoryStruct.comp (self.app X)
        (CategoryTheory.CategoryStruct.comp ((G.obj (Opposite.op X)).map f) h)) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op Y)).map f)
      (CategoryTheory.CategoryStruct.comp (self.app Y) (CategoryTheory.CategoryStruct.comp ((G.map f.op).app Y) h))
-- Mathlib.Data.List.Basic
List.filter_attach' : ∀ {α : Type u} (l : List α) (p : { a // a ∈ l } → Bool) [inst : DecidableEq α],
  List.filter p l.attach =
    List.map (Subtype.map id ⋯) (List.filter (fun x => decide (∃ (h : x ∈ l), p ⟨x, h⟩ = true)) l).attach
-- Mathlib.Topology.Algebra.AsymptoticCone
Finset.asymptoticCone_biUnion : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] {ι : Type u_4} (s : Finset ι)
  (f : ι → Set P), asymptoticCone k (⋃ i ∈ s, f i) = ⋃ i ∈ s, asymptoticCone k (f i)
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.instUniqueToTypeTerminal : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            [inst_3 : CategoryTheory.Limits.HasTerminal C] →
              [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) (CategoryTheory.forget C)] →
                Unique (CategoryTheory.ToType (⊤_ C))
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_ext₂_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] {X Y Z : C} {f : J → C}
  {g h :
    X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y (CategoryTheory.MonoidalCategoryStruct.tensorObj Z (⨁ f))},
  (∀ (j : J),
      CategoryTheory.CategoryStruct.comp g
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j))) =
        CategoryTheory.CategoryStruct.comp h
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.Limits.biproduct.π f j)))) →
    g = h
-- Init.Data.Option.Lemmas
Option.get_of_any_eq_true : ∀ {α : Type u_1} (p : α → Bool) (x : Option α) (h : Option.any p x = true), p (x.get ⋯) = true
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesRegistrationOptions.mk.inj : ∀ {watchers watchers_1 : Array Lean.Lsp.FileSystemWatcher},
  { watchers := watchers } = { watchers := watchers_1 } → watchers = watchers_1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by negation.  -/
ContinuousAddMonoidHom.neg : (E : Type u_6) → [inst : AddCommGroup E] → [inst_1 : TopologicalSpace E] → [IsTopologicalAddGroup E] → E →ₜ+ E
-- Mathlib.Algebra.Order.Floor.Defs
/-- A `FloorSemiring` is an ordered semiring over `α` with a function
`floor : α → ℕ` satisfying `∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x)`.
Note that many lemmas require a `LinearOrder`. Please see the above `TODO`.  -/
FloorSemiring : (α : Type u_4) → [Semiring α] → [PartialOrder α] → Type u_4
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_apply_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), toIcoMod hp a (a + p) = a
-- Init.Data.Fin.Fold
Fin.foldlM_add : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n k : ℕ} [inst : Monad m] [LawfulMonad m] (f : α → Fin (n + k) → m α),
  Fin.foldlM (n + k) f = fun x =>
    Fin.foldlM n (fun x i => f x (Fin.castLE ⋯ i)) x >>= Fin.foldlM k fun x i => f x (Fin.natAdd n i)
-- Mathlib.Tactic.SetNotationForOrder
/-- Delaborate `x < y` into `x ⊂ y` if the type is tagged with `@[use_set_notation_for_order]`.  -/
Mathlib.Meta.SetNotationForOrder.delabLt : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Internal.Do.Triple.SpecLemmas
_private.Std.Internal.Do.Triple.SpecLemmas.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Mathlib.Order.Category.BddDistLat
BddDistLat.Iso.mk_hom : ∀ {α β : BddDistLat} (e : ↑α.toDistLat ≃o ↑β.toDistLat),
  (BddDistLat.Iso.mk e).hom =
    BddDistLat.ofHom
      (have __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
-- Mathlib.Logic.Equiv.List
Encodable.encodeList.eq_1 : ∀ {α : Type u_1} [inst : Encodable α], Encodable.encodeList [] = 0
-- Mathlib.Topology.Compactness.Compact
/-- Complement of a set belongs to `coclosedCompact` if and only if its closure is compact.  -/
Filter.compl_mem_coclosedCompact : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, sᶜ ∈ Filter.coclosedCompact X ↔ IsCompact (closure s)
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_mono_left : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (ϕ : τ → α → β) (s : Set α)
  {f₁ f₂ : Filter τ}, f₁ ≤ f₂ → omegaLimit f₁ ϕ s ⊆ omegaLimit f₂ ϕ s
-- Mathlib.RingTheory.Unramified.LocalStructure
_private.Mathlib.RingTheory.Unramified.LocalStructure.0.Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top_aux₁ : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Ideal R)
  [inst_3 : P.IsPrime] (x : S),
  R[x] = ⊤ →
    Ideal.map (Polynomial.mapRingHom (algebraMap R P.ResidueField)) (RingHom.ker (Polynomial.aeval x).toRingHom) =
      RingHom.ker (Polynomial.aeval (1 ⊗ₜ[R] x)).toRingHom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_diff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.Const.get? (m₁.diff m₂ ⋯) k =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then none else Std.DTreeMap.Internal.Impl.Const.get? m₁ k
-- Mathlib.Order.Defs.Unbundled
/-- An upper set relative to a predicate `P` is a set such that all elements satisfy `P` and
any element greater than one of its members and satisfying `P` is also a member.  -/
IsRelUpperSet : {α : Type u_1} → [LE α] → Set α → (α → Prop) → Prop
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
CategoryTheory.preservesLimits_preadditiveCoyonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : C),
  CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveCoyonedaObj X)
-- Lean.Server.Requests
/-- NB: This method may only be called in `initialize` blocks (user or builtin).

Register another handler to invoke after the last one registered for a method.
At least one handler for the method must have already been registered to perform
chaining.

For more details on the registration of a handler, see `registerLspRequestHandler`.  -/
Lean.Server.chainLspRequestHandler : String →
  (paramType : Type) →
    [Lean.FromJson paramType] →
      (respType : Type) →
        [Lean.FromJson respType] →
          [Lean.ToJson respType] →
            (paramType → Lean.Server.RequestTask respType → Lean.Server.RequestM (Lean.Server.RequestTask respType)) →
              IO Unit
-- Mathlib.GroupTheory.Coset.Basic
QuotientAddGroup.leftRel_prod : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {β : Type u_2} [inst_1 : AddGroup β] (s' : AddSubgroup β),
  QuotientAddGroup.leftRel (s.prod s') = (QuotientAddGroup.leftRel s).prod (QuotientAddGroup.leftRel s')
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_swap : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β}, Measurable Prod.swap
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_lt_fib : ∀ {m : ℕ}, 2 ≤ m → ∀ {n : ℕ}, Nat.fib m < Nat.fib n ↔ m < n
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 2} (φ : R₁ ⟶ R₂),
  R₁.Exact →
    R₂.Exact →
      CategoryTheory.Mono
          (R₂.map' 0 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_9
            CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
          CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
            CategoryTheory.Epi
              (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.category_comp_right : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {X Y Z : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  (α : CategoryTheory.Limits.CatCospanTransformMorphism X Y) (β : CategoryTheory.Limits.CatCospanTransformMorphism Y Z),
  (CategoryTheory.CategoryStruct.comp α β).right = CategoryTheory.CategoryStruct.comp α.right β.right
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Checking exact colimits of shape `Discrete ℕ` is enough for countable AB4, provided that the
category has finite biproducts and finite limits.
 -/
CategoryTheory.CountableAB4.of_hasExactColimitsOfShape_nat : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteLimits C]
  [inst_4 : CategoryTheory.Limits.HasCountableCoproducts C]
  [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete ℕ) C], CategoryTheory.CountableAB4 C
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, List.find? (fun x => x.1 == k) m.toList = none ↔ k ∉ m
-- Batteries.Tactic.ShowUnused
/-- `#show_unused decl1 decl2 ..` will highlight every theorem or definition in the current file
not involved in the definition of declarations `decl1`, `decl2`, etc. The result is shown
both in the message on `#show_unused`, as well as on the declarations themselves.
```
def foo := 1
def baz := 2
def bar := foo
#show_unused bar -- highlights `baz`
```
 -/
Batteries.Tactic.ShowUnused.«command#show_unused___» : Lean.ParserDescr
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_Iic_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsCodirectedOrder α] {a : α} {f : β → ↑(Set.Iic a)} {l : Filter β},
  Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun x => ↑(f x)) l Filter.atBot
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
affineSpan_prod_eq : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] (s : Set P) (t : Set Q), affineSpan k (s ×ˢ t) = (affineSpan k s).prod (affineSpan k t)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- Get the common section for a reflexive pair.  -/
CategoryTheory.commonSection : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {A B : C} → (f g : A ⟶ B) → [CategoryTheory.IsReflexivePair f g] → B ⟶ A
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.MkHInjTypeResult.mk : Lean.Expr → List Lean.Level → ℕ → Lean.Meta.MkHInjTypeResult✝
-- Init.Data.Range.Polymorphic.Char
Char.instLawfulHasSize : Std.Rxc.LawfulHasSize Char
-- Mathlib.CategoryTheory.Shift.Basic
/-- the family of shift functors  -/
CategoryTheory.ShiftMkCore.F : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddMonoid A] → CategoryTheory.ShiftMkCore C A → A → CategoryTheory.Functor C C
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.inr_inr_pushoutAssoc_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Z₁ Z₂ : C} (g₁ : Z₁ ⟶ X₁) (g₂ : Z₁ ⟶ X₂)
  (g₃ : Z₂ ⟶ X₂) (g₄ : Z₂ ⟶ X₃) [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂]
  [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄]
  [inst_4 :
    CategoryTheory.Limits.HasPushout g₁
      (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pushout.inr g₁
          (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
        (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) =
    CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂))
      g₄
-- Mathlib.Order.UpperLower.Closure
LowerSet.lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] (s : LowerSet α), lowerClosure ↑s = s
-- Mathlib.Order.Lattice
instAssociativeMin_mathlib : ∀ {α : Type u} [inst : SemilatticeInf α], Std.Associative fun x1 x2 => x1 ⊓ x2
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_X : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {s : σ},
  m.leadingCoeff (MvPolynomial.X s) = 1
-- Aesop.RuleSet
/-- The simprocs array must contain at least one `Simprocs` structure, for the
same reason as above.
 -/
Aesop.LocalRuleSet.simprocsArrayNonempty : ∀ (self : Aesop.LocalRuleSet), 0 < self.simprocsArray.size
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.IsDynCoverOf.eq_1 : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ) (s : Set X),
  Dynamics.IsDynCoverOf T F U n s = (Dynamics.dynEntourage T U n).IsCover F s
-- Mathlib.Order.Interval.Basic
NonemptyInterval.snd_dual : ∀ {α : Type u_1} [inst : LE α] (s : NonemptyInterval α),
  (NonemptyInterval.dual s).toProd.2 = OrderDual.toDual s.toProd.1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.hom_inv_id_tensor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f.inv h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id V) g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id V) h)
-- Mathlib.Data.Nat.Upto
/-- Lift the "greater than" relation on natural numbers to `Nat.Upto`.  -/
Nat.Upto.GT : (p : ℕ → Prop) → Nat.Upto p → Nat.Upto p → Prop
-- Mathlib.Topology.Order.Basic
IsOpen.exists_Ioo_subset : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [Nontrivial α] {s : Set α},
  IsOpen s → s.Nonempty → ∃ a b, a < b ∧ Set.Ioo a b ⊆ s
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_attach : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β) (f : β → α),
  (s.attach.inf fun x => f ↑x) = s.inf f
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
_private.Mathlib.RingTheory.PowerSeries.WeierstrassPreparation.0.PowerSeries.IsWeierstrassDivisorAt.seq.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The linear map associated to the conjugate transpose of a matrix corresponding to two
orthonormal bases is the adjoint of the linear map associated to the matrix.  -/
Matrix.toLin_conjTranspose : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F] {m : Type u_5}
  {n : Type u_6} [inst_5 : Fintype m] [inst_6 : DecidableEq m] [inst_7 : Fintype n] [inst_8 : DecidableEq n]
  [inst_9 : FiniteDimensional 𝕜 E] [inst_10 : FiniteDimensional 𝕜 F] (v₁ : OrthonormalBasis n 𝕜 E)
  (v₂ : OrthonormalBasis m 𝕜 F) (A : Matrix m n 𝕜),
  (Matrix.toLin v₂.toBasis v₁.toBasis) A.conjTranspose = LinearMap.adjoint ((Matrix.toLin v₁.toBasis v₂.toBasis) A)
-- Batteries.Lean.Meta.InstantiateMVars
/-- Instantiate metavariables in the local context and type of the given
metavariable.
 -/
Lean.MVarId.instantiateMVars : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → [Lean.MonadError m] → Lean.MVarId → m Unit
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.toSeq_ofSeq : ∀ {α : Type u} (s : Stream'.Seq α), (↑s).toSeq = s
-- Mathlib.CategoryTheory.GradedObject.Unitor
/-- Given `F : C ⥤ D ⥤ D`, `X : C` and `Y : GradedObject J D`,
`((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y a` is an initial object
when `a : I × J` is such that `a.1 ≠ 0`.  -/
CategoryTheory.GradedObject.mapBifunctorObjSingle₀ObjIsInitial : {C : Type u_1} →
  {D : Type u_2} →
    {I : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
            [inst_2 : Zero I] →
              [inst_3 : DecidableEq I] →
                [inst_4 : CategoryTheory.Limits.HasInitial C] →
                  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) →
                    (X : C) →
                      [∀ (Y : D),
                            CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)] →
                        (Y : CategoryTheory.GradedObject J D) →
                          (a : I × J) →
                            a.1 ≠ 0 →
                              CategoryTheory.Limits.IsInitial
                                (((CategoryTheory.GradedObject.mapBifunctor F I J).obj
                                      ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
                                  Y a)
-- Init.Data.Range.Polymorphic.Iterators
Std.Rxc.Iterator.upwardEnumerableLe_of_isPlausibleIndirectOutput : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] {it : Std.Iter α} {out : α},
  it.IsPlausibleIndirectOutput out → ∃ a, it.internalState.next = some a ∧ Std.PRange.UpwardEnumerable.LE a out
-- Mathlib.Algebra.WithConv
WithConv.instDecidableEq : {A : Type u_2} → [DecidableEq A] → DecidableEq (WithConv A)