mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Operations
/-- A balanced tree of the given size.  -/
Std.DTreeMap.Internal.Impl.Tree : (α : Type u) → (α → Type v) → ℕ → Type (max u v)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeMap.Raw.unitOfList l cmp).getKey? k' = some k
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionUnitIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] (x : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso x =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (Opposite.op x)).symm.unop
-- Init.Data.Array.Attach
Array.filter_attachWith : ∀ {α : Type u_1} {stop : ℕ} {q : α → Prop} {xs : Array α} {p : { x // q x } → Bool} (H : ∀ x ∈ xs, q x),
  stop = (xs.attachWith q H).size →
    Array.filter p (xs.attachWith q H) 0 stop =
      Array.map
        (fun x =>
          match x with
          | ⟨x, h⟩ => ⟨x, ⋯⟩)
        (Array.filter
          (fun x =>
            match x with
            | ⟨x, h⟩ => p ⟨x, ⋯⟩)
          xs.attach)
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.notValue.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.funUnique.eq_1 : ∀ (α : Type u_2) (M : Type u_4) [inst : Mul M] [inst_1 : Unique α],
  MulEquiv.funUnique α M = { toEquiv := Equiv.funUnique α M, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.ω₁_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : CategoryTheory.ComposableArrows EInt 1} (φ : X ⟶ Y),
  t.ω₁.map φ = t.eTruncLT.map (φ.app 1) ◫ t.eTruncGE.map (φ.app 0)
-- Mathlib.MeasureTheory.Measure.Regular
/-- The measure of a measurable set is the supremum of the measures of compact sets it contains.  -/
MeasurableSet.measure_eq_iSup_isCompact : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] ⦃U : Set α⦄,
  MeasurableSet U → ∀ (μ : MeasureTheory.Measure α) [μ.InnerRegular], μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), μ K
-- Mathlib.Data.FinEnum
/-- Any non-empty enumeration has more than one element.  -/
FinEnum.card_pos : ∀ {α : Type u_1} [inst : FinEnum α] [Nonempty α], 0 < FinEnum.card α
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Equivariant ring homomorphisms.  -/
«MulSemiringActionHomIdLocal≺» : Lean.TrailingParserDescr
-- Lean.Elab.Term.TermElabM
/-- Returns whether `className` has a `deriving` handler installed.
 -/
Lean.Elab.Term.hasDerivingHandler : Lean.Name → IO Bool
-- Std.Async.TCP
/-- Gets the local address of the server socket.
 -/
Std.Async.TCP.Socket.Server.getSockName : Std.Async.TCP.Socket.Server → IO Std.Net.SocketAddress
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The isomorphism `(M₁ →+ N) ≃+ (M₂ →+ N)` obtained by postcomposition with
an additive equivalence `e : M₁ ≃+ M₂`.  -/
AddEquiv.addMonoidHomCongrLeft : {M₁ : Type u_5} →
  {M₂ : Type u_6} →
    {N : Type u_8} →
      [inst : AddZeroClass M₁] →
        [inst_1 : AddZeroClass M₂] → [inst_2 : AddCommMonoid N] → M₁ ≃+ M₂ → (M₁ →+ N) ≃+ (M₂ →+ N)
-- Mathlib.Analysis.Normed.Group.Real
Real.enorm_natCast : ∀ (n : ℕ), ‖↑n‖ₑ = ↑n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List ((a : α) × β a)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (t.insertMany l).getKeyD k' fallback = k
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toBoundedContinuousFunction_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] {β : Type u_6} [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β]
  (f : CompactlySupportedContinuousMap α β) (a : α), f.toBoundedContinuousFunction a = f a
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_cubic : ∀ {R : Type u} {a b c d : R} [inst : Semiring R],
  a ≠ 0 →
    (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X +
          Polynomial.C d).degree =
      3
-- Init.Data.OfScientific
/-- Converts a natural number into the closest-possible 32-bit floating-point number, or an infinite
floating-point value if the range of `Float32` is exceeded.
 -/
