mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.π₀.d_fromChainComplexXZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (n : ℕ),
  CategoryTheory.CategoryStruct.comp ((X.chainComplex R).d n 0) (SSet.π₀.fromChainComplexXZero X R) = 0
-- Mathlib.Data.Nat.Digits.Lemmas
/-- The list of digits of `n` in base `b` with some `0`'s appended so that its length is equal to `l`
if it is `< l`. This is an inverse function of `Nat.ofDigits` for `n < b ^ l`,
see `Nat.setInvOn_digitsAppend_ofDigits`.
If `n ≥ b ^ l`, then the list of digits of `n` in base `b` is of length at least `l` and
this function just return `b.digits n`.
 -/
Nat.digitsAppend : ℕ → ℕ → ℕ → List ℕ
-- Mathlib.Data.Finset.NAry
Finset.image₂_subset_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t t' : Finset β},
  t ⊆ t' → Finset.image₂ f s t ⊆ Finset.image₂ f s t'
-- Mathlib.GroupTheory.Order.Min
Monoid.le_minOrder_iff_forall_subgroup : ∀ {G : Type u_1} [inst : Group G] {n : ℕ∞},
  n ≤ Monoid.minOrder G ↔ ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.ncard_left : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G}, Subgroup.IsComplement S ↑H → S.ncard = H.index
-- Mathlib.RingTheory.Multiplicity
pow_dvd_iff_le_emultiplicity : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {k : ℕ}, a ^ k ∣ b ↔ ↑k ≤ emultiplicity a b
-- Mathlib.Topology.Sheaves.Presheaf
/-- If `U ⊆ V` and `f '' U`, `f '' V` are open, then the isomorphisms `f⁻¹ℱ U ≅ ℱ (f '' U)`,
`f⁻¹ℱ V ≅ ℱ (f '' V)` given by `pullbackObjObjOfImageOpen` are compatible with the restriction
maps.  -/
TopCat.Presheaf.pullbackObjObjOfImageOpen_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (ℱ : TopCat.Presheaf C Y) {U V : TopologicalSpace.Opens ↑X}
  (HU : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U))
  (HV : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑V)) (le : U ≤ V),
  CategoryTheory.CategoryStruct.comp (((TopCat.Presheaf.pullback C f).obj ℱ).map (CategoryTheory.homOfLE le).op)
      (TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ U HU).hom =
    CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ V HV).hom
      (ℱ.map (IsOpenMap.functorMap HU HV le).op)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.map.eq_1 : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.FiniteMeasure Ω) (f : Ω → Ω'), ν.map f = ⟨MeasureTheory.Measure.map f ↑ν, ⋯⟩
-- Init.Data.Ord.Basic
List.compareLex.eq_def : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x x_1 : List α),
  List.compareLex cmp x x_1 =
    match x, x_1 with
    | [], [] => Ordering.eq
    | [], x => Ordering.lt
    | x, [] => Ordering.gt
    | x :: xs, y :: ys =>
      match cmp x y with
      | Ordering.lt => Ordering.lt
      | Ordering.eq => List.compareLex cmp xs ys
      | Ordering.gt => Ordering.gt
-- Mathlib.Order.Lex
instLawfulBEqColex : ∀ (α : Type u_2) [inst : BEq α] [LawfulBEq α], LawfulBEq (Colex α)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- (Implementation). This is a (primarily internal) equivalence between natural transformations
and compatible families.

Cf the discussion after Lemma 7.47.10 in <https://stacks.math.columbia.edu/tag/00YW>. See also
the proof of C2.1.4 of [Elephant], and the discussion in [MM92], Chapter III, Section 4.
 -/
