mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Predicate
/-- If `L : C ⥤ D` is a localization for `W : MorphismProperty C`, then it is also
the case of a functor obtained by post-composing `L` with an equivalence of categories.  -/
CategoryTheory.Functor.IsLocalization.of_equivalence_target : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_4} [inst_2 : CategoryTheory.Category.{v_4, u_4} E]
  (L' : CategoryTheory.Functor C E) (eq : D ≌ E) [L.IsLocalization W] (e : L.comp eq.functor ≅ L'), L'.IsLocalization W
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_inv_app_hom_apply_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F X : CategoryTheory.Functor C V)
  (a :
    (CategoryTheory.coyoneda.obj
          (Opposite.op
            (F, CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V)).1)).obj
      X)
  (X_1 : C × CategoryTheory.Discrete PUnit.{1}),
  ((CategoryTheory.ConcreteCategory.hom
            ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso F).inv.app X))
          a).app
      X_1 =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X_1.1)).hom
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.prod.rightUnitorEquivalence C).unit.app X_1).1)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X_1.1)).inv
          (CategoryTheory.CategoryStruct.comp
            (((CategoryTheory.CategoryStruct.id
                      ((CategoryTheory.prod.rightInverseUnitor C).comp
                          (CategoryTheory.MonoidalCategory.externalProduct F
                            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))) ⟶
                        (CategoryTheory.prod.rightInverseUnitor C).comp
                          (((CategoryTheory.Functor.id C).prod
                                (CategoryTheory.Functor.fromPUnit
                                  (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).comp
                            ((CategoryTheory.MonoidalCategory.tensor C).comp X)))).hom'
                  ((TypeCat.ofHom fun g =>
                        CategoryTheory.CategoryStruct.comp g
                          (((CategoryTheory.Functor.whiskeringLeft C C V).map
                                (CategoryTheory.NatIso.ofComponents
                                    (fun x => CategoryTheory.MonoidalCategoryStruct.rightUnitor x) ⋯).inv).app
                            X)).hom'
                    ((TypeCat.ofHom fun g =>
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.NatIso.ofComponents
                                (fun x => (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj x)).symm) ⋯).inv
                            g).hom'
                      a))).app
              X_1.1)
            (CategoryTheory.CategoryStruct.comp (X.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X_1.1).hom)
              (CategoryTheory.CategoryStruct.comp
                (X.map ((CategoryTheory.prod.rightUnitorEquivalence C).unitInv.app X_1).1)
                (X.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X_1.1).inv))))))
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.ext_adjoin : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B]
  [inst_7 : StarRing B] [inst_8 : StarModule R A] {s : Set A} [inst_9 : FunLike F (↥(StarAlgebra.adjoin R s)) B]
  [AlgHomClass F R (↥(StarAlgebra.adjoin R s)) B] [StarHomClass F (↥(StarAlgebra.adjoin R s)) B] {f g : F},
  (∀ (x : ↥(StarAlgebra.adjoin R s)), ↑x ∈ s → f x = g x) → f = g
-- Mathlib.Data.Nat.Factorial.Basic
_private.Mathlib.Data.Nat.Factorial.Basic.0.Nat.ascFactorialBinary.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (k n : ℕ) → k = n + 2 → motive n.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k@h:n.succ.succ => h_3 k n h) =
    h_1 ()
-- Lean.Meta.WHNF
/-- Default unfolding function. `e` is of the form `f.{us} a₁ ... aₙ`, and `fInfo` is the `ConstantInfo` for `f`.
This function has special support for unfolding class fields.
The support is particularly important when the user marks a class field as `[reducible]` and
the transparency mode is `.reducible`. For example, suppose `e` is `a ≤ b` where `a b : Nat`,
and `LE.le` is marked as `[reducible]`. Simply unfolding `LE.le` would give `instLENat.1 a b`,
which would be stuck because `instLENat` has transparency `[instance_reducible]`. To avoid this, when we unfold
a `[reducible]` class field, we also unfold the associated projection `instLENat.1` using
`withReducibleAndInstances` (i.e. `.instances` transparency), ultimately returning `Nat.le a b`.
 -/
