mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whisker_exchange : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f θ)
      (CategoryTheory.Bicategory.whiskerRight η i) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h)
      (CategoryTheory.Bicategory.whiskerLeft g θ)
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget₂Mon_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommMonCat MonCat)
-- Init.Omega.Constraint
Lean.Omega.Constraint.mk.injEq : ∀ (lowerBound : Lean.Omega.LowerBound) (upperBound : Lean.Omega.UpperBound) (lowerBound_1 : Lean.Omega.LowerBound)
  (upperBound_1 : Lean.Omega.UpperBound),
  ({ lowerBound := lowerBound, upperBound := upperBound } =
      { lowerBound := lowerBound_1, upperBound := upperBound_1 }) =
    (lowerBound = lowerBound_1 ∧ upperBound = upperBound_1)
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.eqLocus_same : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), f.eqLocus f = ⊤
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.congr_fun : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  {f g : α →𝒄 β}, f = g → ∀ (x : α), f x = g x
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndepOn.mono : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {s t : Set ι}, AlgebraicIndepOn R x t → s ⊆ t → AlgebraicIndepOn R x s
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.mk.injEq : ∀ {α : Type u_5} {β : Type u_6} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (toMonoidHom : α →* β)
  (map_zero' : (↑toMonoidHom).toFun 0 = 0)
  (map_add' : ∀ (x y : α), (↑toMonoidHom).toFun (x + y) = (↑toMonoidHom).toFun x + (↑toMonoidHom).toFun y)
  (toMonoidHom_1 : α →* β) (map_zero'_1 : (↑toMonoidHom_1).toFun 0 = 0)
  (map_add'_1 : ∀ (x y : α), (↑toMonoidHom_1).toFun (x + y) = (↑toMonoidHom_1).toFun x + (↑toMonoidHom_1).toFun y),
  ({ toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' } =
      { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }) =
    (toMonoidHom = toMonoidHom_1)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- For any `f : Arrow C`, the map `((ιIteration I κ).app f).right` is
a transfinite composition of isomorphisms.  -/
CategoryTheory.SmallObject.transfiniteCompositionOfShapeιIterationAppRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              (f : CategoryTheory.Arrow C) →
                (CategoryTheory.MorphismProperty.isomorphisms C).TransfiniteCompositionOfShape κ.ord.ToType
                  (CategoryTheory.Arrow.Hom.right ((CategoryTheory.SmallObject.ιIteration I κ).app f))
-- Init.Grind.Attr
/-- Marks a theorem or definition for use by the `lia` (linear integer arithmetic) tactic.

`lia` is `grind` restricted to the `cutsat` solver. It does not use the `@[grind]` lemma
set, but `cutsat` benefits from a small amount of instantiation, e.g. of `Nat.max_def` and
`Nat.min_def`. Lemmas tagged with `@[lia]` form a dedicated set that `lia` instantiates via
E-matching, without enabling the much larger `@[grind]` set.

The modifiers are the same as for `@[grind]`, e.g. `@[lia =]`, `@[lia ←]`, `@[lia →]`.
 -/
Lean.Parser.Attr.lia : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.symbol.injEq : ∀ (prio prio_1 : ℕ), (Lean.Meta.Grind.AttrKind.symbol prio = Lean.Meta.Grind.AttrKind.symbol prio_1) = (prio = prio_1)
-- Mathlib.Topology.Category.TopCat.Basic
/-- The `MorphismProperty` in `TopCat` of a morphism being an embedding.  -/
TopCat.isEmbedding : CategoryTheory.MorphismProperty TopCat
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.X.congr_simp : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K], RatFunc.X = RatFunc.X
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations are reflexive.  -/
AddCon.refl : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) (x : M), c x x
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.comp_apply : ∀ {M N T : AddMonCat} (f : M ⟶ N) (g : N ⟶ T) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Data.EReal.Operations
EReal.add_ne_top : ∀ {x y : EReal}, x ≠ ⊤ → y ≠ ⊤ → x + y ≠ ⊤
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- The algebra isomorphism between multivariable power series in `Option σ` and
power series with coefficients in `MvPowerSeries σ R`.  -/
MvPowerSeries.optionEquivLeft : (σ : Type u_1) →
  (R : Type u_2) → [inst : CommSemiring R] → MvPowerSeries (Option σ) R ≃ₐ[R] PowerSeries (MvPowerSeries σ R)
-- Mathlib.Data.Finsupp.Basic
Finsupp.graph.eq_1 : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M),
  f.graph = Finset.map { toFun := fun a => (a, f a), inj' := ⋯ } f.support
-- Mathlib.LinearAlgebra.Determinant
/-- If the determinant of a map vanishes, then the map is not injective.  -/
LinearMap.bot_lt_ker_of_det_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.Free R M] {f : M →ₗ[R] M}, LinearMap.det f = 0 → ⊥ < f.ker
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.instHashableAlphaKey : Hashable Lean.Meta.Sym.AlphaKey
-- Init.Data.UInt.Bitwise
UInt8.and_neg_one : ∀ {a : UInt8}, a &&& -1 = a
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instDistribMulAction : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {G : ι → Type u_3} →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : Nonempty ι] →
                    [inst_5 : Monoid R] →
                      [inst_6 : (i : ι) → AddMonoid (G i)] →
                        [inst_7 : (i : ι) → DistribMulAction R (G i)] →
                          [inst_8 : ∀ (i j : ι) (h : i ≤ j), DistribMulActionHomClass (T h) R (G i) (G j)] →
                            DistribMulAction R (DirectLimit G f)
-- Init.Tactics
/-- The `sorry` tactic is a temporary placeholder for an incomplete tactic proof,
closing the main goal using `exact sorry`.

This is intended for stubbing-out incomplete parts of a proof while still having a syntactically correct proof skeleton.
Lean will give a warning whenever a proof uses `sorry`, so you aren't likely to miss it,
but you can double check if a theorem depends on `sorry` by looking for `sorryAx` in the output
of the `#print axioms my_thm` command, the axiom used by the implementation of `sorry`.
 -/
Lean.Parser.Tactic.tacticSorry : Lean.ParserDescr
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.RankInfinite.mk : ∀ {α : Type u_1} {M : Matroid α}, (∃ B, M.IsBase B ∧ B.Infinite) → M.RankInfinite
-- Init.Data.Ord.Basic
List.compareLex_nil_nil : ∀ {α : Type u_1} {cmp : α → α → Ordering}, List.compareLex cmp [] [] = Ordering.eq
-- Mathlib.Tactic.WithoutCDot
_private.Mathlib.Tactic.WithoutCDot.0.Lean.Elab.Term.withoutCDotContents.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_eq_of_forall : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α) {a : α},
  (∀ b ∈ s, f b = a) → s.inf' H f = a