Float32.ofNat : ℕ → Float32
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The kernel is a positive semidefinite matrix.  -/
RKHS.posSemidef_kernel : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] (H : Type u_4) [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V], (RKHS.kernel H).PosSemidef
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.CanonicallyOverClass.toOverClass : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {X : C} → {S : semiOutParam C} → [self : CategoryTheory.CanonicallyOverClass X S] → CategoryTheory.OverClass X S
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.Eqv.of_add_scalar : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (r r' : R) (f : (i : ι) → s i),
  PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, f) + FreeAddMonoid.of (r', f)) (FreeAddMonoid.of (r + r', f))
-- Mathlib.Algebra.Ring.Prod
RingEquiv.prodZeroRing_symm_apply : ∀ (R : Type u_1) (S : Type u_3) [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] [inst_2 : Subsingleton S]
  (self : R × S), (RingEquiv.prodZeroRing R S).symm self = self.1
-- Mathlib.Computability.Partrec
_private.Mathlib.Computability.Partrec.0.Nat.lbp : (ℕ →. Bool) → ℕ → ℕ → Prop
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mk_inf_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U V : Set α} {hU : IsOpen U} {hV : IsOpen V},
  { carrier := U, is_open' := hU } ⊓ { carrier := V, is_open' := hV } = { carrier := U ⊓ V, is_open' := ⋯ }
-- Mathlib.GroupTheory.Subgroup.Simple
AddSubgroup.isSimpleAddGroup_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  IsSimpleAddGroup ↥H ↔ H ≠ ⊥ ∧ ∀ H' ≤ H, (H'.addSubgroupOf H).Normal → H' = ⊥ ∨ H' = H
-- Mathlib.FieldTheory.Finite.Valuation
FiniteField.valuation_algebraMap_eq_one : ∀ {Fq : Type u_1} {A : Type u_2} {Γ : Type u_3} [inst : Field Fq] [Finite Fq] [inst_2 : Ring A] [inst_3 : Algebra Fq A]
  [inst_4 : LinearOrderedCommMonoidWithZero Γ] (v : Valuation A Γ) (a : Fq), a ≠ 0 → v ((algebraMap Fq A) a) = 1
-- Init.Data.Int.Order
Int.lt_neg_add_of_add_lt : ∀ {a b c : ℤ}, a + b < c → b < -a + c
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmullerFun_spec : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R},
  (∀ (n : ℕ), ∃ z, (Ideal.Quotient.mk I) z = (Perfection.coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) →
    x.teichmullerFun = y
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.BddBelow_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : LinearOrder Γ] [Nonempty Γ], BddBelow (Function.support 0)
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.instInhabited : {α : Type u} → [inst : UniformSpace α] → [Inhabited α] → Inhabited (CauchyFilter α)
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.algebraMap_quotientMulEquiv_smul : ∀ (G : Type u_1) (G' : Type u_2) [inst : Group G] [inst_1 : Group G'] (A : Type u_5) (B : Type u_6) (C : Type u_7)
  [inst_2 : CommRing A] [inst_3 : CommRing B] [inst_4 : CommRing C] [inst_5 : IsDomain C] [inst_6 : Algebra A B]
  [inst_7 : Algebra A C] [inst_8 : Algebra B C] [inst_9 : FaithfulSMul A B] [inst_10 : FaithfulSMul B C]
  [inst_11 : IsScalarTower A B C] [inst_12 : Finite G] [inst_13 : Finite G'] (N : Subgroup G) [inst_14 : N.Normal]
  [inst_15 : MulSemiringAction G C] [inst_16 : IsGaloisGroup G A C] [inst_17 : IsGaloisGroup (↥N) B C]
  [inst_18 : MulSemiringAction G' B] [inst_19 : IsGaloisGroup G' A B] (g : G) (x : B),
  (algebraMap B C) ((IsGaloisGroup.quotientMulEquiv G G' A B C N) ↑g • x) = g • (algebraMap B C) x
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (X : CategoryTheory.Endofunctor.Algebra F),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).unitIso.inv.app X).f =
    CategoryTheory.CategoryStruct.id X.a
-- Lean.DeprecatedModule
Lean.deprecatedModuleExt : Lean.ModuleEnvExtension (Option Lean.DeprecatedModuleEntry)
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.mul_self : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → t * t = 1
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.stdAddChar_apply : ∀ {N : ℕ} [inst : NeZero N] (j : ZMod N), ZMod.stdAddChar j = ↑(ZMod.toCircle j)
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.«termα⁻¹_» : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofNatLT : ∀ {n : ℕ} {h : n < UInt32.size}, (UInt32.ofNatLT n h).toNat = n
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingHom_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [inst_2 : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J) (x : R) (y : ↥I.primeCompl),
  (Localization.localRingHom I J f hIJ) (IsLocalization.mk' (Localization.AtPrime I) x y) =
    IsLocalization.mk' (Localization.AtPrime J) (f x) ⟨f ↑y, ⋯⟩
-- Mathlib.LinearAlgebra.Contraction
dualTensorHomEquiv.eq_1 : ∀ (R : Type u_2) (M : Type u_3) (N : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Module.Finite R M]
  [inst_6 : Module.Projective R M], dualTensorHomEquiv R M N = LinearEquiv.ofBijective (dualTensorHom R M N) ⋯
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S] {Z : AlgebraicGeometry.Scheme}
  (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S ↘ S) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C))
      (CategoryTheory.CategoryStruct.comp S.isoSpec.inv h)