_private.Lean.Meta.WHNF.0.Lean.Meta.unfoldDefault : Lean.ConstantInfo → List Lean.Level → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.restrictPreimage_surjective`. -/
Function.Surjective.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
  Function.Surjective f → Function.Surjective (t.restrictPreimage f)
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_zero' : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.taylor 0 = LinearMap.id
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.toComposition_boundaries : ∀ {n : ℕ} (c : CompositionAsSet n), c.toComposition.boundaries = c.boundaries
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.builtinDocStrings : IO.Ref (Lean.NameMap String)
-- Mathlib.Dynamics.Ergodic.Conservative
/-- A self-map preserving a finite measure is conservative.  -/
MeasureTheory.MeasurePreserving.conservative : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MeasurePreserving f μ μ → MeasureTheory.Conservative f μ
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- The inverse of a `TransvectionStruct`, designed so that `t.inv.toMatrix` is the inverse of
`t.toMatrix`.  -/
Matrix.TransvectionStruct.inv : {n : Type u_1} → {R : Type u₂} → [CommRing R] → Matrix.TransvectionStruct n R → Matrix.TransvectionStruct n R
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] {t : Set β},
  HasSumLocallyUniformlyOn f g t → s ⊆ t → HasSumLocallyUniformlyOn f g s
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- The prime spectrum of a semiring has discrete Zariski topology iff there are only
finitely many maximal ideals and their intersection is contained in the nilradical.  -/
PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical : ∀ {R : Type u} [inst : CommSemiring R],
  DiscreteTopology (PrimeSpectrum R) ↔ Finite ↑{I | I.IsMaximal} ∧ sInf {I | I.IsMaximal} ≤ nilradical R
-- Mathlib.Order.CompletePartialOrder
Directed.le_iSup : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompletePartialOrder α] {f : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f → ∀ (i : ι), f i ≤ ⨆ j, f j
-- Mathlib.Algebra.Group.Embedding
mulLeftEmbedding_apply : ∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsLeftCancelMul G] (g h : G), (mulLeftEmbedding g) h = g * h
-- Std.Time.DateTime.Timestamp
/-- Converts a `Timestamp` to nanoseconds as `Millisecond.Offset`.
 -/
Std.Time.Timestamp.toMillisecondsSinceUnixEpoch : Std.Time.Timestamp → Std.Time.Millisecond.Offset
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousAt.zpow₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀] [ContinuousMul G₀]
  {X : Type u_4} [inst_4 : TopologicalSpace X] {a : X} {f : X → G₀},
  ContinuousAt f a → ∀ (m : ℤ), f a ≠ 0 ∨ 0 ≤ m → ContinuousAt (fun x => f x ^ m) a
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (sq' : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j) {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp p h) =
    CategoryTheory.CategoryStruct.comp (c.ι.app ⊥) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.exists_walk_of_edist_ne_top : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.edist u v ≠ ⊤ → ∃ p, ↑p.length = G.edist u v
-- Mathlib.Algebra.Algebra.Basic
/-- If there is a linear map `f : A →ₗ[R] B` that preserves `1`, then `algebraMap R B r` is
a unit when `algebraMap R A r` is.  -/
IsUnit.algebraMap_of_algebraMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₗ[R] B),
  f 1 = 1 → ∀ {r : R}, IsUnit ((algebraMap R A) r) → IsUnit ((algebraMap R B) r)
-- Init.Data.BitVec.Lemmas
/-- If `y > x`, then the subtraction `(x - y)` *does* overflow, and the result is the wraparound.
Thus, `(x - y).toNat = 2^w - (y.toNat - x.toNat)`.
 -/
BitVec.toNat_sub_of_lt : ∀ {w : ℕ} {x y : BitVec w}, x < y → (x - y).toNat = 2 ^ w - (y.toNat - x.toNat)
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- The canonical map from `α` to `FreeAbelianGroup α`.  -/
FreeAbelianGroup.of : {α : Type u} → α → FreeAbelianGroup α
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.integral_preimage : ∀ {d : Type u_1} [inst : Fintype d] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  (f : UnitAddTorus d → E) (a : d → ℝ),
  ∫ (x : UnitAddTorus d), f x = ∫ (x : d → ℝ) in {x | ∀ (i : d), x i ∈ Set.Ioc (a i) (a i + 1)}, f fun i => ↑(x i)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.toIdPUnitEquiv_functor_iso : ∀ {B : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} B]
  {L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})}
  {R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})},
  (CategoryTheory.Comma.toIdPUnitEquiv L R).functor = CategoryTheory.Comma.snd L R
-- Mathlib.MeasureTheory.Measure.Prod
/-- For an s-finite measure `ν`, see `prod_apply` below.  -/
MeasureTheory.Measure.prod_apply_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {s : Set (α × β)}, MeasurableSet s → (μ.prod ν) s ≤ ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- A zero object is in particular terminal.  -/
CategoryTheory.Limits.HasZeroObject.hasTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.HasTerminal C
-- Mathlib.Topology.UniformSpace.Cauchy
completeSpace_iff_isComplete_univ : ∀ {α : Type u} [uniformSpace : UniformSpace α], CompleteSpace α ↔ IsComplete Set.univ
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.pow_add : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : α) (k₁ k₂ : ℕ), a ^ (k₁ + k₂) = a ^ k₁ * a ^ k₂
-- Mathlib.Logic.Equiv.Basic
/-- Dependent `curry` equivalence: the type of dependent functions on `Σ i, β i` is equivalent
to the type of dependent functions of two arguments (i.e., functions to the space of functions).

This is `Sigma.curry` and `Sigma.uncurry` together as an equiv.  -/
Equiv.piCurry : {α : Type u_11} →
  {β : α → Type u_9} →
    (γ : (a : α) → β a → Type u_10) → ((x : (i : α) × β i) → γ x.fst x.snd) ≃ ((a : α) → (b : β a) → γ a b)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_left_Ioc : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → ∀ (b c : G₀), (fun x => a * x) '' Set.Ioc b c = Set.Ioc (a * b) (a * c)
-- Mathlib.Data.Set.Basic
Set.union_inter_cancel_right : ∀ {α : Type u} {s t : Set α}, (s ∪ t) ∩ t = t
-- Lean.Meta.Tactic.Backtrack
/-- If we solve any "independent" goals, don't fail.
See `Lean.MVarId.independent?` for the definition of independence.
 -/
Lean.Meta.Tactic.Backtrack.BacktrackConfig.commitIndependentGoals : Lean.Meta.Tactic.Backtrack.BacktrackConfig → Bool
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.eval_zero : ∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L), RatFunc.eval f a 0 = 0
-- Std.Http.Data.Status
Std.Http.Status.unused.sizeOf_spec : sizeOf Std.Http.Status.unused = 1
-- Mathlib.Data.Set.Semiring
SetSemiring.instCommSemigroup : {α : Type u_1} → [CommSemigroup α] → CommSemigroup (SetSemiring α)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instAddCommGroup : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommGroup M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] → [inst_4 : Module R M₂] → AddCommGroup (MultilinearMap R M₁ M₂)
-- Mathlib.Tactic.ReduceModChar
/-- The tactic `reduce_mod_char` looks for numeric expressions in characteristic `p`
and reduces these to lie between `0` and `p`.

For example:
```
example : (5 : ZMod 4) = 1 := by reduce_mod_char
example : (X ^ 2 - 3 * X + 4 : (ZMod 4)[X]) = X ^ 2 + X := by reduce_mod_char
```

It also handles negation, turning it into multiplication by `p - 1`,
and similarly subtraction.

This tactic uses the type of the subexpression to figure out if it is indeed of positive
characteristic, for improved performance compared to trying to synthesise a `CharP` instance.
The variant `reduce_mod_char!` also tries to use `CharP R n` hypotheses in the context.
(Limitations of the typeclass system mean the tactic can't search for a `CharP R n` instance if
`n` is not yet known; use `have : CharP R n := inferInstance; reduce_mod_char!` as a workaround.)
 -/
Tactic.ReduceModChar.reduce_mod_char! : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.card_sInf_range_compl_le : ∀ {ι : Type u} (f : ι → Ordinal.{u}), (sInf (Set.range f)ᶜ).card ≤ Cardinal.mk ι
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `colimit F` is functorial in `F`, when `C` has all colimits of shape `J`.  -/
CategoryTheory.Limits.colim : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [CategoryTheory.Limits.HasColimitsOfShape J C] → CategoryTheory.Functor (CategoryTheory.Functor J C) C
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.RightAdjoint.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {left : a ⟶ b} [inst_1 : SizeOf B] (right : b ⟶ a)
  (adj : CategoryTheory.Bicategory.Adjunction left right),
  sizeOf { right := right, adj := adj } = 1 + sizeOf right + sizeOf adj
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousAt.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace β] {f : α → Set β} {g : γ → α} {x : γ},
  LowerHemicontinuousAt f (g x) → ContinuousAt g x → LowerHemicontinuousAt (f ∘ g) x
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- Expressing locally uniform convergence using `dist`.  -/
Metric.tendstoLocallyUniformly_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {F : ι → β → α}
  {f : β → α} {p : Filter ι},
  TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
-- Mathlib.SetTheory.Cardinal.NatCard
/-- NB: `Nat.card` is defined to be `0` for infinite types.  -/
Finite.card_eq_zero_of_injective : ∀ {α : Type u_1} {β : Type u_2} [Nonempty α] {f : α → β}, Function.Injective f → Nat.card α = 0 → Nat.card β = 0
-- Init.Data.Float.Model.Float32
/-- The logical model for the `Float32` type.

This is defined as the type of `UInt32` with the additional restriction that bit patterns encoding
a `NaN` must be exactly a chosen canonical `NaN`.

Most functions on `Float32.Model` work by unpacking the `Float32.Model` into the inductive type
`UnpackedFloat`, performing the operation there, and then repacking the result into a
`Float32.Model`.

It is not a goal of this development to serve as the basis for a general-purpose floating-point
library or to have any direct lemmas written about it at all. Rather, users interested in a library
about floating-point numbers should develop such a library completely separately, and users
interested in proving properties of their programs involving `Float32` should prove that the
operations defined here are equivalent to the operations defined in the separate library and then
transfer lemmas from the library to the `Float` and `Float32` types.
 -/
Float32.Model : Type
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddMonoid.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : AddMonoid α], Shrink.instAddMonoid = (equivShrink α).symm.addMonoid
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The conjugate of the golden ratio `ψ := (1 - √5)/2`.  -/
Real.goldenConj : ℝ
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vlt_mul : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {a b c d : R}, a <ᵥ b → c <ᵥ d → a * c <ᵥ b * d
-- Mathlib.Topology.Algebra.UniformMulAction
AddMonoid.uniformContinuousConstSMul_nat : ∀ (X : Type x) [inst : UniformSpace X] [inst_1 : AddGroup X] [IsUniformAddGroup X], UniformContinuousConstSMul ℕ X
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The homotopy equivalence between `K` and `K.pathObject`.  -/
HomologicalComplex.pathObject.homotopyEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasPathObject] → (∀ (i : α), ∃ j, c.Rel i j) → HomotopyEquiv K K.pathObject
-- Lean.Parser.Term
Lean.Parser.Term.namedPattern.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Measure.Dirac
/-- A measure on a countable type is a sum of Dirac measures.
If `α` has measurable singletons, `sum_smul_dirac` gives a simpler sum.  -/
MeasureTheory.Measure.exists_sum_smul_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Countable α] (μ : MeasureTheory.Measure α),
  ∃ s, μ = MeasureTheory.Measure.sum fun x => μ (measurableAtom ↑x) • MeasureTheory.Measure.dirac ↑x
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.coe_inj : ∀ {α : Type u_1} [inst : UniformSpace α] [T0Space α] {a b : α}, ↑a = ↑b ↔ a = b
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.instDecidableEqWalk.decEq : {V : Type u_1} → {G : SimpleGraph V} → {a a_1 : V} → [DecidableEq V] → (x x_1 : G.Walk a a_1) → Decidable (x = x_1)
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The composition of the derivative of `extChartAt` with the derivative of the inverse of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).target`.  -/
mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [IsManifold I 1 M] {x : M} {y : E},
  y ∈ (extChartAt I x).target →
    mfderiv% ↑(extChartAt I x) (↑(extChartAt I x).symm y) ∘SL mfderiv[Set.range ↑I] ↑(extChartAt I x).symm y =
      ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) y)
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.fiberwiseColimit.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G G_1 : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H) (e_G : G = G_1)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))],
  CategoryTheory.Limits.fiberwiseColimit G = CategoryTheory.Limits.fiberwiseColimit G_1