-- Std.Http.Data.URI.Basic
Std.Http.URI.instDecidableEqPort.decEq : (x x_1 : Std.Http.URI.Port) → Decidable (x = x_1)
-- Mathlib.Data.ENNReal.Inv
/-- Very general version for distributivity of multiplication over an infimum.

See `ENNReal.iInf_mul_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.iInf_mul` for the special case assuming `Nonempty ι`.  -/
ENNReal.iInf_mul' : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal},
  (a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0) → (a = 0 → Nonempty ι) → (⨅ i, f i) * a = ⨅ i, f i * a
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- If `f : X ⟶ Y` is open, injective, `X` is quasi-compact and `Y` is affine, then `f` is stalkwise
injective if it is injective on global sections.  -/
AlgebraicGeometry.stalkMap_injective_of_isOpenMap_of_injective : ∀ {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine Y] {f : X ⟶ Y} [CompactSpace ↥X],
  IsOpenMap ⇑f →
    Function.Injective ⇑f →
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f)) →
        ∀ (x : ↥X),
          Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x))
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos : Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Tactic.TacticAnalysis
/-- The option corresponding to this pass, used to enable it.

Example: `linter.tacticAnalysis.grindReplacement`.
 -/
Mathlib.TacticAnalysis.Pass.opt : Mathlib.TacticAnalysis.Pass → Option (Lean.Option Bool)
-- Mathlib.Order.PropInstances
Prop.decidablePredBot : {α : Type u} → DecidablePred ⊥
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isNonloop_iff_restrict_of_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α}, e ∈ R → (M.IsNonloop e ↔ (M.restrict R).IsNonloop e)
-- Mathlib.Data.Num.Bitwise
instZeroSNum : Zero SNum
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote' : {α : Type u_1} → [Lean.Grind.Semiring α] → Lean.Grind.CommRing.Context α → Lean.Grind.CommRing.Mon → α
-- Mathlib.Order.Interval.Set.Monotone
Antitone.Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  Antitone f → Monotone g → Monotone fun x => Set.Icc (f x) (g x)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Post-composition by a uniformly continuous function is uniformly continuous on `α →ᵤ β`.