-- Mathlib.Data.Int.Sqrt
Int.exists_mul_self : ∀ (x : ℤ), (∃ n, n * n = x) ↔ Int.sqrt x * Int.sqrt x = x
-- Init.Data.Array.Lemmas
Array.getElem_swap_right : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} {hi : i < xs.size} {hj : j < xs.size}, (xs.swap i j hi hj)[j] = xs[i]
-- Init.Grind.Module.Basic
/-- Scalar multiplication by one is the identity.  -/
Lean.Grind.IntModule.one_zsmul : ∀ {M : Type u} [self : Lean.Grind.IntModule M] (a : M), 1 • a = a
-- Lean.Compiler.IR.CompilerM
Lean.IR.containsDecl' : Lean.Name → Array Lean.IR.Decl → Lean.IR.CompilerM Bool
-- Init.Data.Int.Order
Int.zero_max_ofNat : ∀ (n : ℕ), max 0 ↑n = ↑n
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.matchesAt_iff_exists_isLongestMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt pat pos ↔
    ∃ endPos, ∃ (h : pos ≤ endPos), String.Slice.Pattern.Model.IsLongestMatch pat (pos.sliceFrom endPos h)
-- Mathlib.Analysis.Normed.Operator.Bilinear
LinearMap.mk₂'ₛₗ.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] (ρ₁₂ : R →+* R₂) (σ₁₂ : S →+* S₂)
  (f f_1 : M → N → P) (e_f : f = f_1) (H1 : ∀ (m₁ m₂ : M) (n : N), f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (H2 : ∀ (c : R) (m : M) (n : N), f (c • m) n = ρ₁₂ c • f m n)
  (H3 : ∀ (m : M) (n₁ n₂ : N), f m (n₁ + n₂) = f m n₁ + f m n₂)
  (H4 : ∀ (c : S) (m : M) (n : N), f m (c • n) = σ₁₂ c • f m n),
  LinearMap.mk₂'ₛₗ ρ₁₂ σ₁₂ f H1 H2 H3 H4 = LinearMap.mk₂'ₛₗ ρ₁₂ σ₁₂ f_1 ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.adjoint_conj : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] {T : E →L[𝕜] E},
  T.IsPositive → ∀ (S : F →L[𝕜] E), (ContinuousLinearMap.adjoint S ∘SL T ∘SL S).IsPositive
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The sieve `S` on `X` `J`-covers an arrow `f` to `X` if `S.pullback f ∈ J Y`.
This definition is an alternate way of presenting a Grothendieck topology.
 -/
