mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddCommGroup.ofAddDist'.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : AddCommGroup E] [inst_2 : PseudoMetricSpace E]
  (h₁ : ∀ (x : E), ‖x‖ = dist 0 x) (h₂ : ∀ (x y z : E), dist (z + x) (z + y) ≤ dist x y),
  SeminormedAddCommGroup.ofAddDist' h₁ h₂ =
    { toNorm := (SeminormedAddGroup.ofAddDist' h₁ h₂).toNorm,
      toAddGroup := (SeminormedAddGroup.ofAddDist' h₁ h₂).toAddGroup, add_comm := ⋯,
      toPseudoMetricSpace := (SeminormedAddGroup.ofAddDist' h₁ h₂).toPseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_true`. -/
Set.setOf_true : ∀ {α : Type u}, {_x | True} = Set.univ
-- Batteries.Data.PairingHeap
Batteries.PairingHeap.instInhabited : {α : Type u} → {le : α → α → Bool} → Inhabited (Batteries.PairingHeap α le)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inr : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} → (self : CategoryTheory.Limits.BinaryBicone P Q) → Q ⟶ self.pt
-- Mathlib.Order.Filter.Extr
IsMinOn.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β} {s : Set α} {a : α},
  IsMinOn f s a → ∀ {g : β → γ}, Antitone g → IsMaxOn (g ∘ f) s a
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- **Alias** of `SimpleGraph.IsAcyclic.sup_edge_of_not_reachable`.

---

Connecting two unreachable vertices by an edge preserves acyclicity.  -/
SimpleGraph.IsAcyclic.isAcyclic_sup_fromEdgeSet_of_not_reachable : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, ¬G.Reachable u v → G.IsAcyclic → (G ⊔ SimpleGraph.edge u v).IsAcyclic
-- Lean.Meta.CongrTheorems
Lean.Meta.CongrTheorem.type : Lean.Meta.CongrTheorem → Lean.Expr
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the number of mappings present in the map.  -/
Std.ExtDTreeMap.size : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.ExtDTreeMap α β cmp → ℕ
-- Mathlib.Algebra.Order.UpperLower
UpperSet.coe_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s t : UpperSet α),
  ↑(s - t) = ↑s - ↑t
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.instHasTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.HasTerminal (CategoryTheory.WithTerminal C)
-- Mathlib.Order.Std
/-- Arguments for `PartialOrder.ofStd`; see that function for details.  -/
PartialOrder.OfStdArgs : Type u_1 → Type u_1
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_reindex_iff : ∀ {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix n n α} (f : n ≃ m),
  ((Matrix.reindex f f) A).IsSymm ↔ A.IsSymm
-- Init.NotationExtra
Lean.unifConstraint : Lean.ParserDescr
-- Lean.Parser.Term
Lean.Parser.Term.funImplicitBinder : Lean.Parser.Parser
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the monadic predicate `p` returns `ULift.up true` for
all elements emitted by the iterator `it`.

`O(|it|)`. Short-circuits upon encountering the first mismatch. The outputs of `it` are
examined in order of iteration.
 -/
Std.IterM.allM : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → (β → m (ULift.{w, 0} Bool)) → Std.IterM m β → m (ULift.{w, 0} Bool)
-- Mathlib.Topology.Homotopy.Lifting
IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_surjective : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] (hp : IsAddQuotientCoveringMap p G) {x : X} (e : ↑(p ⁻¹' {x}))
  [PathConnectedSpace E], Function.Surjective ⇑(hp.fundamentalGroupToMulOpposite e)
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.instIsStableUnderRetractsTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.IsStableUnderRetracts
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Obvious triangles `0 ⟶ X ⟶ X ⟶ 0⟦1⟧` are distinguished  -/
CategoryTheory.Pretriangulated.contractible_distinguished₁ : ∀ {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] (X : C),
  CategoryTheory.Pretriangulated.Triangle.mk 0 (CategoryTheory.CategoryStruct.id X) 0 ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
-- Lean.Meta.Tactic.LibrarySearch
/-- Create lemma from name and mod.  -/
Lean.Meta.LibrarySearch.mkLibrarySearchLemma : Lean.Name → Lean.Meta.LibrarySearch.DeclMod → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
/-- If `C` is a finitely cocomplete category and `A : Cᵒᵖ ⥤ Type u` is a presheaf that preserves
finite limits, then `CostructuredArrow yoneda A` is filtered.

One direction of Proposition 3.3.13 of [Kashiwara2006].
 -/
CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C]
  (A : CategoryTheory.Functor Cᵒᵖ (Type v)) [CategoryTheory.Limits.PreservesFiniteLimits A],
  CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
-- Init.Data.List.Nat.Pairwise
/-- Given a sublist `l' <+ l`, there exists an increasing list of indices `is` such that
`l' = is.map fun i => l[i]`.  -/
List.sublist_eq_map_getElem : ∀ {α : Type u_1} {l l' : List α},
  l'.Sublist l → ∃ is, l' = List.map (fun x => l[x]) is ∧ List.Pairwise (fun x1 x2 => x1 < x2) is
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.mul_def : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (a b : N ⋊[φ] G),
  a * b = ⟨a.left * (φ a.right) b.left, a.right * b.right⟩
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.write.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (x : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ),
  Turing.TM1to1.write [] x = x
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_map_map : ∀ {E : Type v} [inst : Field E] (A B : Subfield E) {L : Type v} [inst_1 : Field L] (f : E →+* L),
  (Subfield.map f A).relrank (Subfield.map f B) = A.relrank B
-- Init.Data.Order.Classes
/-- This typeclass bundles `MaxEqOr α` and `LawfulOrderSup α`. It characterizes when a `Max α`
instance reasonably computes maxima in some type `α` that has an `LE α` instance.

As long as `α` is a preorder (see `IsPreorder α`), this typeclass implies that the order on
`α` is total and that `Min.min a b` returns either `a` or `b`, whichever is greater or equal to
the other.
 -/
Std.LawfulOrderMax : (α : Type u) → [Max α] → [LE α] → Prop
-- Aesop.Search.Expansion.Simp
Aesop.SimpResult : Type
-- Mathlib.Order.Filter.Pointwise
Filter.map_inv' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (m : F) {f : Filter α}, Filter.map (⇑m) f⁻¹ = (Filter.map (⇑m) f)⁻¹
-- Std.Http.Data.Body.Empty
/-- Selector that immediately resolves with end-of-stream for an empty body.
 -/
Std.Http.Body.Empty.recvSelector : Std.Http.Body.Empty → Std.Async.Selector (Option Std.Http.Chunk)
-- Mathlib.Topology.Algebra.Algebra
instContinuousMulElemIocOfNat : ∀ (A : Type u) [inst : Semiring A] [inst_1 : TopologicalSpace A] [inst_2 : PartialOrder A]
  [inst_3 : IsStrictOrderedRing A] [ContinuousMul A], ContinuousMul ↑(Set.Ioc 0 1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β},
  m.WF → (k ∈ Std.DHashMap.Raw.Const.alter m k f ↔ (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true)
-- Init.Data.Dyadic.Basic
Dyadic.toRat_sub : ∀ (x y : Dyadic), (x - y).toRat = x.toRat - y.toRat
-- Mathlib.MeasureTheory.Function.LpSpace.CompleteOfCompleteLp
MeasureTheory.nontrivial_Lp_real_of_nontrivial_Lp : ∀ {α : Type u_1} (E : Type u_2) [inst : NormedAddCommGroup E] {mα : MeasurableSpace α} (p : ENNReal)
  (μ : MeasureTheory.Measure α) [Nontrivial ↥(MeasureTheory.Lp E p μ)], Nontrivial ↥(MeasureTheory.Lp ℝ p μ)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_ΨSq : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), (W.ΨSq n).coeff (n.natAbs ^ 2 - 1) = ↑n ^ 2
-- Mathlib.Topology.Compactness.CountablyCompact
/-- In a first-countable space, a countably compact set is sequentially compact.  -/
IsCountablyCompact.isSeqCompact : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E} [FirstCountableTopology E],
  IsCountablyCompact A → IsSeqCompact A
-- Mathlib.Data.List.Permutation
List.permutationsAux2.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (x : List α → β) (y : α) (ys : List α),
  List.permutationsAux2 t ts r (y :: ys) x =
    match List.permutationsAux2 t ts r ys fun x_1 => x (y :: x_1) with
    | (us, zs) => (y :: us, x (t :: y :: us) :: zs)
-- Mathlib.Algebra.Group.Even
Even.two_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] (r : α), Even (2 • r)
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.widePullbackShapeEquivObj_apply : ∀ {J : Type u_1} (x : CategoryTheory.Limits.WidePullbackShape J),
  CategoryTheory.WithTerminal.widePullbackShapeEquivObj✝ x =
    match x with
    | some x => CategoryTheory.WithTerminal.of { as := x }
    | none => CategoryTheory.WithTerminal.star
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `F : D ⥤ K ⥤ C` preserves the limit of some `G : J ⥤ D` if it does for each `k : K`.  -/
CategoryTheory.Limits.preservesLimit_of_evaluation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor D (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor J D),
  (∀ (k : K), CategoryTheory.Limits.PreservesLimit G (F.comp ((CategoryTheory.evaluation K C).obj k))) →
    CategoryTheory.Limits.PreservesLimit G F
