mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functorialityEquivalence_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D),
  (CategoryTheory.Limits.Cone.functorialityEquivalence F e).counitIso =
    CategoryTheory.NatIso.ofComponents (fun c => CategoryTheory.Limits.Cone.ext (e.counitIso.app c.pt) ⋯) ⋯
-- Mathlib.Order.Bounds.Basic
/-- If `s` is bounded, then so is `s ∩ t`  -/
BddAbove.inter_of_left : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, BddAbove s → BddAbove (s ∩ t)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Coequifibered.whiskerRight : ∀ {J : Type u_1} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F G : CategoryTheory.Functor J C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Coequifibered α →
    ∀ (H : CategoryTheory.Functor C D)
      [∀ (i j : J) (f : j ⟶ i),
          CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span (F.map f) (α.app j)) H],
      CategoryTheory.NatTrans.Coequifibered (CategoryTheory.Functor.whiskerRight α H)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiable_of_subsingleton : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} [Subsingleton E], MDiff f
-- Mathlib.Order.Shrink
instBotShrink : {α : Type u_1} → [inst : Small.{u, u_1} α] → [Bot α] → Bot (Shrink.{u, u_1} α)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.Type₁.mk.sizeOf_spec : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) (d : ℕ)
  (hd : x.dim = d + 1) (index : Fin (d + 1)) (isIndex : SSet.prodStdSimplex.pairingCore.IsIndex x hd index.succ),
  sizeOf { x := x, d := d, hd := hd, index := index, isIndex := isIndex } =
    1 + sizeOf x + sizeOf d + sizeOf hd + sizeOf index + sizeOf isIndex
-- Batteries.Data.UInt
UInt32.min_def : ∀ (x y : UInt32), x ⊓ y = if x ≤ y then x else y
-- Mathlib.Topology.EMetricSpace.Defs
AddOpposite.edist_op : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x y : α), edist (AddOpposite.op x) (AddOpposite.op y) = edist x y
-- Init.Data.Vector.Range
Vector.take_range : ∀ {n i : ℕ}, (Vector.range n).take i = Vector.range (min i n)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_comm : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {g : α → F} [ContinuousNeg E] {f₁ f₂ : α → E},
  (f₁ - f₂) =o[𝕜; l] g ↔ (f₂ - f₁) =o[𝕜; l] g
-- Mathlib.Order.Category.FinBddDistLat
/-- The equivalence between `FinBddDistLat` and itself induced by `OrderDual` both ways.  -/
FinBddDistLat.dualEquiv : FinBddDistLat ≌ FinBddDistLat
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side.  -/
EuclideanGeometry.dist_div_tan_angle_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
    p₁ ≠ p₂ ∨ p₃ = p₂ → dist p₁ p₂ / Real.tan (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₃ p₂
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
HasCompactSupport.contDiff_convolution_right : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} [inst_3 : RCLike 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : MeasurableSpace G] [inst_9 : NormedAddCommGroup G] [BorelSpace G] [inst_11 : NormedSpace 𝕜 G]
  {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) {n : ℕ∞},
  HasCompactSupport g →
    MeasureTheory.LocallyIntegrable f μ → ContDiff 𝕜 (↑n) g → ContDiff 𝕜 (↑n) (MeasureTheory.convolution f g L μ)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_lt_log_iff : ∀ {x y : ENNReal}, x.log < y.log ↔ x < y
-- Mathlib.Topology.Continuous
continuous_def : ∀ {X : Type u_1} {Y : Type u_2} {x : TopologicalSpace X} {x_1 : TopologicalSpace Y} {f : X → Y},
  Continuous f ↔ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)
-- Mathlib.Algebra.Module.Rat
IsScalarTower.rat : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Module ℚ R]
  [inst_4 : Module ℚ M], IsScalarTower ℚ R M