CategoryTheory.Presieve.shrinkFunctorHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {S : CategoryTheory.Sieve X} →
        [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
          {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
            ((CategoryTheory.Sieve.shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F) ≃ { x // x.Compatible }
-- Init.Data.SInt.Lemmas
Int32.toUInt32_ofBitVec : ∀ (b : BitVec 32), (Int32.ofBitVec b).toUInt32 = { toBitVec := b }
-- Mathlib.Order.DirSupClosed
dirSupClosedOn_univ : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], DirSupClosedOn Set.univ s ↔ DirSupClosed s
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.rightInvOn : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.RightInvOn (↑e.symm) (↑e) e.target
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- Insert `res` into the section state `s`.  -/
Mathlib.Tactic.ClickSuggestions.SectionState.insertResult : {α : Type} →
  [Ord α] →
    [Inhabited α] →
      Mathlib.Tactic.ClickSuggestions.SectionState α →
        Mathlib.Tactic.ClickSuggestions.Result α →
          (α → α → Lean.MetaM Bool) → Lean.MetaM (Mathlib.Tactic.ClickSuggestions.SectionState α)
-- Init.Data.List.Basic
/-- Returns the index of the first element equal to `a`, or `none` if no element is equal to `a`.

Examples:
* `["carrot", "potato", "broccoli"].idxOf? "carrot" = some 0`
* `["carrot", "potato", "broccoli"].idxOf? "broccoli" = some 2`
* `["carrot", "potato", "broccoli"].idxOf? "tomato" = none`
* `["carrot", "potato", "broccoli"].idxOf? "anything else" = none`
 -/
List.idxOf? : {α : Type u} → [BEq α] → α → List α → Option ℕ
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Infix notation for `OrderAddMonoidIso`.  -/
«term_≃+o_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Constructions
isDiscrete_iff_discreteTopology : ∀ {X : Type u_5} [inst : TopologicalSpace X] {s : Set X}, IsDiscrete s ↔ DiscreteTopology ↑s
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_coproduct : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderFiniteCoproducts] {J : Type u_2} [Finite J] {f : J → C}
  [inst_3 : CategoryTheory.Limits.HasCoproduct f], (∀ (j : J), P (f j)) → P (∐ f)
-- Init.Classical
Classical.skolem : ∀ {α : Sort u} {b : α → Sort v} {p : (x : α) → b x → Prop}, (∀ (x : α), ∃ y, p x y) ↔ ∃ f, ∀ (x : α), p x (f x)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.cons_left_iff : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {a : α} {b : Bool},
  FreeAddGroup.Red.Step ((a, b) :: L₁) L₂ ↔ (∃ L, FreeAddGroup.Red.Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.bijOn_reflection_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  Set.BijOn (⇑(P.reflection i)) (Set.range ⇑P.root) (Set.range ⇑P.root)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry?_eq_maxEntry? : ∀ {α : Type u} {β : Type v} [Ord α] {l : Std.DTreeMap.Internal.Impl α fun x => β},
  Std.DTreeMap.Internal.Impl.Const.maxEntry? l = Option.map (fun x => (x.fst, x.snd)) l.maxEntry?
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.adicValuation_ne_inftyValuation : ∀ {K : Type u_1} [inst : Field K] [inst_1 : DecidableEq (RatFunc K)]
  (p : IsDedekindDomain.HeightOneSpectrum (Polynomial K)),
  IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) p ≠ RatFunc.inftyValuation K
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.whiskerLeft_curry'_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.Closed X] [inst_3 : CategoryTheory.Closed Y] (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X ⟹ Y) (CategoryTheory.MonoidalClosed.curry' f))
      (CategoryTheory.MonoidalClosed.comp X Y Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (X ⟹ Y)).hom
      ((CategoryTheory.ihom X).map f)