-- Init.Data.Fin.Lemmas
Fin.pos_iff_nonempty : ∀ {n : ℕ}, 0 < n ↔ Nonempty (Fin n)
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The multiplication operation in incidence algebras is defined on an interval by summing over
all divisions into two subintervals the product of the values of the original pair of functions.
 -/
IncidenceAlgebra.instMul : {𝕜 : Type u_2} →
  {α : Type u_5} →
    [inst : Preorder α] → [LocallyFiniteOrder α] → [inst_2 : AddCommMonoid 𝕜] → [Mul 𝕜] → Mul (IncidenceAlgebra 𝕜 α)
-- Mathlib.Analysis.Normed.Module.Bases
/-- The sum converges to `x` along the provided `SummationFilter L`.  -/
GeneralSchauderBasis.expansion : ∀ {β : Type u_3} {𝕜 : Type u_4} {X : Type u_5} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {L : SummationFilter β} (self : GeneralSchauderBasis β 𝕜 X L) (x : X),
  HasSum (fun i => (self.coord i) x • ↑self i) x L
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.Nat.cast_eq_algebraMap : ∀ (A : Type u_1) [inst : CommSemiring A] (n : ℕ), ↑n = (algebraMap ℕ A) n
-- Init.Data.List.ToArray
List.forIn'_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (l : List α) (b : β)
  (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)), forIn' l.toArray b f = forIn' l b fun a m b => f a ⋯ b
