mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- Variant of `IsPushout.of_right` where `h₂₂` is induced from a morphism `h₂₃ : X₂₁ ⟶ X₂₃`, and
the universal property of the left square.

The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
|            |            |
v₁₁          v₁₂          v₁₃
↓            ↓            ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
```
 -/
CategoryTheory.IsPushout.of_left' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
  {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₃ : X₂₁ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃}
  (s : CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ h₂₃)
  (t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁),
  CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ (t.desc (CategoryTheory.CategoryStruct.comp h₁₂ v₁₃) h₂₃ ⋯)
-- Mathlib.Data.Tree.Basic
BinaryTree.numNodes.eq_2 : ∀ {α : Type u} (a : α) (l r : BinaryTree α), (BinaryTree.node a l r).numNodes = l.numNodes + r.numNodes + 1
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim_ι_ι_inv : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_5 : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)]
  {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j)
        (CategoryTheory.Limits.colimitCurrySwapCompColimIsoColimitCurryCompColim G).inv) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).obj k) j)
      (CategoryTheory.Limits.colimit.ι
        ((CategoryTheory.Functor.curry.obj ((CategoryTheory.Prod.swap K J).comp G)).comp CategoryTheory.Limits.colim) k)
-- Aesop.Stats.Basic
Aesop.ForwardRuleStateStats.mk.injEq : ∀ (ruleName : Aesop.RuleName) (clusterStateStats : Array Aesop.ForwardClusterStateStats) (ruleName_1 : Aesop.RuleName)
  (clusterStateStats_1 : Array Aesop.ForwardClusterStateStats),
  ({ ruleName := ruleName, clusterStateStats := clusterStateStats } =
      { ruleName := ruleName_1, clusterStateStats := clusterStateStats_1 }) =
    (ruleName = ruleName_1 ∧ clusterStateStats = clusterStateStats_1)
-- Init.Data.UInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toUInt32 : Bool → UInt32
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  groupCohomology.coboundaries₁ A = (ModuleCat.Hom.hom (groupCohomology.d₀₁ A)).range
-- Mathlib.CategoryTheory.Whiskering
/-- Auxiliary definition for `whiskeringLeft₃`.  -/
CategoryTheory.Functor.whiskeringLeft₃Obj : {C₁ : Type u_1} →
  (C₂ : Type u_2) →
    (C₃ : Type u_3) →
      {D₁ : Type u_4} →
        (D₂ : Type u_5) →
          (D₃ : Type u_6) →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        (E : Type u_7) →
                          [inst_6 : CategoryTheory.Category.{v_7, u_7} E] →
                            CategoryTheory.Functor C₁ D₁ →
                              CategoryTheory.Functor (CategoryTheory.Functor C₂ D₂)
                                (CategoryTheory.Functor (CategoryTheory.Functor C₃ D₃)
                                  (CategoryTheory.Functor
                                    (CategoryTheory.Functor D₁
                                      (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)))
                                    (CategoryTheory.Functor C₁
                                      (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))))
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.diseq_unsat : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α),
  Lean.Grind.Linarith.Poly.denote ctx Lean.Grind.Linarith.Poly.nil ≠ 0 → False
-- Mathlib.Order.Atoms.Finite
Fintype.IsSimpleOrder.card : ∀ {α : Type u_1} [inst : LE α] [inst_1 : BoundedOrder α] [inst_2 : IsSimpleOrder α] [inst_3 : DecidableEq α],
  Fintype.card α = 2
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.drewritePre : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.PrincipalIdealDomain
isCoprime_of_irreducible_dvd : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {x y : R},
  ¬(x = 0 ∧ y = 0) → (∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y) → IsCoprime x y
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.spectrum.termσ_1 : Lean.ParserDescr
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.allM_filterM : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : MonadLiftT m n] [inst_3 : Monad m] [LawfulMonad m] [inst_5 : Monad n] [inst_6 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [LawfulMonadLiftT m n] {it : Std.IterM m β}
  {f p : β → n (ULift.{w, 0} Bool)},
  Std.IterM.allM p (Std.IterM.filterM f it) =
    Std.IterM.allM
      (fun x => do
        let __do_lift ← f x
        if __do_lift.down = true then p x else pure { down := true })
      (Std.IterM.mapM pure it)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.constLinearEquivOfIsEmpty_symm_apply : ∀ (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ι → Type v₁) (M₂ : Type v₂) [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂]
  [inst_8 : IsEmpty ι] (f : MultilinearMap R M₁ M₂), (MultilinearMap.constLinearEquivOfIsEmpty R S M₁ M₂).symm f = f 0
-- Mathlib.RingTheory.ReesAlgebra
monomial_mem_adjoin_monomial : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R} {n : ℕ} {r : R},
  r ∈ I ^ n → (Polynomial.monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.toLax_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) (a : B), F.toLax.mapId a = (F.mapId a).inv
-- Init.Data.BEq
BEq.neq_of_beq_of_neq : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {a b c : α}, (a == b) = true → (b == c) = false → (a == c) = false
-- Mathlib.FieldTheory.KummerExtension
autAdjoinRootXPowSubCEquiv.congr_simp : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) [inst_1 : NeZero n],
  autAdjoinRootXPowSubCEquiv hζ H = autAdjoinRootXPowSubCEquiv hζ H
-- Init.Data.SInt.Basic
/-- Convert an `ISize` to `BitVec 32`, assuming that the system bit-width is 32.

This operation is intended for proof purposes.
 -/
ISize.toBitVec32 : ISize → System.Platform.numBits = 32 → BitVec 32
-- Lean.Data.Lsp.Window
Lean.Lsp.ShowMessageRequestParams.actions? : Lean.Lsp.ShowMessageRequestParams → Option (Array Lean.Lsp.MessageActionItem)
-- Mathlib.Algebra.Prime.Lemmas
pow_inj_of_not_isUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {q : M},
  ¬IsUnit q → q ≠ 0 → ∀ {m n : ℕ}, q ^ m = q ^ n ↔ m = n
-- Mathlib.Topology.Separation.Profinite
/-- A locally compact Hausdorff totally disconnected space has a basis with clopen elements.  -/
loc_compact_Haus_tot_disc_of_zero_dim : ∀ {H : Type u_3} [inst : TopologicalSpace H] [LocallyCompactSpace H] [T2Space H] [TotallyDisconnectedSpace H],
  TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.realize_exClosure_of_realize_equivSentence : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} [inst_1 : DecidableEq α]
  [inst_2 : (L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {φ : L.Formula α},
  M ⊨ FirstOrder.Language.Formula.equivSentence φ → M ⊨ φ.exClosure
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.precompEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} [inst_3 : W.RespectsIso]
  [inst_4 : W.IsCompatibleWithShift M] [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X X]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y X]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z]
  [inst_10 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z]
  [inst_11 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] (f : X ⟶ Y) (hf : W f) {a : M}
  (α : CategoryTheory.Localization.SmallShiftedHom W Y Z a),
  (CategoryTheory.Localization.SmallShiftedHom.precompEquiv f hf) α =
    (CategoryTheory.Localization.SmallShiftedHom.mk₀ W 0 ⋯ f).comp α ⋯
-- Mathlib.CategoryTheory.Localization.SmallHom
/-- Up to an equivalence, the type `SmallHom.{w} W X Y n` does not depend on the universe `w`.  -/
CategoryTheory.Localization.SmallHom.chgUniv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y : C} →
        [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] →
          [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] →
            CategoryTheory.Localization.SmallHom W X Y ≃ CategoryTheory.Localization.SmallHom W X Y
-- Mathlib.Order.Hom.WithTopBot
InfHom.withTop_id : ∀ {α : Type u_1} [inst : SemilatticeInf α], (InfHom.id α).withTop = InfTopHom.id (WithTop α)
-- Init.Data.Vector.Attach
Vector.getElem_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} (f : (a : α) → p a → β) {xs : Vector α n} (h : ∀ a ∈ xs, p a)
  {i : ℕ} (hn : i < n), (Vector.pmap f xs h)[i] = f xs[i] ⋯
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.comp_bitraverse : ∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t] {F G : Type u → Type u}
  [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : t α α'),
  bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
    Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- The quaternion basis vectors within the algebra.  -/
CliffordAlgebraQuaternion.quaternionBasis : {R : Type u_1} →
  [inst : CommRing R] →
    (c₁ c₂ : R) → QuaternionAlgebra.Basis (CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)) c₁ 0 c₂
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.isCompleteSpace : ∀ (self : CpltSepUniformSpace), CompleteSpace self.α
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mul_subset_mul_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_nonempty : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s : TopologicalSpace.Closeds α}, (↑s).Nonempty ↔ s ≠ ⊥
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_maxKey?_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {kme : α},
      Std.Internal.List.maxKey? (Std.Internal.List.eraseKey k l) = some kme → Std.Internal.List.containsKey kme l = true
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.mk_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y),
  (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).fst = π₁
-- Mathlib.Algebra.Module.FinitePresentation
/-- Let `M` be a finitely presented `R`-module, `N` be an `R`-module, `S` be a submonoid of `R`,
`Mₚ` be the localization of `M` at `S`, `Nₚ` be the localization of `N` at `S`. Then any surjective
linear map `ϕ : Mₚ →ₗ[R] Nₚ` lifts to a linear map `φ : M →ₗ[R] N` that is surjective after
localization at `S`.  -/
Module.exists_localizedMap_surjective_of_surjective : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FinitePresentation R M] (S : Submonoid R) {Mₚ : Type u_1}
  [inst_6 : AddCommGroup Mₚ] [inst_7 : Module R Mₚ] (f : M →ₗ[R] Mₚ) [inst_8 : IsLocalizedModule S f] {Nₚ : Type u_2}
  [inst_9 : AddCommGroup Nₚ] [inst_10 : Module R Nₚ] (g : N →ₗ[R] Nₚ) [inst_11 : IsLocalizedModule S g]
  {ϕ : Mₚ →ₗ[R] Nₚ},
  Function.Surjective ⇑ϕ →
    ∃ φ s, ∃ (_ : (IsLocalizedModule.map S f g) φ = s • ϕ), Function.Surjective ⇑((IsLocalizedModule.map S f g) φ)
-- Init.Data.BitVec.Bitblast
/-- `DivModArgs` contains the arguments to a `divrem` call which remain constant throughout
execution.  -/
BitVec.DivModArgs : ℕ → Type
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C) (j : κ.ord.ToType) {Z : C}
  (h : (((CategoryTheory.SmallObject.iterationFunctor I κ).obj (Order.succ j)).obj f).right ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Arrow.Hom.right
        (CategoryTheory.Arrow.Hom.right (CategoryTheory.SmallObject.iterationFunctorMapSuccAppArrowIso I κ f j).hom))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Arrow.Hom.right
          (((CategoryTheory.SmallObject.iterationFunctor I κ).map (CategoryTheory.homOfLE ⋯)).app f))
        h) =
    h
-- Mathlib.Tactic.Linter.UpstreamableDecl
/-- Does the declaration with this name depend on definitions in the current file?

Here, "definition" means everything that is not a theorem, and so includes `def`,
`structure`, `inductive`, etc.
 -/
_private.Mathlib.Tactic.Linter.UpstreamableDecl.0.Lean.Environment.localDefinitionDependencies : Lean.Environment → Lean.Syntax → Lean.Syntax → Lean.Elab.Command.CommandElabM Bool
-- Mathlib.RingTheory.AdjoinRoot
/-- `algHomOfDvd` sends `AdjoinRoot.root f` to `AdjoinRoot.root q`.  -/
AdjoinRoot.algHomOfDvd_root : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hgf : g ∣ f), (AdjoinRoot.algHomOfDvd R f g hgf) (AdjoinRoot.root f) = AdjoinRoot.root g
-- Init.Data.SInt.Lemmas
Int64.toInt8_ofBitVec : ∀ (b : BitVec 64), (Int64.ofBitVec b).toInt8 = Int8.ofBitVec (BitVec.signExtend 8 b)
-- Mathlib.Algebra.Order.Sub.Defs
tsub_le_tsub : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c d : α}
  [AddLeftMono α], a ≤ b → c ≤ d → a - d ≤ b - c
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] [IsDomain R]
  {M : Matrix n n R}, ((Matrix.toLinearMap₂' R) M).SeparatingLeft ↔ M.det ≠ 0
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instDecidableEqUnitVal : {α : ℚ} → DecidableEq (Std.Time.Internal.UnitVal α)
-- Std.Http.Protocol.H1.Parser
Std.Http.Protocol.H1.TakeResult.incomplete.inj : ∀ {data : ByteSlice} {remaining : ℕ} {data_1 : ByteSlice} {remaining_1 : ℕ},
  Std.Http.Protocol.H1.TakeResult.incomplete data remaining =
      Std.Http.Protocol.H1.TakeResult.incomplete data_1 remaining_1 →
    data = data_1 ∧ remaining = remaining_1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.ofList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {hd : α} {tl : List α},
  Std.TreeSet.ofList (hd :: tl) cmp = (∅.insert hd).insertMany tl
-- Mathlib.Topology.Spectral.Prespectral
/-- In a prespectral space, the lattice of opens is determined by its lattice of compact opens.  -/
PrespectralSpace.opensEquiv : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [PrespectralSpace X] → TopologicalSpace.Opens X ≃o Order.Ideal (TopologicalSpace.CompactOpens X)
-- Mathlib.Order.Filter.NAry
Filter.map_map₂_distrib : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} {m : α → β → γ}
  {f : Filter α} {g : Filter β} {n : γ → δ} {m' : α' → β' → δ} {n₁ : α → α'} {n₂ : β → β'},
  (∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)) →
    Filter.map n (Filter.map₂ m f g) = Filter.map₂ m' (Filter.map n₁ f) (Filter.map n₂ g)
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Expressing `HasFDerivAtFilter f f' x L` in terms of `HasDerivAtFilter`  -/
hasFDerivAtFilter_iff_hasDerivAtFilter : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {L : Filter (𝕜 × 𝕜)} [inst_4 : ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F},
  HasFDerivAtFilter f f' L ↔ HasDerivAtFilter f (f' 1) L
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- `hsymmPart` is the product of the symmetric polynomials `hsymm μᵢ`,
where `μ = (μ₁, μ₂, ...)` is a partition.  -/
MvPolynomial.hsymmPart : (σ : Type u_5) →
  (R : Type u_6) → [inst : CommSemiring R] → [Fintype σ] → [DecidableEq σ] → {n : ℕ} → n.Partition → MvPolynomial σ R
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.FinitePlace.norm_embedding_int`.

---

The norm of the image after the embedding associated to `v` is equal to the norm of `v` raised
to the power of the `v`-adic valuation for integers.  -/
NumberField.FinitePlace.norm_def_int : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : R),
  ‖(NumberField.FinitePlace.embedding v) ((algebraMap R K) x)‖ = ↑((WithZeroMulInt.toNNReal ⋯) (v.intValuation x))
-- Mathlib.Topology.Separation.Hausdorff
/-- If `V : ι → Set X` is a decreasing family of compact sets then any neighborhood of
`⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhds_of_isCompact'` where we
don't need to assume each `V i` closed because it follows from compactness since `X` is
assumed to be Hausdorff.  -/
exists_subset_nhds_of_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {ι : Type u_4} [Nonempty ι] {V : ι → Set X},
  Directed (fun x1 x2 => x1 ⊇ x2) V →
    (∀ (i : ι), IsCompact (V i)) → ∀ {U : Set X}, (∀ x ∈ ⋂ i, V i, U ∈ nhds x) → ∃ i, V i ⊆ U
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioo_cast : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioo (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.Ioo a b, f (Fin.cast h i)
-- Lean.Parser.Term
Lean.Parser.Term.dbgTrace.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain_v_fst_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m)
  (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + 1 = p₃),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂)
      ((↑(CochainComplex.mappingCone.fst φ)).v p₂ p₃ h₂₃) =
    α.v p₁ p₃ ⋯