-- Mathlib.Algebra.Field.Subfield.Basic
RingHom.mem_fieldRange_self : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (f : K →+* L) (x : K), f x ∈ f.fieldRange
-- Mathlib.Algebra.Order.Antidiag.Prod
/-- A point in the antidiagonal is determined by its first co-ordinate (subtype version of
`Finset.antidiagonal_congr`). This lemma is used by the `ext` tactic.  -/
Finset.HasAntidiagonal.antidiagonal_subtype_ext : ∀ {A : Type u_1} [inst : AddCancelMonoid A] [inst_1 : Finset.HasAntidiagonal A] {n : A}
  {p q : ↥(Finset.HasAntidiagonal.antidiagonal n)}, (↑p).1 = (↑q).1 → p = q
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_neg : ∀ {α : Type u_1} [inst : Neg α] (a : αᵒᵈ), OrderDual.ofDual (-a) = -OrderDual.ofDual a
-- Mathlib.LinearAlgebra.Matrix.RowCol
/-- Update, i.e. replace the `i`th row of matrix `A` with the values in `b`.  -/
Matrix.updateRow : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [DecidableEq m] → Matrix m n α → m → (n → α) → Matrix m n α
-- Init.Data.Option.Lemmas
Option.mem_ite_none_left : ∀ {α : Type u_1} {p : Prop} {x : α} {x_1 : Decidable p} {l : Option α}, (x ∈ if p then none else l) ↔ ¬p ∧ x ∈ l
-- Init.Data.SInt.Basic
instShiftLeftInt64 : ShiftLeft Int64
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_singleton_left : ∀ {G : Type u_1} [inst : Group G] {S : Set G} {g : G}, Subgroup.IsComplement {g} S ↔ S = Set.univ
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.unop_le_one : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] {a : αᵐᵒᵖ}, MulOpposite.unop a ≤ 1 ↔ a ≤ 1
-- Lean.Parser.Do
Lean.Parser.Term.doContinue.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.Divisors
Nat.primeFactors_filter_dvd_of_dvd : ∀ {m n : ℕ}, n ≠ 0 → m ∣ n → {p ∈ n.primeFactors | p ∣ m} = m.primeFactors
-- Mathlib.Order.Filter.Map
Filter.disjoint_of_map : ∀ {α : Type u_6} {β : Type u_7} {F G : Filter α} {f : α → β}, Disjoint (Filter.map f F) (Filter.map f G) → Disjoint F G
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.unopMap_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ),
  CategoryTheory.ShortComplex.unopMap (CategoryTheory.CategoryStruct.id S) = CategoryTheory.CategoryStruct.id S.unop
