mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instQuasiIsoOppositeMapSymmOpFunctorOp : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L)
  [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i] [QuasiIso φ],
  QuasiIso ((HomologicalComplex.opFunctor V c).map φ.op)
-- Lean.Linter.Init
Lean.Linter.linterSetsExt : Lean.PersistentEnvExtension (Lean.Name × Lean.NameSet) (Lean.Name × Lean.NameSet) Lean.Linter.LinterSetsState
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.radical_eq_maximalIdeal : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [inst_2 : IsLocalRing R] (I : Ideal R),
  I ≠ ⊤ → I.radical = IsLocalRing.maximalIdeal R
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_iff_closedBall_smul : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {s : Set E},
  Balanced 𝕜 s ↔ Metric.closedBall 0 1 • s ⊆ s
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Vertices of the subgraph  -/
SimpleGraph.Subgraph.verts : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → Set V
-- Mathlib.Topology.Order.IsLUB
IsClosed.lowerClosure : ∀ {α : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, IsClosed s → IsClosed (lowerClosure s).carrier
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
toAdd_list_sum : ∀ {M : Type u_3} [inst : AddMonoid M] (s : List (Multiplicative M)),
  Multiplicative.toAdd s.prod = (List.map (⇑Multiplicative.toAdd) s).sum
-- Std.Data.DHashMap.Internal.Model
/-- This is the general theorem to show that modification operations preserve well-formedness of
buckets.  -/
Std.DHashMap.Internal.IsHashSelf.updateBucket : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Array (Std.DHashMap.Internal.AssocList α β)} {h : 0 < m.size} {a : α}
  {f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β},
  (∀ (l : Std.DHashMap.Internal.AssocList α β),
      ∀ p ∈ (f l).toList, Std.Internal.List.containsKey p.fst l.toList = true ∨ hash p.fst = hash a) →
    Std.DHashMap.Internal.IsHashSelf m → Std.DHashMap.Internal.IsHashSelf (Std.DHashMap.Internal.updateBucket m h a f)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instPartialOrderFiniteIndexNormalSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G], FiniteIndexNormalSubgroup.instPartialOrderFiniteIndexNormalSubgroup = inferInstance
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.measurableSMul₂_iterateMulAct : ∀ {α : Type u_2} {x : MeasurableSpace α} {f : α → α}, Measurable f → MeasurableSMul₂ (IterateMulAct f) α
-- Mathlib.Algebra.GCDMonoid.Nat
Int.exists_unit_of_abs : ∀ (a : ℤ), ∃ u, ∃ (_ : IsUnit u), ↑a.natAbs = u * a
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (D : F.DescentData' sq sq₃) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ i₃ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (f₃ : Y ⟶ X i₃)
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
      CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
      CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'._auto_3)
  (hf₃ :
    autoParam (CategoryTheory.CategoryStruct.comp f₃ (f i₃) = q)
      CategoryTheory.Pseudofunctor.DescentData'.comp_pullHom'._auto_5),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom q f₁ f₂ hf₁ hf₂)
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom q f₂ f₃ hf₂ hf₃) =
    CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom q f₁ f₃ hf₁ hf₃
-- Mathlib.CategoryTheory.Enriched.Opposite
/-- The equivalence between the underlying category of the enriched category `Cᵒᵖ` and
the opposite of the underlying category of the enriched category `C`.  -/
CategoryTheory.forgetEnrichmentOppositeEquivalence : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      [inst_2 : CategoryTheory.BraidedCategory V] →
        (C : Type u) →
          [inst_3 : CategoryTheory.EnrichedCategory V C] →
            CategoryTheory.ForgetEnrichment V Cᵒᵖ ≌ (CategoryTheory.ForgetEnrichment V C)ᵒᵖ
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_dirac : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {f : X → E} {B : E →L[ℝ] F →L[ℝ] G} [inst_6 : MeasurableSpace X] [MeasurableSingletonClass X] [CompleteSpace G]
  {a : X} {v : F}, ∫ᵛ (x : X), f x ∂[B; MeasureTheory.VectorMeasure.dirac a v] = (B (f a)) v