-- Mathlib.Algebra.Notation.Support
Subsingleton.support_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] [Subsingleton M] (f : ι → M), Function.support f = ∅
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.mk.inj : ∀ {stx : Lean.Syntax} {ci : Lean.Elab.ContextInfo} {mctxBefore mctxAfter : Lean.MetavarContext}
  {goalsTargetedBy goalsCreatedBy : List Lean.MVarId} {stx_1 : Lean.Syntax} {ci_1 : Lean.Elab.ContextInfo}
  {mctxBefore_1 mctxAfter_1 : Lean.MetavarContext} {goalsTargetedBy_1 goalsCreatedBy_1 : List Lean.MVarId},
  { stx := stx, ci := ci, mctxBefore := mctxBefore, mctxAfter := mctxAfter, goalsTargetedBy := goalsTargetedBy,
        goalsCreatedBy := goalsCreatedBy } =
      { stx := stx_1, ci := ci_1, mctxBefore := mctxBefore_1, mctxAfter := mctxAfter_1,
        goalsTargetedBy := goalsTargetedBy_1, goalsCreatedBy := goalsCreatedBy_1 } →
    stx = stx_1 ∧
      ci = ci_1 ∧
        mctxBefore = mctxBefore_1 ∧
          mctxAfter = mctxAfter_1 ∧ goalsTargetedBy = goalsTargetedBy_1 ∧ goalsCreatedBy = goalsCreatedBy_1