-- Mathlib.Algebra.Free
FreeMagma.mul_seq : ∀ {α β : Type u} {f g : FreeMagma (α → β)} {x : FreeMagma α}, f * g <*> x = (f <*> x) * (g <*> x)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.isPathConnected_compl_singleton : ∀ (x : Circle), IsPathConnected {x}ᶜ
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.lift_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z)
  (h : autoParam (CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) _auto_83✝),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.lift a b h)
      (CategoryTheory.ChosenPullbacksAlong.snd f g) =
    b
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instIsTopologicalRingOfLocallyCompactSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [LocallyCompactSpace α]
  [inst_3 : NonUnitalRing β] [inst_4 : IsTopologicalRing β], IsTopologicalRing C(α, β)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} (t : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
  (TopologicalSpace.Opens.map (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base).obj
      (PrimeSpectrum.basicOpen (HomogeneousLocalization.mk t)) =
    (TopologicalSpace.Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ })
      (ProjectiveSpectrum.basicOpen 𝒜 ↑t.num)
-- Mathlib.Order.SymmDiff
le_bihimp_iff : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, c ≤ bihimp a b ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertList_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α},
  Std.Internal.List.containsKey k toInsert = false →
    Std.Internal.List.getKeyD k (Std.Internal.List.insertList l toInsert) fallback =
      Std.Internal.List.getKeyD k l fallback
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.inclusion_right : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  (h : S ≤ T) (x : ↥T) (m : ↑x ∈ S), (Subalgebra.inclusion h) ⟨↑x, m⟩ = x
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.mul_integral_comp_mul_right : ∀ {a b : ℝ} {f : ℝ → ℝ} (c : ℝ), c * ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x
-- Mathlib.RepresentationTheory.Equiv
/-- Equiv between the intertwining map module `(α →₀ G →₀ k) → V` and the function space `α → V`.  -/
Representation.freeLiftLEquiv : {G : Type v} →
  [inst : Monoid G] →
    {V : Type v'} →
      [inst_1 : AddCommMonoid V] →
        {k : Type u} →
          [inst_2 : CommSemiring k] →
            [inst_3 : Module k V] →
              (σ : Representation k G V) → (α : Type w') → (Representation.free k G α).IntertwiningMap σ ≃ₗ[k] α → V
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.levelParams : Lean.Elab.Structural.EqnInfo → List Lean.Name
-- Mathlib.NumberTheory.Padics.ProperSpace
/-- The field of p-adic numbers `ℚ_[p]` is a proper metric space.  -/
Padic.instProperSpace : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ProperSpace ℚ_[p]
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_compl' : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] (s : Set α) (f : α → G), sᶜ.mulIndicator f = f / s.mulIndicator f
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The unoriented angle at `p` between two points not equal to `p` is the absolute value of the
oriented angle.  -/
EuclideanGeometry.angle_eq_abs_oangle_toReal : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ : P}, p₁ ≠ p → p₂ ≠ p → EuclideanGeometry.angle p₁ p p₂ = |(EuclideanGeometry.oangle p₁ p p₂).toReal|
-- Mathlib.Topology.Constructible
IsRetrocompact.isCompact : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} [CompactSpace X], IsRetrocompact s → IsCompact s
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- A subgroup of `Equiv.Perm α` which is (card α - 2)-pretransitive
contains `alternatingGroup α`.  -/
IsMultiplyPretransitive.alternatingGroup_le : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α] (G : Subgroup (Equiv.Perm α)),
  MulAction.IsMultiplyPretransitive (↥G) α (Nat.card α - 2) → alternatingGroup α ≤ G
-- Mathlib.Order.RelClasses
/-- **Alias** of `isTrans_lt`. -/
transitive_lt : ∀ {α : Type u} [inst : Preorder α], IsTrans α LT.lt
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.exists_toPermFiber_eq : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hf : IsQuotientCoveringMap f G) {x : X} (e e' : ↑(f ⁻¹' {x})),
  ∃ g, ((hf.toPermFiber x) g) e = e'
-- Init.Control.Except
ExceptT.instMonadFunctor : {ε : Type u} → {m : Type u → Type v} → MonadFunctor m (ExceptT ε m)
-- Mathlib.Data.Set.Prod
Set.disjoint_univ_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {t₁ t₂ : (i : ι) → Set (α i)},
  Disjoint (Set.univ.pi t₁) (Set.univ.pi t₂) ↔ ∃ i, Disjoint (t₁ i) (t₂ i)
-- Init.Data.List.Nat.TakeDrop
/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
dropping the first `i` elements. Version designed to rewrite from the small list to the big list.  -/
List.getElem_drop : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} {h : j < (List.drop i xs).length}, (List.drop i xs)[j] = xs[i + j]
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.code : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.DeclValue pu
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- Any lift of the zero morphism is homotopic to zero.  -/
CategoryTheory.ProjectiveResolution.liftHomotopyZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        {P : CategoryTheory.ProjectiveResolution Y} →
          {Q : CategoryTheory.ProjectiveResolution Z} →
            (f : P.complex ⟶ Q.complex) → CategoryTheory.CategoryStruct.comp f Q.π = 0 → Homotopy f 0