More precisely, if `f : γ → β` is uniformly continuous, then `(fun g ↦ f ∘ g) : (α →ᵤ γ) → (α →ᵤ β)`
is uniformly continuous.  -/
UniformFun.postcomp_uniformContinuous : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] [inst_1 : UniformSpace γ] {f : γ → β},
  UniformContinuous f → UniformContinuous (⇑UniformFun.ofFun ∘ (fun x => f ∘ x) ∘ ⇑UniformFun.toFun)
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.mk : {α : Type u} →
  {β : Type v} →
    {cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw._auto_1} →
      Std.DTreeMap.Raw α (fun x => β) cmp → Std.TreeMap.Raw α β cmp
-- Mathlib.Data.Seq.Defs
Stream'.IsSeq.eq_1 : ∀ {α : Type u} (s : Stream' (Option α)), s.IsSeq = ∀ {n : ℕ}, s n = none → s (n + 1) = none
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Return all encodings of `e` as a `Array Key`. This is used for testing.  -/
Lean.Meta.RefinedDiscrTree.encodeExprWithEta : Lean.Expr → Bool → Lean.MetaM (Array (Array Lean.Meta.RefinedDiscrTree.Key))
-- Mathlib.Data.Matrix.Reflection
Matrix.mulᵣ.eq_1 : ∀ {l m n : ℕ} {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [inst_2 : Zero α] (A : Matrix (Fin l) (Fin m) α)
  (B : Matrix (Fin m) (Fin n) α),
  A.mulᵣ B = Matrix.of (FinVec.map (fun v₁ => FinVec.map (fun v₂ => Matrix.dotProductᵣ v₁ v₂) B.transpose) A)
-- Mathlib.Logic.Lemmas
ite_ite_distrib_left : ∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a b c : α},
  (if p then a else if q then b else c) = if q then if p then a else b else if p then a else c
-- Mathlib.Algebra.Star.Conjneg
conjneg_prod : ∀ {ι : Type u_1} {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R]
  (s : Finset ι) (f : ι → G → R), conjneg (∏ i ∈ s, f i) = ∏ i ∈ s, conjneg (f i)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_erase_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k).getKey? k = none
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
FiniteDimensional.finiteDimensional_self : ∀ (K : Type u) [inst : DivisionRing K], FiniteDimensional K K
-- Mathlib.Logic.Equiv.Fin.Rotate
finCycle_eq_finRotate_iterate : ∀ {n : ℕ} {k : Fin n}, ⇑(finCycle k) = (⇑(finRotate n))^[↑k]
-- Mathlib.Topology.MetricSpace.Bounded
Bornology.IsBounded.subset_ball : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], Bornology.IsBounded s → ∀ (c : α), ∃ r, s ⊆ Metric.ball c r
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {s : Finset ι} {ι' : Type u_9}
  [inst_2 : DecidableEq ι'] [MulLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N},
  (∀ y ∉ t, ∏ x ∈ s with g x = y, f x ≤ 1) → ∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ s with g x = y, f x
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_isCycle₂_iff : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A] (g : G × G)
  (a : A),
  (groupHomology.IsCycle₂ fun₀ | g => a) ↔ ((fun₀ | g.2 => a) + fun₀ | g.1 => g.1 • a) = fun₀ | g.1 * g.2 => g.1 • a
-- Mathlib.CategoryTheory.Monoidal.Closed.Functor
CategoryTheory.MonoidalClosedFunctor.comparison_iso : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {D : Type u'} {inst_1 : CategoryTheory.Category.{v, u'} D}
  {inst_2 : CategoryTheory.CartesianMonoidalCategory C} {inst_3 : CategoryTheory.CartesianMonoidalCategory D}
  {F : CategoryTheory.Functor C D} {inst_4 : CategoryTheory.MonoidalClosed C} {inst_5 : CategoryTheory.MonoidalClosed D}
  {inst_6 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F}
  [self : CategoryTheory.MonoidalClosedFunctor F] (A : C),
  CategoryTheory.IsIso (CategoryTheory.expComparison F A).natTrans
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplexMap_zero : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X Y : A) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A] [Λ.F.PreservesZeroMorphisms],
  Λ.chainComplexMap 0 = 0
-- Mathlib.Algebra.GroupWithZero.Action.Basic
/-- Each element of the group defines an additive monoid isomorphism.