-- Init.Data.Array.Basic
/-- Drop `none`s from a Array, and replace each remaining `some a` with `a`.  -/
Array.reduceOption : {α : Type u} → Array (Option α) → Array α
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isThetaTVS_iff_isTheta : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =Θ[𝕜; l] g ↔ f =Θ[l] g
-- Mathlib.CategoryTheory.Action.Concrete
Action.ρ_inv_self_apply : ∀ {G : Type u} [inst : Group G] {A : Action (Type u) G} (g : G) (x : A.V),
  (CategoryTheory.ConcreteCategory.hom (A.ρ g⁻¹)) ((CategoryTheory.ConcreteCategory.hom (A.ρ g)) x) = x
-- Std.Data.HashMap.Lemmas
Std.HashMap.get!_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₁ → (m₁ ∪ m₂).get! k = m₂.get! k
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_whiskerRight_assoc : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.id X) Y) h =
    h
-- Mathlib.Order.Max
IsMin.not_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMin a → ¬b < a
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instFromJsonDidSaveTextDocumentParams : Lean.FromJson Lean.Lsp.DidSaveTextDocumentParams
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `L` with the spectral norm is a `SeminormedAddCommGroup`.  -/
spectralNorm.seminormedAddCommGroup : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Algebra.IsAlgebraic K L] → [hu : IsUltrametricDist K] → [CompleteSpace K] → SeminormedAddCommGroup L