mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Semigrp.Basic
AddMagmaCat.ext : ∀ {X Y : AddMagmaCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Init.Data.Option.Lemmas
_private.Init.Data.Option.Lemmas.0.Option.bind.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → (α → Option β) → Sort u_3) (a : α) (f : α → Option β)
  (h_1 : (x : α → Option β) → motive none x) (h_2 : (a : α) → (f : α → Option β) → motive (some a) f),
  (match some a, f with
    | none, x => h_1 x
    | some a, f => h_2 a f) =
    h_2 a f
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.instFaithfulModuleCatFunctor : ∀ (R : Type (u + 1)) [inst : Ring R], (CondensedMod.LocallyConstant.functor R).Faithful
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpaceChain_def' : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) (p q : ℤ),
  LieModule.genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Finset.Ioo p q, LieModule.genWeightSpace M (k • χ₁ + χ₂)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u_1, u, u} k K} {B : Rep.{u_1, u, u} k H} {C : Rep.{u_1, u, u} k G} (f : H →* K) (g : G →* H)
  (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C),
  groupCohomology.mapShortComplexH2 (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor g).map φ) ψ) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH2 f φ) (groupCohomology.mapShortComplexH2 g ψ)
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.lt_of_tsub_lt_tsub_left_of_le : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLT α], AddLECancellable b → c ≤ a → a - b < a - c → c < b
-- Mathlib.Data.Nat.Choose.Sum
Int.alternating_sum_range_choose_eq_choose : ∀ {n m : ℕ}, ∑ k ∈ Finset.range (m + 1), (-1) ^ k * ↑((n + 1).choose k) = (-1) ^ m * ↑(n.choose m)
-- Mathlib.Analysis.Calculus.Deriv.Inverse
HasDerivAt.of_comp_left : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {f g h : 𝕜 → 𝕜} {f' h' a : 𝕜},
  ContinuousAt g a → HasDerivAt f f' (g a) → HasDerivAt h h' a → f' ≠ 0 → f ∘ g =ᶠ[nhds a] h → HasDerivAt g (h' / f') a
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.equivalenceRightFractionRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} (X Y : C)
  [W.HasRightCalculusOfFractions], Equivalence CategoryTheory.MorphismProperty.RightFractionRel