CategoryTheory.GrothendieckTopology.Covers : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.GrothendieckTopology C → CategoryTheory.Sieve X → (Y ⟶ X) → Prop
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.bifunctorComp₁₂Iso_hom_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_4} {E : Type u_9}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_3} C₁₂]
  [inst_4 : CategoryTheory.Category.{v_9, u_9} E] (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ E)) (X : C₁) (X_1 : C₂) (X_2 : C₃),
  (((F₁₂.bifunctorComp₁₂Iso G).hom.app X).app X_1).app X_2 =
    CategoryTheory.CategoryStruct.id ((G.obj ((F₁₂.obj X).obj X_1)).obj X_2)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat.inj : ∀ {e : Lean.Expr} {natStructId : ℕ} {lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr} {e_1 : Lean.Expr}
  {natStructId_1 : ℕ} {lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat e natStructId lhs rhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat e_1 natStructId_1 lhs_1 rhs_1 →
    e = e_1 ∧ natStructId = natStructId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.lt_def : ∀ {α : Type u_2} [inst : TopologicalSpace α] {β : Type u_5} [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  [inst_3 : PartialOrder β] {f g : CompactlySupportedContinuousMap α β}, f < g ↔ (∀ (a : α), f a ≤ g a) ∧ ∃ a, f a < g a
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheaf.ι_evalHom : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (N : Type u)
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M N).obj) U)
      (smoothSheaf.evalHom IM I N x) =
    TypeCat.ofHom (smoothSheaf.evalAt IM I N x (Opposite.unop U))
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
fixingAddSubgroup_union : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α},
  fixingAddSubgroup M (s ∪ t) = fixingAddSubgroup M s ⊓ fixingAddSubgroup M t
-- Mathlib.Order.Atoms
Set.isSimpleOrder_Ici_iff_isCoatom : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsSimpleOrder ↑(Set.Ici a) ↔ IsCoatom a
-- Init.Data.Dyadic.Basic
/-- Convert an integer to a dyadic number (which will necessarily have non-positive precision).  -/
Dyadic.ofInt : ℤ → Dyadic
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getEntry? a (Std.Internal.List.insertEntry k v l) =
    if (k == a) = true then some ⟨k, v⟩ else Std.Internal.List.getEntry? a l
-- Mathlib.Analysis.RCLike.Basic
/-- ℝ and ℂ are both of characteristic zero.  -/
RCLike.charZero_rclike : ∀ {K : Type u_1} [inst : RCLike K], CharZero K
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- For natural numbers `n`, the characteristic function for the zeros of `f ^ n` equals `n` times the
characteristic counting function for the zeros of `f`.
 -/
ValueDistribution.characteristic_pow_zero : ∀ {f : ℂ → ℂ} {n : ℕ},
  Meromorphic f → ValueDistribution.characteristic (f ^ n) 0 = n • ValueDistribution.characteristic f 0
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.arrowCongr_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [inst : CommSemiring R]
  [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₁'] [inst_4 : Semiring A₂'] [inst_5 : Algebra R A₁]
  [inst_6 : Algebra R A₂] [inst_7 : Algebra R A₁'] [inst_8 : Algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂')
  (f : A₁ →ₐ[R] A₂), (e₁.arrowCongr e₂) f = ((↑e₂).comp f).comp ↑e₁.symm
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.instBEqSeq.beq.match_1.splitter : (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) →
  (x x_1 : Lean.Grind.AC.Seq) →
    ((a b : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var a) (Lean.Grind.AC.Seq.var b)) →
      ((a : Lean.Grind.AC.Var) →
          (a_1 : Lean.Grind.AC.Seq) →
            (b : Lean.Grind.AC.Var) →
              (b_1 : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons a a_1) (Lean.Grind.AC.Seq.cons b b_1)) →
        ((x x_2 : Lean.Grind.AC.Seq) →
            (∀ (a b : Lean.Grind.AC.Var), x = Lean.Grind.AC.Seq.var a → x_2 = Lean.Grind.AC.Seq.var b → False) →
              (∀ (a : Lean.Grind.AC.Var) (a_1 : Lean.Grind.AC.Seq) (b : Lean.Grind.AC.Var) (b_1 : Lean.Grind.AC.Seq),
                  x = Lean.Grind.AC.Seq.cons a a_1 → x_2 = Lean.Grind.AC.Seq.cons b b_1 → False) →
                motive x x_2) →
          motive x x_1
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `setWidth'` on `BitVec`s.  -/
BitVec.reduceSetWidth' : Lean.Meta.Simp.DSimproc
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_snd_pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β)
  (g : MeasureTheory.SimpleFunc α γ), MeasureTheory.SimpleFunc.map Prod.snd (f.pair g) = g