-- Mathlib.CategoryTheory.Monoidal.Skeleton
/-- A monoidal functor between monoidal categories induces a monoid homomorphism between
the skeleta.  -/
CategoryTheory.Skeleton.monoidHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) → [F.Monoidal] → CategoryTheory.Skeleton C →* CategoryTheory.Skeleton D
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.hom_inv_id_app_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E']
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D (CategoryTheory.Functor E E'))} (e : F ≅ G) (X₁ : C)
  (X₂ : D) (X₃ : E),
  CategoryTheory.CategoryStruct.comp (((e.hom.app X₁).app X₂).app X₃) (((e.inv.app X₁).app X₂).app X₃) =
    CategoryTheory.CategoryStruct.id (((F.obj X₁).obj X₂).obj X₃)
-- Lean.Meta.Closure
Lean.Meta.Closure.MkValueTypeClosureResult.mk.injEq : ∀ (levelParams : Array Lean.Name) (type value : Lean.Expr) (levelArgs : Array Lean.Level) (exprArgs : Array Lean.Expr)
  (levelParams_1 : Array Lean.Name) (type_1 value_1 : Lean.Expr) (levelArgs_1 : Array Lean.Level)
  (exprArgs_1 : Array Lean.Expr),
  ({ levelParams := levelParams, type := type, value := value, levelArgs := levelArgs, exprArgs := exprArgs } =
      { levelParams := levelParams_1, type := type_1, value := value_1, levelArgs := levelArgs_1,
        exprArgs := exprArgs_1 }) =
    (levelParams = levelParams_1 ∧ type = type_1 ∧ value = value_1 ∧ levelArgs = levelArgs_1 ∧ exprArgs = exprArgs_1)
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.toKaroubiEquivalence.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.IsIdempotentComplete C],
  CategoryTheory.Idempotents.toKaroubiEquivalence C = CategoryTheory.Idempotents.toKaroubiEquivalence C
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.postcomp_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n : ℤ} (z : CochainComplex.HomComplex.Cocycle F G n) (f : G ⟶ K),
  ↑(z.postcomp f) = (↑z).comp (CochainComplex.HomComplex.Cochain.ofHom f) ⋯