This is a stronger version of `MulAction.toPerm`.  -/
DistribMulAction.toAddEquiv : {G : Type u_1} → (A : Type u_3) → [inst : Group G] → [inst_1 : AddMonoid A] → [DistribMulAction G A] → G → A ≃+ A
-- Lean.Data.PersistentArray
_private.Lean.Data.PersistentArray.0.Lean.PersistentArray.foldlFromMAux : {α : Type u} →
  {m : Type v → Type w} →
    [Monad m] → {β : Type v} → (β → α → m β) → Lean.PersistentArrayNode α → USize → USize → β → m β
-- Init.Data.Nat.Div.Lemmas
Nat.div_le_div_left : ∀ {c b a : ℕ}, c ≤ b → 0 < c → a / b ≤ a / c
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.ContinuousRiemannianMetric.pos : ∀ {B : Type u_4} [inst : TopologicalSpace B] {F : Type u_5} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_6} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (b : B) → TopologicalSpace (E b)]
  [inst_5 : (b : B) → AddCommGroup (E b)] [inst_6 : (b : B) → Module ℝ (E b)] [inst_7 : FiberBundle F E]
  [inst_8 : VectorBundle ℝ F E] (self : Bundle.ContinuousRiemannianMetric F E) (b : B) (v : E b),
  v ≠ 0 → 0 < ((self.inner b) v) v
-- Mathlib.Algebra.Ring.IsFormallyReal
IsSumNonzeroSq.below.sq : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [inst_2 : Zero R] {motive : (a : R) → IsSumNonzeroSq a → Prop} {a : R}
  (ha : a ≠ 0), IsSumNonzeroSq.below ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.down_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.WithInitial.down (CategoryTheory.CategoryStruct.id (CategoryTheory.WithInitial.of X)) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.GroupTheory.Perm.Centralizer
/-- The function that will provide a right inverse `toCentralizer` to `toPermHom`  -/
Equiv.Perm.Basis.ofPermHomFun : {α : Type u_1} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] → {g : Equiv.Perm α} → g.Basis → ↥(Equiv.Perm.OnCycleFactors.range_toPermHom' g) → α → α
-- Std.Time.Format.DateFormat
/-- Narrow AM marker (used by `aaaaa`).
 -/
Std.Time.DateFormatSymbols.amNarrow : Std.Time.DateFormatSymbols → String
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
_private.Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.0.CategoryTheory.Limits.WalkingPair.swap.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) (h_1 : Unit → motive CategoryTheory.Limits.WalkingPair.left)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingPair.right),
  (match CategoryTheory.Limits.WalkingPair.right with
    | CategoryTheory.Limits.WalkingPair.left => h_1 ()
    | CategoryTheory.Limits.WalkingPair.right => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Equivalence.pi_counitIso : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : I → Type u₂}
  [inst_1 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] (E : (i : I) → C i ≌ D i),
  (CategoryTheory.Equivalence.pi E).counitIso = CategoryTheory.NatIso.pi fun i => (E i).counitIso
-- Init.Data.Slice.Array.Lemmas
Array.start_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (Std.Rco.Sliceable.mkSlice xs lo...hi).start = min lo (min hi xs.size)
-- Mathlib.Tactic.Abel
/-- A normal form for `abel`.
Expressions are represented as a list of terms of the form `e = n • x`,
where `n : ℤ` and `x` is an arbitrary element of the additive commutative monoid or group.
We explicitly track the `Expr` forms of `e` and `n`, even though they could be reconstructed,
for efficiency.  -/
Mathlib.Tactic.Abel.NormalExpr : Type
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The currying of `(pullback f).obj A ⟶ X` in `Over I` to a morphism `A ⟶ (pushforward f).obj X`
in `Over J`.  -/
CategoryTheory.ExponentiableMorphism.pushforwardCurry : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J : C} →
      {f : I ⟶ J} →
        [inst_1 : CategoryTheory.ChosenPullbacksAlong f] →
          [inst_2 : CategoryTheory.ExponentiableMorphism f] →
            {X : CategoryTheory.Over I} →
              {A : CategoryTheory.Over J} →
                ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj A ⟶ X) →
                  (A ⟶ (CategoryTheory.ExponentiableMorphism.pushforward f).obj X)
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.mem_sInf : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {𝒮 : Set ↥L} {x : X}, x ∈ sInf 𝒮 ↔ ∀ T ∈ 𝒮, x ∈ T
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot_restrict : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (S : AffineSubspace ℝ P)
  (hS : affineSpan ℝ (Set.range s.points) ≤ S) (i : Fin (n + 1)), ↑((s.restrict S hS).altitudeFoot i) = s.altitudeFoot i