-- Std.Time.Format.Modifier
Std.Time.Modifier.n.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.n presentation = Std.Time.Modifier.n presentation_1) = (presentation = presentation_1)
-- Mathlib.Algebra.Homology.CochainComplexPlus
/-- The inclusion of the full subcategory of bounded below cochain complexes
is fully faithful.  -/
CochainComplex.Plus.fullyFaithfulι : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (CochainComplex.Plus.ι C).FullyFaithful
-- Mathlib.Algebra.Ring.Parity
Nat.two_mul_div_two_add_one_of_odd : ∀ {n : ℕ}, Odd n → 2 * (n / 2) + 1 = n
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.instRankOneAdicCompletion`. -/
NumberField.HeightOneSpectrum.NumberField.instRankOneAdicCompletion : (K : Type u_1) →
  [inst : Field K] →
    {R : Type u_2} →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R K] →
          [inst_3 : IsDedekindDomain R] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) → [Module.Finite ℤ R] → [Module.Free ℤ R] → Valued.v.RankOne
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_three_mul : ∀ (x : ℝ), Real.cosh (3 * x) = 4 * Real.cosh x ^ 3 - 3 * Real.cosh x
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instCategory.eq_1 : AddMonCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := AddMonoidHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @AddMonCat.instCategory._proof_1,
    comp_id := @AddMonCat.instCategory._proof_2, assoc := @AddMonCat.instCategory._proof_3 }
-- Mathlib.NumberTheory.Multiplicity
emultiplicity_geom_sum₂_eq_one : ∀ {R : Type u_1} [inst : CommRing R] {x y : R} {p : ℕ} [IsDomain R],
  Prime ↑p → Odd p → ↑p ∣ x - y → ¬↑p ∣ x → emultiplicity (↑p) (∑ i ∈ Finset.range p, x ^ i * y ^ (p - 1 - i)) = 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.HashMap.Raw.unitOfList l).isEmpty = l.isEmpty
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.step.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (upper : α),
  { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper }.step = Std.IterStep.done
-- Init.Core
recSubsingleton : ∀ {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)]
  [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)], Subsingleton (Decidable.casesOn h h₂ h₁)
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
tendsto_arithGeom_atTop_of_one_lt : ∀ {R : Type u_1} {a b u₀ : R} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R],
  1 < a → b / (1 - a) < u₀ → Filter.Tendsto (arithGeom a b u₀) Filter.atTop Filter.atTop
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.Eqv.of_add_left : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m₁ m₂ : M) (n : N),
  TensorProduct.Eqv R M N (FreeAddMonoid.of (m₁, n) + FreeAddMonoid.of (m₂, n)) (FreeAddMonoid.of (m₁ + m₂, n))
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ico_Iic_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ico (Filter.principal (Set.Iic a)) (Filter.principal (Set.Iio a))
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_3.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t)
  (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t) (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_3 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_6 t (Aesop.GoalUnsafe.brecOn_3.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Aesop.Util.UnionFind
Aesop.UnionFind.instEmptyCollection : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → EmptyCollection (Aesop.UnionFind α)
-- Lean.Meta.SynthInstance
/-- Create a new generator node for `mvar` and add `waiter` as its waiter.
`key` must be `mkTableKey mctx mvarType`.  -/
Lean.Meta.SynthInstance.newSubgoal : Lean.MetavarContext → Lean.Expr → Lean.Expr → Lean.Meta.SynthInstance.Waiter → Lean.Meta.SynthInstance.SynthM Unit
-- Mathlib.Analysis.Complex.Basic
Complex.nnnorm_eq_one_of_pow_eq_one : ∀ {ζ : ℂ} {n : ℕ}, ζ ^ n = 1 → n ≠ 0 → ‖ζ‖₊ = 1
-- Mathlib.Order.Filter.Pointwise
/-- If `φ : α →+ β` then `mapAddMonoidHom φ` is the monoid homomorphism
`Filter α →+ Filter β` induced by `map φ`.  -/
Filter.mapAddMonoidHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : AddZeroClass α] →
        [inst_1 : AddZeroClass β] → [inst_2 : FunLike F α β] → [AddMonoidHomClass F α β] → F → Filter α →+ Filter β
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_aux : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    {R : Type u_1} →
      [inst_1 : CommSemiring R] →
        [inst_2 : Algebra R ℤ_[p]] →
          {F : Polynomial R} →
            {a : ℤ_[p]} →
              ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
                (n : ℕ) → { z // ih_gen✝ n z }
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.instIsConnectedStructuredArrowCostructuredArrowObjCostructuredArrowRightwardsOfGuitartExact : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [hw : w.GuitartExact] {X₃ : C₃} (g : CategoryTheory.CostructuredArrow R (B.obj X₃)),
  CategoryTheory.IsConnected (CategoryTheory.StructuredArrow g (w.costructuredArrowRightwards X₃))
-- Init.Control.Except
/-- Runs an action, ensuring that some other action always happens afterward.

More specifically, `tryFinally' x f` runs `x` and then the “finally” computation `f`. If `x`
succeeds with some value `a : α`, `f (some a)` is returned. If `x` fails for `m`'s definition of
failure, `f none` is returned.

`tryFinally'` can be thought of as performing the same role as a `finally` block in an imperative
programming language.
 -/