-- Mathlib.Analysis.Normed.Field.Basic
/-- A normed division ring is a division ring endowed with a seminorm which satisfies the equality
`‖x y‖ = ‖x‖ ‖y‖`.  -/
NormedDivisionRing : Type u_5 → Type u_5
-- Mathlib.Probability.ConditionalProbability
/-- The conditional probability measure of measure `μ` on set `{ω | X ω = x}`.

It is `μ` restricted to `{ω | X ω = x}` and scaled by the inverse of `μ {ω | X ω = x}`
(to make it a probability measure): `(μ {ω | X ω = x})⁻¹ • μ.restrict {ω | X ω = x}`.  -/
ProbabilityTheory.«term__[_|_←_]» : Lean.TrailingParserDescr
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocFrame.mk.injEq : ∀ (content : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (priorParts : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)) (titleString : String)
  (title : Array (Lean.Doc.Inline Lean.ElabInline)) (content_1 : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (priorParts_1 : Array (Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty)) (titleString_1 : String)
  (title_1 : Array (Lean.Doc.Inline Lean.ElabInline)),
  ({ content := content, priorParts := priorParts, titleString := titleString, title := title } =
      { content := content_1, priorParts := priorParts_1, titleString := titleString_1, title := title_1 }) =
    (content = content_1 ∧ priorParts = priorParts_1 ∧ titleString = titleString_1 ∧ title = title_1)
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_ne_zero_iff : ∀ {α : Type u} [inst : Preorder α], Order.cof α ≠ 0 ↔ Nonempty α
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.ctor.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (i : Lean.Compiler.LCNF.CtorInfo) (args : Array (Lean.Compiler.LCNF.Arg pu))
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_5),
  sizeOf (Lean.Compiler.LCNF.LetValue.ctor i args h) = 1 + sizeOf i + sizeOf args + sizeOf h
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.instCommuteWith : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [inst_1 : CategoryTheory.Bicategory.HasAbsLeftKanExtension f g] {x : B} (h : c ⟶ x),
  CategoryTheory.Bicategory.Lan.CommuteWith f g h
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
TopModuleCat.instCategoryWithHomology : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R], CategoryTheory.CategoryWithHomology (TopModuleCat R)
-- Mathlib.Tactic.Bound
Mathlib.Tactic.Bound.Nat.cast_pos_of_pos : ∀ {R : Type} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Nontrivial R] {n : ℕ}, 0 < n → 0 < ↑n
-- Mathlib.RingTheory.Polynomial.GaussNorm
PowerSeries.gaussNorm_monomial : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) {c : ℝ} (r : R)
  [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ],
  0 ≤ c → ∀ (n : ℕ), PowerSeries.gaussNorm (⇑v) c ((PowerSeries.monomial n) r) = v r * c ^ n
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformly.div : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l → TendstoLocallyUniformly G g l → TendstoLocallyUniformly (F / G) (f / g) l
-- Mathlib.GroupTheory.Congruence.BigOperators
AddCon.dfinsuppSumAddHom : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M]
  [inst_2 : (i : ι) → AddCommMonoid (β i)] (c : AddCon M) (h h' : (i : ι) → β i →+ M) {f g : Π₀ (i : ι), β i},
  (∀ (i : ι), c ((h i) (f i)) ((h' i) (g i))) → c ((DFinsupp.sumAddHom h) f) ((DFinsupp.sumAddHom h') g)
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- A well-formed tree is balanced. This is needed here already because we need to know that the
tree is balanced to call the optimized modification functions.
 -/
Std.DTreeMap.Internal.Impl.WF.balanced : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β}, t.WF → t.Balanced
-- Mathlib.Data.List.MinMax
List.maximum.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] (l : List α), l.maximum = List.argmax id l
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits of shape `Jᵒᵖ`, then `F.unop : C ⥤ D` preserves colimits
of shape `J`.  -/
CategoryTheory.Limits.preservesColimitsOfShape_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ)
  [CategoryTheory.Limits.PreservesLimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.PreservesColimitsOfShape J F.unop
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.map_invHomId : ∀ {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} (I : hom.InvStruct) (f : X ⟶ Y),
  (I.map f).invHomId = (I.invHomId.map f).ofEq ⋯ ⋯ ⋯
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.coe_id : ∀ {X : AddMonCat}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeRevM?.find.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (val : β) (h_1 : (val : β) → motive (some val))
  (h_2 : Unit → motive none),
  (match some val with
    | some val => h_1 val
    | none => h_2 ()) =
    h_1 val
-- Mathlib.RingTheory.AdicCompletion.Topology
FilterBasis.mk.congr_simp : ∀ {α : Type u_6} (sets sets_1 : Set (Set α)) (e_sets : sets = sets_1) (nonempty : sets.Nonempty)
  (inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y),
  { sets := sets, nonempty := nonempty, inter_sets := inter_sets } = { sets := sets_1, nonempty := ⋯, inter_sets := ⋯ }
-- Std.Do.SPred.Laws
Std.Do.SPred.bientails.to_eq : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, (P ⊣⊢ₛ Q) → P = Q
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- A morphism is separated if the diagonal map is a closed immersion.  -/
AlgebraicGeometry.IsSeparated.isClosedImmersion_diagonal : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsSeparated f],
  AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.augment_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) (X₀ : C)
  (f : X₀ ⟶ X.obj { len := 0 })
  (w :
    ∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
      CategoryTheory.CategoryStruct.comp f (X.map g₁) = CategoryTheory.CategoryStruct.comp f (X.map g₂)),
  (X.augment X₀ f w).right = X