-- Mathlib.Topology.Algebra.Star
Filter.Tendsto.star : ∀ {α : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Star R] [ContinuousStar R] {f : α → R}
  {l : Filter α} {y : R}, Filter.Tendsto f l (nhds y) → Filter.Tendsto (fun x => star (f x)) l (nhds (star y))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.event : Lean.Lsp.CompletionItemKind
-- Mathlib.Algebra.Module.LocalizedModule.Int
IsLocalizedModule.isInteger_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'), IsLocalizedModule.IsInteger f 0
-- Mathlib.Combinatorics.SetFamily.KruskalKatona
/-- The **Lovasz formulation of the Kruskal-Katona theorem**.

If `|𝒜| ≥ k choose r`, (and everything in `𝒜` has size `r`) then the initial segment we compare to
is just all the subsets of `{0, ..., k - 1}` of size `r`. The `i`-th iterated shadow of this is all
the subsets of `{0, ..., k - 1}` of size `r - i`, so the `i`-th iterated shadow of `𝒜` has at least
`k.choose (r - i)` elements.  -/
Finset.kruskal_katona_lovasz_form : ∀ {n r k i : ℕ} {𝒜 : Finset (Finset (Fin n))},
  i ≤ r → r ≤ k → k ≤ n → Set.Sized r ↑𝒜 → k.choose r ≤ 𝒜.card → k.choose (r - i) ≤ (Finset.shadow^[i] 𝒜).card
-- Mathlib.Data.Countable.Defs
Subsingleton.to_countable : ∀ {α : Sort u} [Subsingleton α], Countable α
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.cons : ∀ {m a : ℕ} {L : List ℕ},
  SimplexCategoryGenRel.IsAdmissible (m + 1) L →
    a ≤ m → (∀ (x : 0 < L.length), a < L[0]) → SimplexCategoryGenRel.IsAdmissible m (a :: L)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.comp_apply : ∀ {A B C : ProfiniteAddGrp.{u}} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A.toProfinite.toTop),
  (ProfiniteAddGrp.Hom.hom (CategoryTheory.CategoryStruct.comp f g)) a =
    (ProfiniteAddGrp.Hom.hom g) ((ProfiniteAddGrp.Hom.hom f) a)
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addRup.sizeOf_spec : ∀ {β : Type u} {α : Type v} [inst : SizeOf β] [inst_1 : SizeOf α] (id : ℕ) (c : β) (rupHints : Array ℕ),
  sizeOf (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) = 1 + sizeOf id + sizeOf c + sizeOf rupHints
-- Init.Data.SInt.Lemmas
Int64.toInt_ofNat_of_lt : ∀ {n : ℕ}, n < 2 ^ 63 → (Int64.ofNat n).toInt = ↑n
-- Mathlib.Order.Lattice
Pi.instLattice : {ι : Type u_1} → {α' : ι → Type u_2} → [(i : ι) → Lattice (α' i)] → Lattice ((i : ι) → α' i)
-- Mathlib.Algebra.Order.Archimedean.Submonoid
SubmonoidClass.instMulArchimedean : ∀ {M : Type u_1} {S : Type u_2} [inst : SetLike S M] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M]
  [inst_3 : SubmonoidClass S M] [MulArchimedean M] (H : S), MulArchimedean ↥H
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.zero_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂),
  CochainComplex.HomComplex.Cochain.comp 0 z₂ h = 0
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_inj : ∀ {m n : ℕ∞}, ↑m = ↑n ↔ m = n
-- Mathlib.Data.Set.Prod
Set.eval_preimage' : ∀ {ι : Type u_1} {α : ι → Type u_2} {i : ι} [inst : DecidableEq ι] {s : Set (α i)},
  Function.eval i ⁻¹' s = {i}.pi (Function.update (fun x => Set.univ) i s)