MonadFinally.tryFinally' : {m : Type u → Type v} → [self : MonadFinally m] → {α β : Type u} → m α → (Option α → m β) → m (α × β)
-- Mathlib.Topology.ClusterPt
clusterPt_sup : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F G : Filter X}, ClusterPt x (F ⊔ G) ↔ ClusterPt x F ∨ ClusterPt x G
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.abs' : ∀ {F : Type u → Type v} [q : QPF F] (x y : (QPF.P F).W), QPF.abs x.dest = QPF.abs y.dest → QPF.Wequiv x y
-- Mathlib.Analysis.InnerProductSpace.Dual
OrthonormalBasis.norm_dual : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace ℝ E]
  (b : OrthonormalBasis ι ℝ E) (L : StrongDual ℝ E), ‖L‖ ^ 2 = ∑ i, L (b i) ^ 2
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigO_abs_right`. -/
Asymptotics.IsBigO.of_abs_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
  (f =O[l] fun x => |u x|) → f =O[l] u
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.ofSubsingleton_apply_toContinuousMultilinearMap : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_4) {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : Subsingleton ι] (i : ι) (f : M →L[R] N),
  ((ContinuousAlternatingMap.ofSubsingleton R M N i) f).toContinuousMultilinearMap =
    (ContinuousMultilinearMap.ofSubsingleton R M N i) f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.unitOfList_singleton : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {k : α}, Std.HashMap.Raw.unitOfList [k] = ∅.insertIfNew k ()
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsLimit.mk : ∀ {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] {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D},
  (∀ {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit (F.mapCone c)),
      Nonempty (CategoryTheory.Limits.IsLimit c)) →
    CategoryTheory.Limits.ReflectsLimit K F
-- Mathlib.Data.Finset.Basic
Finset.inter_filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] (s t : Finset α),
  s ∩ Finset.filter p t = Finset.filter p (s ∩ t)
-- Mathlib.Data.Rel
SetRel.prod_comp_prod_of_inter_nonempty : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t₁ t₂ : Set β},
  (t₁ ∩ t₂).Nonempty → ∀ (s : Set α) (u : Set γ), SetRel.comp (s ×ˢ t₁) (t₂ ×ˢ u) = s ×ˢ u
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  ∃ a,
    a ≠ 0 ∧
      ↑|(Algebra.norm ℚ) ↑a| ≤
        (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K).factorial /
            ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
          √|↑(NumberField.discr K)|
-- Mathlib.Order.Filter.Map
Filter.NeBot.map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α}, f.NeBot → ∀ (m : α → β), (Filter.map m f).NeBot
-- Mathlib.CategoryTheory.CofilteredSystem
/-- If `F` satisfies the Mittag-Leffler condition, its restriction to eventual ranges is a
surjective functor.  -/
CategoryTheory.Functor.surjective_toEventualRanges : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [inst_1 : CategoryTheory.IsCofilteredOrEmpty J],
  F.IsMittagLeffler →
    ∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.toEventualRanges.map f))
-- Mathlib.Data.DFinsupp.Module
DFinsupp.filterLinearMap_apply : ∀ {ι : Type u} (γ : Type w) (β : ι → Type v) [inst : Semiring γ] [inst_1 : (i : ι) → AddCommMonoid (β i)]
  [inst_2 : (i : ι) → Module γ (β i)] (p : ι → Prop) [inst_3 : DecidablePred p] (x : Π₀ (i : ι), β i),
  (DFinsupp.filterLinearMap γ β p) x = DFinsupp.filter p x
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.univ : ∀ {α : Type u_2} {g : Set (Set α)}, Filter.CountableGenerateSets g Set.univ
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.lift'_smul : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M''] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (r : R) (m : LocalizedModule S M),
  r • LocalizedModule.lift' S g h m = LocalizedModule.lift' S g h (r • m)
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
Module.IsReflexive.of_isPerfPair : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair], Module.IsReflexive R M
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J],
  CategoryTheory.Limits.HasColimit F
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.instIsStrictOrderedRing : IsStrictOrderedRing ℝ*
-- Mathlib.Lean.Thunk
Thunk.prod_get_snd : ∀ {α : Type u} {β : Type v} {a : Thunk α} {b : Thunk β}, (a.prod b).get.2 = b.get
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_source' : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  (e.trans e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.inter_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ m₃ m₄ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∩ m₂).Equiv (m₃ ∩ m₄)
-- Mathlib.Algebra.Group.Defs
pow_mul_comm' : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), a ^ n * a = a * a ^ n
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.hom_ext : ∀ {R S : CommRingCat} {f g : R ⟶ S}, CommRingCat.Hom.hom f = CommRingCat.Hom.hom g → f = g
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
/-- A cycle `s : Cycle α`, given `Nodup s` can be interpreted as an `Equiv.Perm α`
where each element in the list is permuted to the next one, defined as `formPerm`.
 -/
Cycle.formPerm : {α : Type u_1} → [DecidableEq α] → (s : Cycle α) → s.Nodup → Equiv.Perm α
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An action is `1`-pretransitive iff it is pretransitive.  -/
MulAction.oneEmbedding_isPretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {one : Type u_5} [Unique one],
  MulAction.IsPretransitive G (one ↪ α) ↔ MulAction.IsPretransitive G α
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `f a ≤ B a`;
* `B` has right derivative `B'` at every point of `[a, b)`;
* for each `x ∈ [a, b)` the right-side limit inferior of `(f z - f x) / (z - x)`
  is bounded above by a function `f'`;
* we have `f' x < B' x` whenever `f x = B x`.