-- Mathlib.Topology.Algebra.LinearMapCompletion
AddMonoidHom.extension.congr_simp : ∀ {α : Type u_3} {β : Type u_4} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α]
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [inst_5 : IsUniformAddGroup β] [inst_6 : CompleteSpace β]
  [inst_7 : T0Space β] (f f_1 : α →+ β) (e_f : f = f_1) (hf : Continuous ⇑f), f.extension hf = f_1.extension ⋯
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.insepDegree_bot : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], Field.insepDegree F ↥⊥ = 1
-- Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.PatternMatchState.occs.inj : ∀ {subgoals : Array (ℕ × Lean.MVarId)} {idx : ℕ} {remaining : List (ℕ × ℕ)} {subgoals_1 : Array (ℕ × Lean.MVarId)}
  {idx_1 : ℕ} {remaining_1 : List (ℕ × ℕ)},
  Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals idx remaining =
      Lean.Elab.Tactic.Conv.PatternMatchState.occs subgoals_1 idx_1 remaining_1 →
    subgoals = subgoals_1 ∧ idx = idx_1 ∧ remaining = remaining_1
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.commute_sub_nat : ∀ (f : CircleDeg1Lift) (n : ℕ), Function.Commute ⇑f fun x => x - ↑n
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `s ⊆ fixedBy α g`, then `g • s = s`, which means that `s ∈ fixedBy (Set α) g`.

Note that the reverse implication is in general not true, as `s ∈ fixedBy (Set α) g` is a
weaker statement (it allows for points `x ∈ s` for which `g • x ≠ x` and `g • x ∈ s`).
 -/
MulAction.set_mem_fixedBy_of_subset_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {s : Set α} {g : G},
  s ⊆ MulAction.fixedBy α g → s ∈ MulAction.fixedBy (Set α) g