-- Mathlib.Algebra.Group.Prod
MulHom.coe_fst : ∀ {M : Type u_3} {N : Type u_4} [inst : Mul M] [inst_1 : Mul N], ⇑(MulHom.fst M N) = Prod.fst
-- Mathlib.RepresentationTheory.Continuous.Basic
ContinuousLinearEquiv.isIntertwining_symm_isIntertwining : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {e : V ≃L[R] W},
  (∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) → ∀ (g : G), ↑e.symm ∘SL σ g = ρ g ∘SL ↑e.symm
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.natDegree = WithBot.unbotD 0 p.degree
-- Mathlib.Data.List.TakeDrop
List.drop_length_sub_one : ∀ {α : Type u} {l : List α} (h : l ≠ []), List.drop (l.length - 1) l = [l.getLast h]
-- Mathlib.Topology.Separation.Regular
ULift.instCompletelyNormalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompletelyNormalSpace X], CompletelyNormalSpace (ULift.{u_3, u_1} X)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
/-- Auxiliary definition for `CofibrantObject.HoCat.adj`.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.adjUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor.id (HomotopicalAlgebra.CofibrantObject.HoCat C) ⟶
        HomotopicalAlgebra.CofibrantObject.HoCat.bifibrantResolution.comp
          HomotopicalAlgebra.BifibrantObject.HoCat.ιCofibrantObject
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.find?_toList_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {k : α} {v : β k},
  t.WF → (List.find? (fun x => compare x.fst k == Ordering.eq) t.toList = some ⟨k, v⟩ ↔ t.get? k = some v)
-- Init.Data.Nat.Lemmas
Nat.sub_sub_sub_cancel_right : ∀ {a b c : ℕ}, c ≤ b → a - c - (b - c) = a - b
-- Mathlib.Order.Interval.Set.Monotone
MonotoneOn.Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β} {s : Set α},
  MonotoneOn f s → AntitoneOn g s → AntitoneOn (fun x => Set.Icc (f x) (g x)) s
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.ensureEOS : List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Unit
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_mul_le : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {p q : AddMonoidAlgebra R A} [inst_3 : AddZeroClass A] [inst_4 : Add B],
  (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
    ∀ [AddLeftMono B] [AddRightMono B],
      AddMonoidAlgebra.supDegree D (p * q) ≤ AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
/-- **Monotone convergence theorem** for nonincreasing sequences of functions.  -/
MeasureTheory.lintegral_iInf : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal},
  (∀ (n : ℕ), Measurable (f n)) →
    Antitone f → ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤ → ∫⁻ (a : α), ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
-- Mathlib.Topology.Order.ScottTopology
/-- Type synonym for a preorder equipped with the Scott topology
 -/
Topology.WithScott : Type u_3 → Type u_3
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
Std.IterM.Intermediate.step_appendSnd : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] {it₂ : Std.IterM m β},
  (Std.IterM.Intermediate.appendSnd α₁ it₂).step = do
    let __do_lift ← it₂.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it₂' out, h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.appendSnd α₁ it₂') out ⋯))
      | ⟨Std.IterStep.skip it₂', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.appendSnd α₁ it₂') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_coe : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ⇑↑e = ⇑e