-- Aesop.Tree.Data
Aesop.Iteration.instToString : ToString Aesop.Iteration
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.step_filterWithPostcondition : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} {n : Type w → Type w''}
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} [inst_1 : Monad n] [LawfulMonad n] [MonadLiftT m n],
  (Std.Iter.filterWithPostcondition f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => do
      let __do_lift ← (f out).operation
      match __do_lift with
        | ⟨{ down := false }, h'⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.filterWithPostcondition f it') ⋯))
        | ⟨{ down := true }, h'⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.Iter.filterWithPostcondition f it') out ⋯))
    | ⟨Std.IterStep.skip it', h⟩ =>
      pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.filterWithPostcondition f it') ⋯))
    | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_prod_of_pairwise_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (l : List (Equiv.Perm α)),
  List.Pairwise Equiv.Perm.Disjoint l →
    l.prod.support = List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map Equiv.Perm.support l)
-- Mathlib.Order.Partition.Finpartition
Finpartition.instUniqueBot : {α : Type u_1} → [inst : Lattice α] → [inst_1 : OrderBot α] → Unique (Finpartition ⊥)
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap_bind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Option α) (f : α → Option β) (g : (a : β) → x.bind f = some a → γ),
  Std.Internal.List.Option.dmap✝ (x.bind f) g =
    x.pbind fun a h => Std.Internal.List.Option.dmap✝ (f a) fun b h' => g b ⋯
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.compUliftCoyonedaIso_inv_app_app_hom_apply_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (X : Cᵒᵖ) (X_1 : D)
  (x : ULift.{max v₂ w, v₁} (Opposite.unop X ⟶ G.obj X_1)),
  ((CategoryTheory.ConcreteCategory.hom ((adj.compUliftCoyonedaIso.inv.app X).app X_1)) x).down =
    CategoryTheory.CategoryStruct.comp (F.map x.down) (adj.counit.app X_1)
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The proposition that the values of the function `f : B → G` satisfy the Coxeter relations
corresponding to the matrix `M`.  -/
CoxeterMatrix.IsLiftable : {B : Type u_1} → {G : Type u_5} → [Monoid G] → CoxeterMatrix B → (B → G) → Prop
-- Mathlib.Data.List.Cycle
Cycle.map_nil : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Cycle.map f Cycle.nil = Cycle.nil
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- The associated bilinear form of an anisotropic quadratic form is nondegenerate.  -/
QuadraticMap.separatingLeft_of_anisotropic : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Invertible 2] (Q : QuadraticMap R M R),
  Q.Anisotropic → LinearMap.SeparatingLeft (QuadraticMap.associated' Q)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageFactorisation.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y}
  {F : CategoryTheory.Limits.MonoFactorisation f} {isImage : CategoryTheory.Limits.IsImage F}
  {F_1 : CategoryTheory.Limits.MonoFactorisation f} {isImage_1 : CategoryTheory.Limits.IsImage F_1},
  { F := F, isImage := isImage } = { F := F_1, isImage := isImage_1 } → F = F_1 ∧ isImage ≍ isImage_1
-- Mathlib.LinearAlgebra.Pi
/-- Homs to a pi module are canonically identified with a product of hom types, even linearly so.  -/
LinearEquiv.linearMapPi : {R : Type u} →
  {M₂ : Type w} →
    {ι : Type x} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : Module R M₂] →
            {φ : ι → Type i} →
              [inst_3 : (i : ι) → AddCommMonoid (φ i)] →
                [inst_4 : (i : ι) → Module R (φ i)] →
                  (S : Type u_1) →
                    [inst_5 : Semiring S] →
                      [inst_6 : (i : ι) → Module S (φ i)] →
                        [inst_7 : ∀ (i : ι), SMulCommClass R S (φ i)] →
                          ((i : ι) → M₂ →ₗ[R] φ i) ≃ₗ[S] M₂ →ₗ[R] (i : ι) → φ i
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Inhabited α]
  [inst_1 : Std.TransCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∩ t₂).getKey! k = default
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribSMul.toAddMonoidHom_apply : ∀ {M : Type u_1} (A : Type u_7) [inst : AddZeroClass A] [inst_1 : DistribSMul M A] (x : M) (x_1 : A),
  (DistribSMul.toAddMonoidHom A x) x_1 = x • x_1