-- Mathlib.Order.Sublocale
Nucleus.restrict_toSublocale : ∀ {X : Type u_1} [inst : Order.Frame X] (n : Nucleus X) (x : X), n.toSublocale.restrict x = ⟨n x, ⋯⟩
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.unit_map_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat) {X Y : Cᵒᵖ}
  (f : X ⟶ Y), (CategoryTheory.ConcreteCategory.hom ((PresheafOfModules.unit R).map f)) 1 = 1
-- Mathlib.Topology.Algebra.Order.Floor
continuousOn_fract : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsTopologicalAddGroup α] (n : ℤ), ContinuousOn Int.fract (Set.Ico (↑n) (↑n + 1))
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.BallPackage.r_le : ∀ {β : Type u_1} {α : Type u_2} (self : Besicovitch.BallPackage β α) (b : β), self.r b ≤ self.r_bound
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.bijective_algebraMap_quotient_residueField : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsMaximal],
  Function.Bijective ⇑(algebraMap (R ⧸ I) I.ResidueField)
-- Mathlib.Data.Num.Bitwise
NzsNum.msb : Bool → NzsNum
-- Mathlib.Probability.Independence.Integration
/-- If `X` and `Y` are independent and integrable random variables and `B`
is a continuous bilinear map, then `∫ ω, B (X ω) (Y ω) ∂μ = B μ[X] μ[Y].`  -/
ProbabilityTheory.IndepFun.integral_bilin : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : MeasurableSpace E] [BorelSpace E]
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] [CompleteSpace F] [inst_8 : MeasurableSpace F]
  [BorelSpace F] [inst_10 : NormedAddCommGroup G] [inst_11 : NormedSpace ℝ G] [CompleteSpace G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable X μ →
      MeasureTheory.Integrable Y μ →
        ∀ (B : E →L[ℝ] F →L[ℝ] G), ∫ (ω : Ω), (B (X ω)) (Y ω) ∂μ = (B (∫ (x : Ω), X x ∂μ)) (∫ (x : Ω), Y x ∂μ)
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.symm_comapSubgroup : ∀ {G : Type u_1} [inst : Group G] {H : Type u_5} [inst_1 : Group H] (e : G ≃* H),
  e.comapSubgroup.symm = e.symm.comapSubgroup
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.declaration : Lean.Lsp.SemanticTokenModifier
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_indicator_one : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} ⦃s : Set X⦄,
  MeasurableSet s → ∫ (x : X), s.indicator 1 x ∂μ = μ.real s
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Return the maximum element of the tree, or the provided default value.

```
findMax' 37 {1, 2, 3} = 3
findMax' 37 ∅ = 37
```  -/
Ordnode.findMax' : {α : Type u_1} → α → Ordnode α → α
-- Mathlib.Topology.VectorBundle.Basic
/-- Natural identification to a `FiberBundleCore`.  -/
VectorBundleCore.toFiberBundleCore : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] → {ι : Type u_5} → VectorBundleCore R B F ι → FiberBundleCore ι B F
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
/-- `coprod F G` is the explicit binary coproduct of type-valued functors `F` and `G`.  -/
CategoryTheory.FunctorToTypes.coprod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor C (Type w) → CategoryTheory.Functor C (Type w) → CategoryTheory.Functor C (Type w)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See also `inv_lt_of_inv_lt₀` for a one-sided implication with one fewer assumption.  -/
inv_lt_comm₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → 0 < b → (a⁻¹ < b ↔ b⁻¹ < a)
-- Init.Data.Array.OfFn
_private.Init.Data.Array.OfFn.0.Array.ofFnM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : Fin n → m α),
  Array.ofFnM f = Fin.foldlM n (fun xs i => xs.push <$> f i) (Array.emptyWithCapacity n)
-- Lean.Meta.Transform
Lean.instReprTransformStep.repr : Lean.TransformStep → ℕ → Std.Format
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries.card_image_eq_of_le_nilpotencyClass : ∀ {G : Type u_1} [inst : AddGroup G] {a : ℕ},
  a ≤ AddGroup.nilpotencyClass G → (AddSubgroup.upperCentralSeries G '' Set.Iic a).ncard = a + 1