-- Lean.Environment
_private.Lean.Environment.0.Lean.VisibilityMap.mk.injEq : ∀ {α : Type} («private» «public» private_1 public_1 : α),
  ({ «private» := «private», «public» := «public» } = { «private» := private_1, «public» := public_1 }) =
    («private» = private_1 ∧ «public» = public_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.comp_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} {V3 : Type u_6} {P3 : Type u_7}
  [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1]
  [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : AddCommGroup V3]
  [inst_8 : Module k V3] [inst_9 : AddTorsor V3 P3] (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2),
  (f.comp g).linear = f.linear ∘ₗ g.linear
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- The possible values that can appear in the stack  -/
Lean.Meta.RefinedDiscrTree.StackEntry : Type
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tan_two_mul : ∀ {x : ℝ}, Real.tan (2 * x) = 2 * Real.tan x / (1 - Real.tan x ^ 2)
-- Mathlib.GroupTheory.Nilpotent
AddGroup.IsNilpotent.nilpotent' : ∀ {G : Type u_2} {inst : AddGroup G} [self : AddGroup.IsNilpotent G], ∃ n, AddSubgroup.upperCentralSeries G n = ⊤
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_comp_inv_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (X : ↑(F.obj a)),
  (α.naturality (CategoryTheory.CategoryStruct.comp f g)).inv.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((G.mapComp f g).hom.toNatTrans.app ((α.app a).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((G.map g).toFunctor.map ((α.naturality f).inv.toNatTrans.app X))
        (CategoryTheory.CategoryStruct.comp ((α.naturality g).inv.toNatTrans.app ((F.map f).toFunctor.obj X))
          ((α.app c).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X))))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_eq_isSome_get? : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α}, m.contains a = (m.get? a).isSome
-- Mathlib.Algebra.FreeMonoid.Basic
/-- A variant of `List.sum` that has `[x].sum = x` true definitionally.
The purpose is to make `FreeAddMonoid.lift_eval_of` true by `rfl`.  -/
FreeAddMonoid.sumAux : {M : Type u_6} → [AddMonoid M] → List M → M
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The maximal element that is `< 1` in the value group of a discrete valuation.  -/
ValuativeRel.uniformizer : (R : Type u_1) →
  [inst : Semiring R] → [inst_1 : ValuativeRel R] → [ValuativeRel.IsDiscrete R] → ValuativeRel.ValueGroupWithZero R
-- Lean.Meta.Sym.Arith.Poly
/-- Returns the leading monomial of the given polynomial.  -/
Lean.Grind.CommRing.Poly.lm : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Mon
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : b ≤ a),
  (t.eTruncLTLTIsoLT a b hab).hom = t.eTruncLTLTToLT a b
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.instInhabitedAltExpr.default : {σ : Type} → [Inhabited σ] → Lean.Elab.Term.Do.AltExpr σ
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Helper Lemma for Computations: Extract one factor out of a factorized rational function.
 -/
Function.FactorizedRational.extractFactor : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {d : 𝕜 → ℤ} (u₀ : 𝕜),
  Function.HasFiniteSupport d →
    ∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u =
      (fun x => x - u₀) ^ d u₀ * ∏ᶠ (u : 𝕜), (fun x => x - u) ^ Function.update d u₀ 0 u