Then `f x ≤ B x` everywhere on `[a, b]`.  -/
image_le_of_liminf_slope_right_lt_deriv_boundary' : ∀ {f f' : ℝ → ℝ} {a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r) →
      ∀ {B B' : ℝ → ℝ},
        f a ≤ B a →
          ContinuousOn B (Set.Icc a b) →
            (∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
              (∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
-- Mathlib.Data.Sym.Sym2
Sym2.toMultiset.eq_1 : ∀ {α : Type u_4} (z : Sym2 α), z.toMultiset = Sym2.lift ⟨fun x1 x2 => ↑[x1, x2], ⋯⟩ z
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiffAt.div` -/
ContDiffAt.fun_div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {f g : E → 𝕜} {n : WithTop ℕ∞},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → g x ≠ 0 → ContDiffAt 𝕜 n (fun i => f i / g i) x
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.pushforward₀Obj_obj_carrier : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor Dᵒᵖ RingCat) (M : PresheafOfModules R) (X : Cᵒᵖ),
  ↑((PresheafOfModules.pushforward₀Obj F R M).obj X) = ↑(M.obj (F.op.obj X))
-- Mathlib.Topology.Continuous
Filter.EventuallyEq.continuousAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {x : X} {y : Y},
  (f =ᶠ[nhds x] fun x => y) → ContinuousAt f x
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y),
  HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass (HomotopicalAlgebra.LeftHomotopyClass.mk f) =
    HomotopicalAlgebra.RightHomotopyClass.mk f
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.left : ∀ {α : Type u_1} [inst : Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂ → Ordnode.Valid' o₁ l ↑x
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.exists_lt_nnnorm_lt : ∀ (α : Type u_2) [inst : DenselyNormedField α] {r₁ r₂ : NNReal}, r₁ < r₂ → ∃ x, r₁ < ‖x‖₊ ∧ ‖x‖₊ < r₂
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.aux_G2_tendsto : ∀ (z : UpperHalfPlane),
  Filter.Tendsto
    (fun N =>
      ∑ m ∈ Finset.range N,
        -8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑↑n * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ((m + 1) * ↑n))
    Filter.atTop
    (nhds
      (-8 * ↑Real.pi ^ 2 *
        ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n))
-- Mathlib.GroupTheory.Coxeter.Basic
IsCoxeterGroup.nonempty_system : ∀ {W : Type u} {inst : Group W} [self : IsCoxeterGroup W], ∃ B M, Nonempty (CoxeterSystem M W)
-- Mathlib.CategoryTheory.Join.Basic
/-- The canonical inclusion from C to `C ⋆ D`.
Terms of the form `(inclLeft C D).map f` should be treated as primitive when working with joins
and one should avoid trying to reduce them. For this reason, there is no `inclLeft_map` simp
lemma.  -/
CategoryTheory.Join.inclLeft : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C (CategoryTheory.Join C D)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instT2Space : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3}, T2Space (CStarMatrix m n A)
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_zero : ∀ (α : Type u_1) [inst : AddMonoidWithOne α], Mathlib.Meta.NormNum.IsNat Zero.zero 0
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.algebraMap_bijective_of_isIntegral : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Ring K] [IsDomain K] [hk : IsAlgClosed k]
  [inst_3 : Algebra k K] [Algebra.IsIntegral k K], Function.Bijective ⇑(algebraMap k K)
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux2.eq_1 : ∀ {α : Type u},
  Computation.parallel.aux2✝ =
    List.foldr
      (fun c o =>
        match o with
        | Sum.inl a => Sum.inl a
        | Sum.inr ls => Computation.rmap (fun c' => c' :: ls) c.destruct)
      (Sum.inr [])
-- Mathlib.Order.SupIndep
/-- **Alias** of the forward direction of `iSupIndep_comp_coe_iff_supIndep`. -/
iSupIndep.supIndep : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {s : Finset ι} {f : ι → α},
  iSupIndep (f ∘ Subtype.val) → s.SupIndep f
-- Mathlib.NumberTheory.MulChar.Duality
MulChar.mem_subgroupOrderIsoSubgroupMulChar_symm_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : CommMonoid M] [inst_1 : CommRing R] [inst_2 : Finite M]
  [inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] {X : Subgroup (MulChar M R)} {m : Mˣ},
  m ∈ (MulChar.subgroupOrderIsoSubgroupMulChar M R).symm (OrderDual.toDual X) ↔ ∀ χ ∈ X, χ ↑m = 1