-- Mathlib.RepresentationTheory.Coinduced
/-- Given a monoid homomorphism `φ : G →* H`, the coinduction functors `Rep k G ⥤ Rep k H` given by
`coindFunctor k φ` and `coindFunctor' k φ` are naturally isomorphic, with isomorphism on objects
given by `coindIso φ`.  -/
Rep.coindFunctorIso : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] → [inst_2 : Monoid H] → (φ : G →* H) → Rep.coindFunctor k φ ≅ Rep.coindFunctor' k φ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.ExplorationStep.eq.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {k : α → Ordering} {a : List ((a : α) × β a)}
  {a_1 : Std.DTreeMap.Internal.Cell α β k} {a_2 a_3 : List ((a : α) × β a)} {a_4 : Std.DTreeMap.Internal.Cell α β k}
  {a_5 : List ((a : α) × β a)},
  Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 a_2 = Std.DTreeMap.Internal.Impl.ExplorationStep.eq a_3 a_4 a_5 →
    a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesLimit_finite_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : SemilatticeInf α]
  [inst_2 : OrderTop α] [inst_3 : SemilatticeInf β] [inst_4 : OrderTop β] [inst_5 : InfTopHomClass F α β] {J : Type w}
  [inst_6 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] (K : CategoryTheory.Functor J α),
  CategoryTheory.Limits.PreservesLimit K (↑f).toFunctor
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'Map_f_eq_opcyclesMap : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i'] {i : ι} (hi : e.BoundaryGE i)
  {i' : ι'} (h : e.f i = i'),
  (HomologicalComplex.truncGE'Map φ e).f i =
    CategoryTheory.CategoryStruct.comp (K.truncGE'XIsoOpcycles e h hi).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap φ i') (L.truncGE'XIsoOpcycles e h hi).inv)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
/-- If `C` is a locally `w`-small abelian category with enough injectives,
then `HasExt.{w} C` holds. We do not make this an instance though:
for a given category `C`, there may be different reasonable choices for
the universe `w`, and if we have two `HasExt.{w₁} C` and `HasExt.{w₂} C`
instances, we would have to specify the universe explicitly almost
everywhere, which would be an inconvenience. Then, we must be
very selective regarding `HasExt` instances.  -/
CategoryTheory.hasExt_of_enoughInjectives : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.LocallySmall.{w, v, u} C] [CategoryTheory.EnoughInjectives C], CategoryTheory.HasExt C
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.mk'_top : ∀ (k : Type u_1) (V : Type u_2) {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (p : P), AffineSubspace.mk' p ⊤ = ⊤
-- Mathlib.Geometry.Manifold.Notation
/-- `mfderiv% f x` elaborates to `mfderiv I J f x`,
trying to determine `I` and `J` from the local context.  -/
Manifold.«termMfderiv%__» : Lean.ParserDescr
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.instReprConfig : Repr Mathlib.Tactic.RingNF.Config
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
hasProd_pnat_iff : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} {a : G},
  HasProd (fun x => f ↑x) a ↔ HasProd f (a * f 0)
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.PlausibleStep.fstSkip : ∀ {m : Type w → Type w'} {β α₁ α₂ : Type w} [inst : Std.Iterator α₁ m β] [inst_1 : Std.Iterator α₂ m β]
  {it₁' it₁ : Std.IterM m β} {it₂ : Std.IterM m β},
  it₁.IsPlausibleStep (Std.IterStep.skip it₁') →
    Std.Iterators.Types.Append.PlausibleStep (it₁.append it₂) (Std.IterStep.skip (it₁'.append it₂))
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {k : α} {f : β k → β k} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {he : (Std.Internal.List.modifyKey k f l).isEmpty = false},
      Std.Internal.List.maxKey (Std.Internal.List.modifyKey k f l) he = Std.Internal.List.maxKey l ⋯
-- Mathlib.GroupTheory.OrderOfElement
RightCancelMonoid.infinite_powers : ∀ {G : Type u_1} [inst : RightCancelMonoid G] {a : G}, (↑(Submonoid.powers a)).Infinite ↔ ¬IsOfFinOrder a
-- Mathlib.Data.Nat.Digits.Lemmas
List.fixedLengthDigits_zero : ∀ {b : ℕ} (hb : 1 < b), List.fixedLengthDigits hb 0 = {[]}
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- There is some split equalizer  -/
CategoryTheory.HasSplitEqualizer.splittable : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f g : X ⟶ Y}
  [self : CategoryTheory.HasSplitEqualizer f g], ∃ W h, Nonempty (CategoryTheory.IsSplitEqualizer f g h)
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.inl.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.inl M N = { toFun := fun x => (x, 0), map_zero' := ⋯, map_add' := ⋯ }
-- Lean.Util.ReplaceExpr
Lean.Expr.replaceNoCache : (Lean.Expr → Option Lean.Expr) → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- An isomorphism is in particular a strong monomorphism.  -/
CategoryTheory.strongMono_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : C} (f : Q ⟶ P) [CategoryTheory.IsIso f],
  CategoryTheory.StrongMono f
-- Mathlib.Analysis.Analytic.Basic
/-- If a function `f` is analytic on a set `s` and `g` is linear, then `g ∘ f` is analytic
on `s`.  -/
ContinuousLinearMap.comp_analyticOnNhd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} {s : Set E} (g : F →L[𝕜] G),
  AnalyticOnNhd 𝕜 f s → AnalyticOnNhd 𝕜 (⇑g ∘ f) s
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn_6.go : {motive_1 : Lean.Elab.InfoTree → Sort u} →
  {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u} →
    {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} →
      {motive_4 : Array Lean.Elab.InfoTree → Sort u} →
        {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
          {motive_6 : List Lean.Elab.InfoTree → Sort u} →
            {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
              (t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                ((t : Lean.Elab.InfoTree) → t.below → motive_1 t) →
                  ((t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t) →
                    ((t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t) →
                      ((t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t) →
                        ((t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                            Lean.Elab.InfoTree.below_4 t → motive_5 t) →
                          ((t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t) →
                            ((t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                                Lean.Elab.InfoTree.below_6 t → motive_7 t) →
                              motive_7 t ×' Lean.Elab.InfoTree.below_6 t
-- Mathlib.Analysis.Real.Cardinality
Cardinal.Real.Ioc_countable_iff : ∀ {x y : ℝ}, (Set.Ioc x y).Countable ↔ y ≤ x
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.Normal.mem_comm_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.Normal → ∀ {a b : G}, a + b ∈ H ↔ b + a ∈ H
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_bot_iff : ∀ {α : Type u_1} {s : Set α}, MeasurableSet s ↔ s = ∅ ∨ s = Set.univ
-- Init.Omega.IntList
Lean.Omega.IntList.mul_nil_right : ∀ {xs : List ℤ}, xs * [] = []
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.goCache.match_3.eq_2 : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (motive : Option (aig.RefVec w) → Sort u_1)
  (h_1 : (vec : aig.RefVec w) → motive (some vec)) (h_2 : Unit → motive none),
  (match none with
    | some vec => h_1 vec
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.FieldTheory.SplittingField.Construction
/-- A splitting field of a polynomial.  -/
Polynomial.SplittingField : {K : Type v} → [inst : Field K] → Polynomial K → Type v
-- Mathlib.Data.Finset.Sups
Finset.image_subset_infs_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α} {b : α},
  b ∈ t → Finset.image (fun x => x ⊓ b) s ⊆ s ⊼ t
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEvalRingHom_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (x_1 : Polynomial (Polynomial R)),
  (Polynomial.evalEvalRingHom x y) x_1 = Polynomial.eval x (Polynomial.eval (Polynomial.C y) x_1)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.star : {C : Type u} → CategoryTheory.WithTerminal C
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.isCardinalFiltered_preorder : ∀ (J : Type w) [inst : Preorder J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular],
  (∀ ⦃K : Type w⦄ (s : K → J), Cardinal.mk K < κ → ∃ j, ∀ (k : K), s k ≤ j) → CategoryTheory.IsCardinalFiltered J κ
-- Lean.DocString.Add
/-- Adds a Verso docstring to the environment from a string value, which disables the interactive
features. This should be used for programs that add documentation when there is no syntax available.
 -/
Lean.addVersoDocStringFromString : Lean.Name → String → Lean.Elab.TermElabM Unit
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.inr_ne_inl : ∀ (X Y : AlgebraicGeometry.Scheme) (x : ↥X) (y : ↥Y),
  CategoryTheory.Limits.coprod.inr y ≠ CategoryTheory.Limits.coprod.inl x
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β] (f : InfTopHom α β),
  (InfTopHom.id β).comp f = f