-- Aesop.RuleTac.Forward
Aesop.RuleTac.makeForwardHypProofs : Lean.Expr → Option Aesop.Substitution → Aesop.UnorderedArraySet Aesop.PremiseIndex → Aesop.RuleTac.ForwardM Unit
-- Lean.DocString.Types
Lean.Doc.instReprBlock : {i : Type u_1} → {b : Type u_2} → [Repr i] → [Repr b] → Repr (Lean.Doc.Block i b)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- One gets a pseudometric space from an emetric space if the edistance
is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
uniformity are defeq in the pseudometric space and the emetric space.  -/
PseudoEMetricSpace.toPseudoMetricSpace : {α : Type u} → [inst : PseudoEMetricSpace α] → (∀ (x y : α), edist x y ≠ ⊤) → PseudoMetricSpace α
-- Init.Data.UInt.Lemmas
UInt16.sub_mul : ∀ {a b c : UInt16}, (a - b) * c = a * c - b * c
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃FunctorMap_app_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : 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} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] {F F' : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  (φ : F ⟶ F') (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X₁ : C₁) (X₂ : C₂) (X₃ : C₃),
  ((((CategoryTheory.bifunctorComp₂₃FunctorMap φ).app G₂₃).app X₁).app X₂).app X₃ = (φ.app X₁).app ((G₂₃.obj X₂).obj X₃)
-- Mathlib.Algebra.Group.Action.Defs
/-- A typeclass mixin saying that two multiplicative actions on the same space commute.  -/
SMulCommClass : (M : Type u_9) → (N : Type u_10) → (α : Type u_11) → [SMul M α] → [SMul N α] → Prop
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.Topology.EMetricSpace.Basic
/-- A version of `edist_le_range_sum_edist` with each intermediate distance replaced
with an upper estimate.  -/
edist_le_range_sum_of_edist_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : ℕ → α} (n : ℕ) {d : ℕ → ENNReal},
  (∀ {k : ℕ}, k < n → edist (f k) (f (k + 1)) ≤ d k) → edist (f 0) (f n) ≤ ∑ i ∈ Finset.range n, d i
-- Mathlib.Condensed.TopCatAdjunction
/-- The counit of the adjunction `condensedSetToTopCat ⊣ topCatToCondensedSet`  -/
CondensedSet.topCatAdjunctionCounit : (X : TopCat) → X.toCondensedSet.toTopCat ⟶ X
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod.lift_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F₁ F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F ⟶ F₁)
  (τ₂ : F ⟶ F₂) (x : C),
  (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂).app x =
    TypeCat.ofHom fun y =>
      ((CategoryTheory.ConcreteCategory.hom (τ₁.app x)) y, (CategoryTheory.ConcreteCategory.hom (τ₂.app x)) y)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_eq_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k fallback : α}, m.contains k = true → m.getKeyD k fallback = k
-- Std.Async.Basic
/-- Creates a `BaseAsync` that awaits the completion of the given `Task α`.
 -/
Std.Async.BaseAsync.await : {α : Type} → Task α → Std.Async.BaseAsync α
-- Mathlib.CategoryTheory.Enriched.Basic
/-- An enriched functor induces an honest functor of the underlying categories,
by mapping the `(𝟙_ W)`-shaped morphisms.
 -/
CategoryTheory.EnrichedFunctor.forget : {W : Type v'} →
  [inst : CategoryTheory.Category.{w', v'} W] →
    [inst_1 : CategoryTheory.MonoidalCategory W] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory W C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory W D] →
              CategoryTheory.EnrichedFunctor W C D →
                CategoryTheory.Functor (CategoryTheory.ForgetEnrichment W C) (CategoryTheory.ForgetEnrichment W D)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The diagram