-- Lean.Meta.Basic
Lean.Meta.mapMetaM : {m : Type → Type u_1} →
  [MonadControlT Lean.MetaM m] → [Monad m] → ({α : Type} → Lean.MetaM α → Lean.MetaM α) → {α : Type} → m α → m α
-- Batteries.Data.List.Scan
List.partialProds_cons : ∀ {α : Type u_1} {a : α} [inst : Mul α] [inst_1 : One α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {l : List α},
  (a :: l).partialProds = 1 :: List.map (fun x => a * x) l.partialProds
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- A morphism that is injective on pseudoelements only maps the zero element to zero.  -/
CategoryTheory.Abelian.Pseudoelement.zero_of_map_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  Function.Injective (CategoryTheory.Abelian.Pseudoelement.pseudoApply f) →
    ∀ (a : CategoryTheory.Abelian.Pseudoelement P), CategoryTheory.Abelian.Pseudoelement.pseudoApply f a = 0 → a = 0
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.disjoint_image_image_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {U V : Set α},
  Disjoint (Quotient.mk' '' U) (Quotient.mk' '' V) ↔ ∀ x ∈ U, ∀ (g : G), g +ᵥ x ∉ V
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.factorsThrough_toFunLifted_π : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {S : Type v} [inst_5 : CommSemiring S] [inst_6 : Algebra R S]
  (f : M →ₚₗ[R] N), Function.FactorsThrough (PolynomialLaw.toFunLifted S f) (PolynomialLaw.π R M S)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.finrank_range_polarization_eq_finrank_span_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [IsDomain R] [IsDomain S] [inst_9 : Algebra S R] [inst_10 : FaithfulSMul S R]
  [inst_11 : P.IsValuedIn S] [inst_12 : Module S M] [inst_13 : IsScalarTower S R M] [inst_14 : Module S N]
  [IsScalarTower S R N] [P.IsAnisotropic],
  Module.finrank S ↥(P.PolarizationIn S).range = Module.finrank S ↥(P.corootSpan S)
-- Mathlib.Algebra.Free
FreeMagma.instMul : {α : Type u} → Mul (FreeMagma α)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.isEquiv_of_val_le_one : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] {v : Valuation K Γ₀} {v' : Valuation K Γ'₀},
  (∀ (x : K), v x ≤ 1 ↔ v' x ≤ 1) → v.IsEquiv v'