-- Mathlib.CategoryTheory.Comma.Arrow
/-- `isoMk''` is the dual of `isoMk`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.Arrow.isoMk'' : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    {f g : CategoryTheory.Arrow T} →
      (l : f.right ≅ g.right) →
        (r : f.left ≅ g.left) →
          autoParam (CategoryTheory.CategoryStruct.comp g.hom l.inv = CategoryTheory.CategoryStruct.comp r.inv f.hom)
              CategoryTheory.Arrow.isoMk''._auto_1 →
            (f ≅ g)
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.brecOn_1.eq : ∀ {motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u}
  {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  (t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot))
  (F_1 : (t : Lean.Language.Lean.CommandParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
      Lean.Language.Lean.CommandParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Task Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_3 t → motive_4 t),
  Lean.Language.Lean.CommandParsedSnapshot.brecOn_1 t F_1 F_2 F_3 F_4 =
    F_2 t (Lean.Language.Lean.CommandParsedSnapshot.brecOn_1.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Topology.Defs.Filter
/-- The "neighborhood within" filter. Elements of `𝓝[s] x` are sets containing the
intersection of `s` and a neighborhood of `x`.  -/
nhdsWithin : {X : Type u_1} → [TopologicalSpace X] → X → Set X → Filter X
-- Mathlib.Algebra.Central.Basic
/-- Opposite algebra of a central algebra is central. This instance combined with the coming
`IsSimpleRing` instance for the opposite of central simple algebra will be an
inverse for an element in `BrauerGroup`, find out more about this in
`Mathlib/Algebra/BrauerGroup/Defs.lean`.  -/
Algebra.IsCentral.instMulOpposite : ∀ (K : Type u) [inst : CommSemiring K] (D : Type v) [inst_1 : Semiring D] [inst_2 : Algebra K D]
  [h : Algebra.IsCentral K D], Algebra.IsCentral K Dᵐᵒᵖ
-- Mathlib.Geometry.Manifold.Immersion
/-- A function `f : M → N` between `C^n` manifolds is `C^n` if and only if it is continuous
and its composition `φ ∘ f` with a `C^n` immersion `φ : N → N'` is `C^n`.  -/
ContMDiff.iff_comp_isImmersionOfComplement : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E''' : Type u_4} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup E'''] [inst_6 : NormedSpace 𝕜 E''']
  [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] {H : Type u_7} [inst_9 : TopologicalSpace H] {G : Type u_9}
  [inst_10 : TopologicalSpace G] {G' : Type u_10} [inst_11 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H M] {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {N' : Type u_14} [inst_16 : TopologicalSpace N'] [inst_17 : ChartedSpace G' N'] {n : WithTop ℕ∞} {f : M → N}
  {φ : N → N'},
  Manifold.IsImmersionOfComplement F J J' n φ → (ContMDiff I J n f ↔ Continuous f ∧ ContMDiff I J' n (φ ∘ f))
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.homEquiv_apply_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X),
  ((CategoryTheory.ihom.adjunction A).homEquiv Y X) f = CategoryTheory.MonoidalClosed.curry f
-- Mathlib.Data.List.Basic
List.idxOf_get : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α} (h : List.idxOf a l < l.length),
  l.get ⟨List.idxOf a l, h⟩ = a
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.RuleState.update.addCompleteMatches.loop : Aesop.RuleState →
  Array Aesop.ClusterState →
    ℕ → Array Aesop.Match → Aesop.CompleteMatch → ℕ → StateM (Array Aesop.ForwardRuleMatch) Unit
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.zero.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [inst_1 : SizeOf J],
  sizeOf CommRingCat.Colimits.Prequotient.zero = 1
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X : C} (t : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal t).hom = 0
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.even.lift.aux_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A)
  (x : ↥(CliffordAlgebra.even Q)),
  (CliffordAlgebra.even.lift.aux f) x = (((CliffordAlgebra.foldr Q (CliffordAlgebra.even.lift.fFold✝ f) ⋯) (1, 0)) ↑x).1
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- The singleton prepartition `{J}`, `J ≤ I`.  -/
BoxIntegral.Prepartition.single : {ι : Type u_1} → (I J : BoxIntegral.Box ι) → J ≤ I → BoxIntegral.Prepartition I
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- Given a ring homomorphism `f : R →+* S`, an open set `U` of the prime spectrum of `R` and an open
set `V` of the prime spectrum of `S`, such that `V ⊆ (comap f) ⁻¹' U`, we can push a section `s`
on `U` to a section on `V`, by composing with `Localization.localRingHom _ _ f` from the left and
`comap f` from the right. Explicitly, if `s` evaluates on `comap f p` to `a / b`, its image on `V`
evaluates on `p` to `f(a) / f(b)`.

At the moment, we work with arbitrary dependent functions `s : Π x : U, Localizations R x`. Below,
we prove the predicate `isLocallyFraction` is preserved by this map, hence it can be extended to
a morphism between the structure sheaves of `R` and `S`.
 -/
AlgebraicGeometry.StructureSheaf.comapFun : {R M : Type u} →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        {S : Type u} →
          [inst_3 : CommRing S] →
            {N : Type u} →
              [inst_4 : AddCommGroup N] →
                [inst_5 : Module S N] →
                  {σ : R →+* S} →
                    (M →ₛₗ[σ] N) →
                      (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
                        (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) →
                          V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier →
                            ((x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x) →
                              (y : ↥V) → AlgebraicGeometry.StructureSheaf.Localizations N ↑y
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.instInhabitedPremise : Inhabited Mathlib.Tactic.ClickSuggestions.Premise
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.lengthTRAux.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (head : α) (as : List α) (n : ℕ) (h_1 : (n : ℕ) → motive [] n)
  (h_2 : (head : α) → (as : List α) → (n : ℕ) → motive (head :: as) n),
  (match head :: as, n with
    | [], n => h_1 n
    | head :: as, n => h_2 head as n) =
    h_2 head as n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  t.WF → ∀ {k a : α} {v : β}, (t.insertIfNew k v)[a]! = if cmp k a = Ordering.eq ∧ k ∉ t then v else t[a]!
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldrM.loop.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (n : ℕ) (f : Fin n → α → m α) (a : α) (i : ℕ)
  (h : i + 1 ≤ n), Fin.foldrM.loop✝ n f ⟨i.succ, h⟩ a = f ⟨i, h⟩ a >>= Fin.foldrM.loop✝ n f ⟨i, ⋯⟩