```
ℤ_[p]  <--------  (primesEquiv.symm p).adicCompletionIntegers ℚ
   |                          |
   |                          |
   v                          v
ℚ_[p]  <--------  (primesEquiv.symm p).adicCompletion ℚ
```
commutes.  -/
PadicInt.coe_adicCompletionIntegersEquiv_symm_apply : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Algebra R ℚ] [inst_3 : IsFractionRing R ℚ]
  [inst_4 : IsIntegralClosure R ℤ ℚ] (p : Nat.Primes)
  (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ (Rat.HeightOneSpectrum.primesEquiv.symm p))),
  ↑((PadicInt.adicCompletionIntegersEquiv R p).symm x) = (Padic.adicCompletionEquiv R p).symm ↑x
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_succ : ∀ (o : Ordinal.{u_1}), Cardinal.preAleph (Order.succ o) = Order.succ (Cardinal.preAleph o)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Left.one_lt_mul_of_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [IsBotOneClass α] [MulLeftStrictMono α] {b : α},
  1 < b → ∀ (a : α), 1 < a * b
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.ext_hom_hom : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  {c₁ c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt ≅ c₂.pt)
  (w :
    autoParam (∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b)
      CategoryTheory.Limits.Cofan.ext._auto_1),
  (CategoryTheory.Limits.Cofan.ext e w).hom.hom = e.hom
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState : Type
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint and their elements commute, if `B` is a flat `R`-module,
then for any family of `R`-linearly independent elements of `A`,
they are also `B`-linearly independent.  -/
Subalgebra.LinearDisjoint.linearIndependent_left_of_flat_of_commute : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Flat R ↥B] {ι : Type u_1} {a : ι → ↥A},
      LinearIndependent R a → (∀ (a : ↥A) (b : ↥B), Commute ↑a ↑b) → LinearIndependent (↥B) (⇑A.val ∘ a)
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_anti : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α], Antitone leOnePart
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.coe_mk : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  (t : ιₚ → DiscreteTiling.Prototile G X), ↑{ tiles := t } = t
-- Mathlib.Algebra.Group.Basic
add_ne_left : ∀ {M : Type u_4} [inst : AddMonoid M] [IsLeftCancelAdd M] {a b : M}, a + b ≠ a ↔ b ≠ 0
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.coe_eq_carrier`. -/
Topology.CWComplex.Subcomplex.coe_eq_carrier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {E : Topology.RelCWComplex.Subcomplex C}, ↑E = E.carrier
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousWithinAt_unique : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [inst : Unique ι]
  {F : ι → X → α} {S : Set X} {x : X}, EquicontinuousWithinAt F S x ↔ ContinuousWithinAt (F default) S x
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.mem_tangentsFrom_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {as : AffineSubspace ℝ P} {s : EuclideanGeometry.Sphere P} {p : P},
  as ∈ s.tangentsFrom p ↔ as ∈ s.tangentSet ∧ p ∈ as
-- Mathlib.Algebra.BigOperators.Finprod
/-- See also `Finset.prod_bij`.  -/
finprod_mem_eq_of_bijOn : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] {s : Set α} {t : Set β} {f : α → M} {g : β → M}
  (e : α → β), Set.BijOn e s t → (∀ x ∈ s, f x = g (e x)) → ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : β) (_ : j ∈ t), g j
-- Mathlib.Algebra.MvPolynomial.Equiv
Polynomial.toMvPolynomial_X : ∀ {R : Type u_1} {σ : Type u_3} [inst : CommSemiring R] (i : σ),
  (Polynomial.toMvPolynomial i) Polynomial.X = MvPolynomial.X i
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited (Topology.WithLower α)
-- Std.Do.Triple.Basic
/-- A Hoare triple for reasoning about monadic programs. A Hoare triple `Triple x P Q` is a
*specification* for `x`: if assertion `P` holds before `x`, then postcondition `Q` holds after
running `x`.

`⦃P⦄ x ⦃Q⦄` is convenient syntax for `Triple x P Q`.
 -/
Std.Do.Triple : {m : Type u → Type v} →
  {ps : Std.Do.PostShape} → [Std.Do.WP m ps] → {α : Type u} → m α → Std.Do.Assertion ps → Std.Do.PostCond α ps → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Constructor for morphisms from the point of a colimit multicofork.  -/
CategoryTheory.Limits.Multicofork.IsColimit.desc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      {I : CategoryTheory.Limits.MultispanIndex J C} →
        {K : CategoryTheory.Limits.Multicofork I} →
          CategoryTheory.Limits.IsColimit K →
            {T : C} →
              (k : (a : J.R) → I.right a ⟶ T) →
                (∀ (b : J.L),
                    CategoryTheory.CategoryStruct.comp (I.fst b) (k (J.fst b)) =
                      CategoryTheory.CategoryStruct.comp (I.snd b) (k (J.snd b))) →
                  (K.pt ⟶ T)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.count_roots : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : DecidableEq R] (p : Polynomial R),
  Multiset.count a p.roots = Polynomial.rootMultiplicity a p
-- Mathlib.Topology.UniformSpace.CompactConvergence
ContinuousMap.uniformSpace_eq_inf_precomp_of_cover : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {δ₁ : Type u_1} {δ₂ : Type u_2}
  [inst_2 : TopologicalSpace δ₁] [inst_3 : TopologicalSpace δ₂] (φ₁ : C(δ₁, α)) (φ₂ : C(δ₂, α)),
  IsProperMap ⇑φ₁ →
    IsProperMap ⇑φ₂ →
      Set.range ⇑φ₁ ∪ Set.range ⇑φ₂ = Set.univ →
        inferInstance =
          UniformSpace.comap (fun x => x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun x => x.comp φ₂) inferInstance
-- Mathlib.Analysis.Normed.Module.FiniteDimension
summable_of_isBigO_nat' : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [CompleteSpace E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [FiniteDimensional ℝ F] {f : ℕ → E} {g : ℕ → F},
  Summable g → f =O[Filter.atTop] g → Summable f
-- Mathlib.Algebra.DirectSum.Ring
/-- A graded version of `NonUnitalNonAssocSemiring`.  -/
DirectSum.GNonUnitalNonAssocSemiring : {ι : Type u_1} → (A : ι → Type u_2) → [Add ι] → [(i : ι) → AddCommMonoid (A i)] → Type (max u_1 u_2)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_iff_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α}, a ∈ m ↔ (Std.DHashMap.Const.get? m a).isSome = true
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- The functor sending a representation to its complex of inhomogeneous cochains.  -/
groupCohomology.cochainsFunctor : (k G : Type u) →
  [inst : CommRing k] → [inst_1 : Group G] → CategoryTheory.Functor (Rep.{u, u, u} k G) (CochainComplex (ModuleCat k) ℕ)
-- Mathlib.Topology.DiscreteSubset
/-- **Alias** of `Topology.IsInducing.isDiscrete_range`. -/
IsEmbedding.isDiscrete_range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  [DiscreteTopology X], Topology.IsInducing f → IsDiscrete (Set.range f)
-- Mathlib.Data.Nat.SuccPred
Nat.succ_iterate : ∀ (a n : ℕ), Nat.succ^[n] a = a + n
-- Lean.Meta.Tactic.Grind.ReflCmp
Lean.Meta.Grind.propagateReflCmp : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Data.Multiset.Lattice
Multiset.sup.eq_1 : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (s : Multiset α),
  s.sup = Multiset.fold (fun x1 x2 => x1 ⊔ x2) ⊥ s
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_b_ne_zero' : ∀ {R : Type u_1} {b c d : R} [inst : Semiring R], b ≠ 0 → { a := 0, b := b, c := c, d := d }.toPoly.degree = 2
-- Mathlib.Data.Finset.Powerset
Finset.coe_powerset : ∀ {α : Type u_1} (s : Finset α), ↑s.powerset = SetLike.coe ⁻¹' 𝒫 ↑s
-- Mathlib.Logic.Equiv.Prod
Equiv.pprodProd_symm_apply : ∀ {α₁ : Sort u_2} {β₁ : Sort u_5} {α₂ : Type u_9} {β₂ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a : α₂ × β₂),
  (ea.pprodProd eb).symm a = ⟨ea.symm a.1, eb.symm a.2⟩
-- Mathlib.ModelTheory.Definability
/-- A function from tuples of elements of `M` to `M` is definable if its graph is definable.  -/
Set.DefinableFun : {M : Type u_1} → (L : FirstOrder.Language) → [L.Structure M] → {α : Type u_2} → Set M → ((α → M) → M) → Prop
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] [inst_1 : AlgebraicGeometry.IsAffine Y]
  (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f))
      (CategoryTheory.CategoryStruct.comp Y.isoSpec.inv h) =
    CategoryTheory.CategoryStruct.comp X.isoSpec.inv (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Order.Defs.Unbundled
rel_congr_left : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Symm r] [IsTrans α r] {a b c : α}, r a b → (r a c ↔ r b c)
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.instHasDistribNeg : {d : ℤ} → HasDistribNeg (Pell.Solution₁ d)